Run sanity checks in CI only

2 files changed, 4 insertions, 8 deletions

diff --git a/Makefile b/Makefile
index 0f3e2999..0299d134 100644
--- a/Makefile
+++ b/Makefile
@@ -31,9 +31,8 @@ AENEAS_EXE ?= bin/aeneas
 
 # The user can specify additional translation options for Aeneas.
 # By default we activate the (expensive) sanity checks.
-OPTIONS ?= -checks
+OPTIONS ?=
 
-#
 # The rules use (and update) the following variables
 #
 # The Charon test directory where to look for the .llbc files
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