Integrate the Haskell code emitted from agda-spec into CI (#1344)

Fixes #1343
Note that this PR targets the branch of
#1315 and not
`main`.

This PR adds Nix derivations that:
- generate Haskell code from the Agda spec using the `Makefile`-based
build system in `./docs/agda-spec/`
- wrap the generated code into Nix using `cabal2nix`

In combination with the existing set-up in `flake.nix`, we can now build
the generated code and run it's tests using the following flake output:
```
nix build .#hydraJobs.x86_64-linux.native.agda-spec.hsExe
```
which will also be done in CI, i.e. see the logs from testing this PR
- the job
[x86_64-linux.native.agda-spec.hsExe](https://ci.iog.io/build/6263029/log)
builds and runs tests for the generated code

some other jobs, e.g. the linting of the unit tests for the generated
code, are failing, but we can fix those in
#1315

nix/agda.nix

@@ -49,7 +49,7 @@ let
   };
 
   deps = [ agdaStdlib agdaStdlibClasses agdaStdlibMeta ];
-  agdaWithPkgs = p: customAgda.agda.withPackages { pkgs = p; ghc = pkgs.ghc; };
+  agdaWithPkgs = p: customAgda.agda.withPackages { pkgs = p; };
 
   attrs = pkgs.recurseIntoAttrs rec {
     agda = agdaWithPkgs deps;
@@ -82,8 +82,33 @@ let
       dontInstall = true;
     };
 
+    # this derivation generates the Haskell code from the Agda spec, but does
+    # not build or test it.
+    # TODO(georgy.lukyanov): share agda typechecking with the docs derivation
+    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 = ''
+        OUT_DIR=$out make hs
+      '';
+      doCheck = true;
+      checkPhase = ''
+        test -n "$(find $out/haskell/ -type f -name '*.hs')"
+      '';
+      dontInstall = true;
+    };
+
+    # this derivation picks up the Haskell project generated by hsSrc and
+    # builds and tests it. Note that the profiled build is intentionally disabled
+    # as is causes some GHC versions to panic.
+    hsExe = customAgda.haskell.lib.disableLibraryProfiling (customAgda.haskellPackages.callCabal2nixWithOptions "cardano-consensus-executable-spec" "${hsSrc}/haskell/Spec" "--no-haddock" { });
+
     shell = pkgs.mkShell {
-      packages = [ agda latex ];
+      packages = [ agda latex customAgda.ghc customAgda.cabal-install ];
     };
   };
 in