Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Generate Haskell code from the Agda spec #1315

Draft
wants to merge 12 commits into
base: main
Choose a base branch
from
Prev Previous commit
Next Next commit
Emit, build and test the Haskell code from agda-spec
  • Loading branch information
geo2a committed Dec 13, 2024
commit a9e269991f8e00a05a89e3b161fd1e0deae2586e
27 changes: 26 additions & 1 deletion nix/agda.nix
Original file line number Diff line number Diff line change
@@ -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
Loading