Integrate the Haskell code generate from agda-spec into the build system and CI

[geo2a]

The PR #1315 by @javierdiaz72 adds an executable specification of a part of the consensus layer in Agda.

We need to integrate the spec into the repo's build system and CI:

• check the spec in CI this is already done on main when building the PDF spec
• generate the Haskell code from the spec and run the unit-tests for it. That probably involves integrating the generated code into the top-level Cabal project.
• generate the pdf from the spec (optionally in CI?), which means forwarding the relevant bits to ./nix/pdfs.nix. this is already done on main.

[javierdiaz72]

That probably involves integrating the generated code into the top-level Cabal project.

I would say that the right thing to do is to effectively integrate the code generation part into the top-level Cabal project since, as a workaround, I created an "empty" cabal.project file in Spec/hs-src with the only purpose of the top-level one not interfering with my work.

[geo2a]

I've tried a couple of things today to integrate the the Agda spec and the generated code into the existing Nix build system. Much has already been done by Alex Esgen, i.e. we seem to actually build the pdfs in CI and thus implicitly also type-check the Agda development.

So what remains to be done is the code generation.

Nix mkDerivation approach

A similar setup exists in the formal-ledger-specifications.

After exploring the Nix rabbit hole for a while, I've found a sequence of steps that would allow to expose the extracted code at the top level:

• add an attribute for the extracted code into nix/agda.nix:

  hsSrc = pkgs.stdenv.mkDerivation {
    inherit (locales) LANG LC_ALL LOCALE_ARCHIVE;
    pname = "agda-spec-hs-src";
    version = "0.1";
    src = ../docs/agda-spec;
    meta = { };
    buildInputs = [ agda pkgs.ghc pkgs.cabal ];
    buildPhase = ''
      export CABAL_DIR=$out/haskell/.cabal
      OUT_DIR=$out make hs
    '';
    doCheck = true;
    checkPhase = ''
      test -n "$(find $out/haskell/ -type f -name '*.hs')"
      # OUT_DIR=$out make hsTest
    '';
    dontInstall = true;
  };
  

• this attribute will become exposed in the top-level flake, build it:

  nix build .#hydraJobs.x86_64-linux.native.agda-spec.hsSrc
  

  this will put the sources in ./result/haskell/Spec/.

• put ./result/haskell/Spec/cardano-consensus-executable-spec.cabal into the cabal.project file

• run cabal build cardano-consensus-executable-spec, cabal test cardano-consensus-executable-spec, etc.

I am not satisfied with this approach, because it requires to list a potentially non-existing package in the top-level cabal.project.

Nix haskell-nix.cabalProject approach

As an alternative, I've tried using haskell.nix to pick-up the extracted sources:

hsPkgs = haskell-nix.cabalProject {
  src = "${hsSrc}/haskell/Spec/";
  compiler-nix-name = "ghc966";
  inputMap = {
    "https://chap.intersectmbo.org/" = inputs.CHaP;
  };
};

however, when I try to build that with nix build .#hydraJobs.x86_64-linux.native.agda-spec.hsPkgs, I get a somewhat unhelpful error message:

> cleaned source is empty. Did you forget to 'git add -A'?

which probably comes from haskell.nix.

So looks like it's not straightforward to use haskell.nix. without committing the generated sources.

[geo2a]

I've replicated the second component of the setup in the formal-ledger repo.
This amounts to having two separate derivations: one for sources, and another for the building them:

hsSrc = pkgs.stdenv.mkDerivation {
  inherit (locales) LANG LC_ALL LOCALE_ARCHIVE;
  pname = "agda-spec-hs-src";
  version = "0.1";
  src = ../docs/agda-spec;
  meta = { };
  buildInputs = [ agda customAgda.ghc customAgda.cabal-install ];
  buildPhase = ''
    # export CABAL_DIR=$out/haskell/.cabal
    OUT_DIR=$out make hs
  '';
  doCheck = true;
  checkPhase = ''
    test -n "$(find $out/haskell/ -type f -name '*.hs')"
    # OUT_DIR=$out make hsTest
  '';
  dontInstall = true;
};

hsExe = customAgda.haskellPackages.callCabal2nixWithOptions "cardano-consensus-executable-spec" "${hsSrc}/haskell/Spec" "--no-haddock" {};

However, I'm still hitting a roadblock. Unfortunately trying to build the second derivation (from the top-level flake):

nix build .#hydraJobs.x86_64-linux.native.agda-spec.hsExe

results in GHC panics, e.g.

�[;1m<no location info>: �[;1m�[31merror�[0m�[0m�[;1m:�[0m�[0m�[;1m
    panic! (the 'impossible' happened)
  GHC version 9.6.6:
        getStgArgFromTrivialArg
  (scc<d_'42''45'1'45'rawGroup_24> d__'42'__14)
  `cast` (SelCo:Fun(arg)
              (Sub Univ(nominal CorePrep
                        :: (T_Sign_6 -> T_Sign_6 -> T_Sign_6)
                           -> Any -> (T_Sign_6 -> T_Sign_6) -> T_RawGroup_96, (Any
                                                                               -> Any -> Any)
                                                                              -> Any
                                                                              -> (Any -> Any)
                                                                              -> T_RawGroup_96))
          :: (T_Sign_6 -> T_Sign_6 -> T_Sign_6) ~R# (Any -> Any -> Any))
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/GHC/Utils/Panic.hs:189:37 in ghc:GHC.Utils.Panic
        pprPanic, called at compiler/GHC/CoreToStg.hs:587:13 in ghc:GHC.CoreToStg
  CallStack (from HasCallStack):
    panic, called at compiler/GHC/Utils/Error.hs:454:29 in ghc:GHC.Utils.Error

I'm attaching the full log for reference.
nix-log.txt

Unfortunately, I'll have to give up at that point. It is probably better to wait until Alex Esgen is back from holiday in January.

[geo2a]

Ended up looking a little further into this.

I've noticed that cabal2nix builds the package several times, i.e. includes a profiling-enabled build.

It turns out the panic is in-fact a known issue in GHC encountered by @Soupstraw when generating Haskell from the ledger Agda spec. The issue only seems to manifest in a profiled build. Even though the issue seems to have been resolved in GHC 9.6.6, I still get it.

Disabling the profiled build helps:

hsExe = customAgda.haskell.lib.disableLibraryProfiling (customAgda.haskellPackages.callCabal2nixWithOptions "cardano-consensus-executable-spec" "${hsSrc}/haskell/Spec" "--no-haddock" {});

in the end, we get the generated code built and the tests by calling

nix build .#hydraJobs.x86_64-linux.native.agda-spec.hsExe

and breaking the tests actually makes this build fail.

[geo2a]

I have also decided against integrating the generated code into the top-level cabal.project. The generated code is ephemeral and it requires installing Agda to be generated, thus the package declaration would refer to the code that potentially does not exist. This could interfere with the development process, as not everyone on the team uses Nix and definitely not everyone wants to install Agda.