Emit, build and test the Haskell code from agda-spec

nix/agda.nix

@@ -82,6 +82,31 @@ 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 customAgda.ghc customAgda.cabal-install];
     };