diff options
| -rw-r--r-- | flake.nix | 74 |
1 files changed, 39 insertions, 35 deletions
@@ -52,21 +52,22 @@ version = "0.1.0"; duneVersion = "3"; src = ./compiler; - OCAMLPARAM="_,warn-error=+A"; # Turn all warnings into errors. + OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors. propagatedBuildInputs = [ - easy_logging charon.packages.${system}.charon-ml - ] ++ (with ocamlPackages; [ - calendar - core_unix - ppx_deriving - visitors - yojson - zarith - ocamlgraph - unionFind - ]); + easy_logging + charon.packages.${system}.charon-ml + ] ++ (with ocamlPackages; [ + calendar + core_unix + ppx_deriving + visitors + yojson + zarith + ocamlgraph + unionFind + ]); afterBuild = '' - echo charon.packages.${system}.tests + echo charon.packages.${system}.tests ''; }; # Run the translation on various files. @@ -119,7 +120,7 @@ name = "aeneas_verify_fstar"; src = ./tests/fstar; FSTAR_EXE = "${hacl-nix.packages.${system}.fstar}/bin/fstar.exe"; - buildPhase= '' + buildPhase = '' make prepare-projects make verify -j $NIX_BUILD_CORES ''; @@ -131,7 +132,7 @@ name = "aeneas_verify_coq"; src = ./tests/coq; buildInputs = [ pkgs.coq ]; - buildPhase= '' + buildPhase = '' make prepare-projects make verify -j $NIX_BUILD_CORES ''; @@ -155,7 +156,7 @@ # || pkgs.lib.hasPrefix (toString ./tests/hol4) path; # }; buildInputs = [ pkgs.hol ]; - buildPhase= '' + buildPhase = '' cd ./tests/hol4 make prepare-projects make verify -j $NIX_BUILD_CORES @@ -164,21 +165,23 @@ installPhase = "touch $out"; }; - check-charon-pin = pkgs.runCommand "aeneas-check-charon-pin" { - buildInputs = [ pkgs.jq ]; - } '' - CHARON_REV_FROM_FLAKE="$(jq -r .nodes.charon.locked.rev ${./flake.lock})" - CHARON_REV_FROM_PIN="$(tail -1 ${./charon-pin})" - if [[ "$CHARON_REV_FROM_FLAKE" != "$CHARON_REV_FROM_PIN" ]]; then - echo 'ERROR: The charon version in `flacke.lock` differs from the one in `charon-pin`.' - echo ' In `flake.lock`: '"$CHARON_REV_FROM_FLAKE" - echo ' In `charon-pin`: '"$CHARON_REV_FROM_PIN" - echo 'Use `make charon-pin` to update the `./charon-pin` file.' - exit 1 - fi - touch $out + check-charon-pin = pkgs.runCommand "aeneas-check-charon-pin" + { + buildInputs = [ pkgs.jq ]; + } '' + CHARON_REV_FROM_FLAKE="$(jq -r .nodes.charon.locked.rev ${./flake.lock})" + CHARON_REV_FROM_PIN="$(tail -1 ${./charon-pin})" + if [[ "$CHARON_REV_FROM_FLAKE" != "$CHARON_REV_FROM_PIN" ]]; then + echo 'ERROR: The charon version in `flacke.lock` differs from the one in `charon-pin`.' + echo ' In `flake.lock`: '"$CHARON_REV_FROM_FLAKE" + echo ' In `charon-pin`: '"$CHARON_REV_FROM_PIN" + echo 'Use `make charon-pin` to update the `./charon-pin` file.' + exit 1 + fi + touch $out ''; - in { + in + { packages = { inherit aeneas; default = aeneas; @@ -198,10 +201,11 @@ }; checks = { inherit aeneas aeneas-tests - aeneas-verify-fstar - aeneas-verify-coq - aeneas-verify-hol4 - aeneas-check-tidiness - check-charon-pin; }; + aeneas-verify-fstar + aeneas-verify-coq + aeneas-verify-hol4 + aeneas-check-tidiness + check-charon-pin; + }; }); } |