From 621b8fff5dcd8ad481fd151c8e0fea6e7438d070 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 16 Apr 2024 11:41:21 +0200 Subject: Run sanity checks in CI only --- flake.nix | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) (limited to 'flake.nix') diff --git a/flake.nix b/flake.nix index b638d4ee..29960c9c 100644 --- a/flake.nix +++ b/flake.nix @@ -81,8 +81,9 @@ # 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 test-all -j $NIX_BUILD_CORES + # Run the tests with extra sanity checks enabled + # Remark: we could remove the file + OPTIONS=-checks make test-all -j $NIX_BUILD_CORES # Check that there are no differences between the generated tests # and the original tests @@ -153,10 +154,6 @@ default = aeneas; }; devShells.default = pkgs.mkShell { - # By default, tests run some sanity checks which are pretty slow. - # This disables these checks when developping locally. - OPTIONS = ""; - packages = [ pkgs.ocamlPackages.ocaml pkgs.ocamlPackages.ocamlformat -- cgit v1.2.3 From 75efc0213100f405fa64f3362e2fc4a73d09f61e Mon Sep 17 00:00:00 2001 From: Ryan Lahfa Date: Wed, 17 Apr 2024 14:25:55 +0200 Subject: feat(nix): support non-Flakes users Not all Nix users can make use of Flakes. This adds the compatibility for non-Flakes users. Signed-off-by: Ryan Lahfa --- flake.nix | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'flake.nix') diff --git a/flake.nix b/flake.nix index b638d4ee..5d5fae40 100644 --- a/flake.nix +++ b/flake.nix @@ -8,11 +8,12 @@ flake-utils.follows = "charon/flake-utils"; nixpkgs.follows = "charon/nixpkgs"; hacl-nix.url = "github:hacl-star/hacl-nix"; + flake-compat.url = "github:nix-community/flake-compat"; }; # Remark: keep the list of outputs in sync with the list of inputs above # (see above remark) - outputs = { self, charon, flake-utils, nixpkgs, hacl-nix }: + outputs = { self, charon, flake-utils, nixpkgs, hacl-nix, flake-compat }: flake-utils.lib.eachSystem [ "x86_64-linux" ] (system: let pkgs = import nixpkgs { inherit system; }; -- cgit v1.2.3 From cfda3a990cb3b24d91ce5bf8d1ddec7b265beca5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 16 Apr 2024 13:30:03 +0200 Subject: Ensure we regenerate files properly in CI Files that weren't regenerated were marked as not automatically-generated. --- flake.nix | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) (limited to 'flake.nix') diff --git a/flake.nix b/flake.nix index a436d773..f6a5f04e 100644 --- a/flake.nix +++ b/flake.nix @@ -75,23 +75,20 @@ export AENEAS_EXE=./aeneas # 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 with extra sanity checks enabled # Remark: we could remove the file + make clean-generated OPTIONS=-checks make test-all -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 + 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" + diff -ru tests tests-copy exit 1 fi ''; -- cgit v1.2.3 From 40e797fbf4d7bb47ef48597f25fda4e0b78633c7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 22 Apr 2024 11:55:55 +0200 Subject: ci: check code formatting --- flake.nix | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) (limited to 'flake.nix') diff --git a/flake.nix b/flake.nix index f6a5f04e..1ef810b7 100644 --- a/flake.nix +++ b/flake.nix @@ -30,6 +30,23 @@ }; buildInputs = [ ocamlPackages.calendar ]; }; + + aeneas-check-tidiness = pkgs.stdenv.mkDerivation { + name = "aeneas-check-tidiness"; + src = ./compiler; + buildInputs = [ + ocamlPackages.dune_3 + ocamlPackages.ocaml + ocamlPackages.ocamlformat + ]; + buildPhase = '' + if ! dune build @fmt; then + echo 'ERROR: Code is not fmrmatted. Run `make format` to format the project files'. + exit 1 + fi + ''; + installPhase = "touch $out"; + }; aeneas = ocamlPackages.buildDunePackage { pname = "aeneas"; version = "0.1.0"; @@ -167,6 +184,7 @@ inherit aeneas aeneas-tests aeneas-verify-fstar aeneas-verify-coq - aeneas-verify-hol4; }; + aeneas-verify-hol4 + aeneas-check-tidiness; }; }); } -- cgit v1.2.3 From 468377f078c5d01ec909f1927b329dec13dd46fd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 22 Apr 2024 13:15:42 +0200 Subject: ci: Forbid compilation warnings --- flake.nix | 1 + 1 file changed, 1 insertion(+) (limited to 'flake.nix') diff --git a/flake.nix b/flake.nix index 1ef810b7..5817ee33 100644 --- a/flake.nix +++ b/flake.nix @@ -52,6 +52,7 @@ version = "0.1.0"; duneVersion = "3"; src = ./compiler; + OCAMLPARAM="_,warn-error=+A"; # Turn all warnings into errors. propagatedBuildInputs = [ easy_logging charon.packages.${system}.charon-ml ] ++ (with ocamlPackages; [ -- cgit v1.2.3 From 10e5ca4c48c1d5729ee877612b7d95dfe2636159 Mon Sep 17 00:00:00 2001 From: Guillaume Boisseau Date: Tue, 23 Apr 2024 09:34:43 +0200 Subject: Typo Co-authored-by: Son HO --- flake.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'flake.nix') diff --git a/flake.nix b/flake.nix index 5817ee33..f77bd23b 100644 --- a/flake.nix +++ b/flake.nix @@ -41,7 +41,7 @@ ]; buildPhase = '' if ! dune build @fmt; then - echo 'ERROR: Code is not fmrmatted. Run `make format` to format the project files'. + echo 'ERROR: Code is not formatted. Run `make format` to format the project files'. exit 1 fi ''; -- cgit v1.2.3