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.

Sign up for GitHub

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

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

Merged
merged 2 commits into from
Dec 16, 2024
Merged

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

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4e65a0e
Use GHC that comes with Agda and expose it in the shell
geo2a Dec 13, 2024
a9e2699
Emit, build and test the Haskell code from `agda-spec`
geo2a Dec 13, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 27 additions & 2 deletions nix/agda.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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
Expand Down
Loading