From c184adf70c23fe2c0f3b0b727918ca32e94e673a Mon Sep 17 00:00:00 2001 From: Paul-Nicolas Madelaine Date: Mon, 23 Oct 2023 18:00:34 +0200 Subject: ci: hydra -> github runner --- flake.nix | 1 - 1 file changed, 1 deletion(-) (limited to 'flake.nix') diff --git a/flake.nix b/flake.nix index 4ff46046..ebe1e90d 100644 --- a/flake.nix +++ b/flake.nix @@ -169,6 +169,5 @@ default = aeneas; }; checks = { inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-coq aeneas-verify-lean aeneas-verify-hol4; }; - hydraJobs = { inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-coq aeneas-verify-lean aeneas-verify-hol4; }; }); } -- cgit v1.3.1 From d300be95c28ff3147bb6f6a65992df5b9b571bdf Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 10 Nov 2023 18:04:29 +0100 Subject: Check in nix that the regenerated files don't differ from the checked out files --- flake.nix | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) (limited to 'flake.nix') diff --git a/flake.nix b/flake.nix index ebe1e90d..e2b7a796 100644 --- a/flake.nix +++ b/flake.nix @@ -92,11 +92,28 @@ cp ${aeneas}/bin/aeneas_driver aeneas.exe export AENEAS_EXE=./aeneas.exe - # Run the tests + # Copy the tests + mkdir tests-copy + cp -r tests tests-copy + + # TODO: remove the test files to make sure we regenerate exactly + # the files which are checked out (we have to be careful about + # files like lakefile.lean, and the user hand-written files) + + # Run the tests - remark: we could remove the file make tests -j $NIX_BUILD_CORES + + # Check that there are no differences between the generated tests + # and the original tests + if [[ $(diff -rq tests tests-copy) ]]; then + echo "Ok: the regenerated test files are the same as the checked out files" + else + echo "Error: the regenerated test files differ from the checked out files" + exit 1 + fi ''; # Tests don't generate anything new as the generated files are - # versionned, but the installation phase still needs to prodocue + # versionned, but the installation phase still needs to produce # something, otherwise Nix will consider the build has failed. installPhase = "touch $out"; }; -- cgit v1.3.1 From d163bb804f3418ea8e2c89fe6e8d1c0587fd544b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 22 Nov 2023 14:52:15 +0100 Subject: Fix an issue with the nix flake and update the flake.lock --- compiler/dune | 2 +- flake.lock | 19 ++++++++++--------- flake.nix | 29 +++++++---------------------- 3 files changed, 18 insertions(+), 32 deletions(-) (limited to 'flake.nix') diff --git a/compiler/dune b/compiler/dune index 0d0a8017..3a40e086 100644 --- a/compiler/dune +++ b/compiler/dune @@ -1,6 +1,6 @@ (executable (name main) - (public_name aeneas_main) + (public_name aeneas) (package aeneas) (libraries aeneas) (modules Main)) diff --git a/flake.lock b/flake.lock index c85c619c..d32ac689 100644 --- a/flake.lock +++ b/flake.lock @@ -8,15 +8,16 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1700650378, - "narHash": "sha256-ZqQFeCsAySM13Qkj2Sz6eMTvw0HtNaq2cth/rfKHYUg=", + "lastModified": 1700660953, + "narHash": "sha256-vsMlaH7A5S7+uQGIYtu7Zt81s177X/xWbj2wdu54mtI=", "owner": "aeneasverif", "repo": "charon", - "rev": "aa0d5227d86f8d3a42b443424bf48c98ef8387cd", + "rev": "6760bf9d1dcf3314f2eb15999582d3b486cea6eb", "type": "github" }, "original": { "owner": "aeneasverif", + "ref": "son_fix_nix", "repo": "charon", "type": "github" } @@ -265,11 +266,11 @@ "nixpkgs": "nixpkgs_4" }, "locked": { - "lastModified": 1700591212, - "narHash": "sha256-87IXaQdBge+18Da7sd+mX39/g8Ibbqq7dGI/S+GByY4=", + "lastModified": 1700650599, + "narHash": "sha256-AK9AO8COmeBpBFmhM9YLrAz/S7XknokCdXLIDC7tfQc=", "owner": "leanprover", "repo": "lean4", - "rev": "fb30932ca7a88cb713e15e4557205dfff8a1a9da", + "rev": "9efdde23e0858f0925f0d3b4a6df842670b626c9", "type": "github" }, "original": { @@ -318,11 +319,11 @@ "nixpkgs": "nixpkgs_7" }, "locked": { - "lastModified": 1700591212, - "narHash": "sha256-87IXaQdBge+18Da7sd+mX39/g8Ibbqq7dGI/S+GByY4=", + "lastModified": 1700650599, + "narHash": "sha256-AK9AO8COmeBpBFmhM9YLrAz/S7XknokCdXLIDC7tfQc=", "owner": "leanprover", "repo": "lean4", - "rev": "fb30932ca7a88cb713e15e4557205dfff8a1a9da", + "rev": "9efdde23e0858f0925f0d3b4a6df842670b626c9", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index e2b7a796..8263174d 100644 --- a/flake.nix +++ b/flake.nix @@ -33,37 +33,22 @@ }; buildInputs = [ ocamlPackages.calendar ]; }; - ocamlgraph = ocamlPackages.buildDunePackage rec { - pname = "ocamlgraph"; - version = "2.0.0"; - src = pkgs.fetchurl { - url = "https://github.com/backtracking/ocamlgraph/releases/download/2.0.0/ocamlgraph-2.0.0.tbz"; - sha256 = "20fe267797de5322088a4dfb52389b2ea051787952a8a4f6ed70fcb697482609"; - }; - buildInputs = [ ocamlPackages.stdlib-shims ocamlPackages.graphics ]; - }; - unionFind = ocamlPackages.buildDunePackage rec { - pname = "unionFind"; - version = "20220122"; - src = pkgs.fetchurl { - url = "https://gitlab.inria.fr/fpottier/unionFind/-/archive/20220122/archive.tar.gz"; - sha512 = "c49dd3f9a6689f6a5efe39c26efe2c137f8812b4be6ee76c2cc20068cf86ad73c0ac97ec9a543245dddb63792ce8c1904576b3435bf419cc7837bc5e368eee6d"; - }; - buildInputs = []; - }; aeneas = ocamlPackages.buildDunePackage { pname = "aeneas"; version = "0.1.0"; duneVersion = "3"; src = ./compiler; - buildInputs = [ easy_logging ocamlgraph unionFind charon.packages.${system}.charon-ml ] - ++ (with ocamlPackages; [ + propagatedBuildInputs = [ + 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 @@ -89,8 +74,8 @@ export CHARON_TESTS_POLONIUS_DIR=${charon.checks.${system}.tests-polonius} # Copy the Aeneas executable, and update the path to it - cp ${aeneas}/bin/aeneas_driver aeneas.exe - export AENEAS_EXE=./aeneas.exe + cp ${aeneas}/bin/aeneas aeneas + export AENEAS_EXE=./aeneas # Copy the tests mkdir tests-copy -- cgit v1.3.1