From 4e65a0efa106aefd35f6731090079d117b6a055c Mon Sep 17 00:00:00 2001
From: Georgy Lukyanov <mail@geo2a.info>
Date: Fri, 13 Dec 2024 11:46:26 +0100
Subject: [PATCH 1/2] Use GHC that comes with Agda and expose it in the shell

---
 nix/agda.nix | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/nix/agda.nix b/nix/agda.nix
index 03f91165c9..c41b532a5d 100644
--- a/nix/agda.nix
+++ b/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;
@@ -83,7 +83,7 @@ let
     };
 
     shell = pkgs.mkShell {
-      packages = [ agda latex ];
+      packages = [ agda latex customAgda.ghc customAgda.cabal-install];
     };
   };
 in

From a9e269991f8e00a05a89e3b161fd1e0deae2586e Mon Sep 17 00:00:00 2001
From: Georgy Lukyanov <mail@geo2a.info>
Date: Fri, 13 Dec 2024 11:50:06 +0100
Subject: [PATCH 2/2] Emit, build and test the Haskell code from `agda-spec`

---
 nix/agda.nix | 27 ++++++++++++++++++++++++++-
 1 file changed, 26 insertions(+), 1 deletion(-)

diff --git a/nix/agda.nix b/nix/agda.nix
index c41b532a5d..9cfd55e58a 100644
--- a/nix/agda.nix
+++ b/nix/agda.nix
@@ -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 customAgda.ghc customAgda.cabal-install];
+      packages = [ agda latex customAgda.ghc customAgda.cabal-install ];
     };
   };
 in