Merge remote-tracking branch 'refs/remotes/origin/javierdiaz72/agda-s…

…pec-to-haskell' into javierdiaz72/agda-spec-to-haskell

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