Make the Nix build work

5 files changed, 101 insertions, 33 deletions

diff --git a/Makefile b/Makefile
index 9f71079b..7f1edf7a 100644
--- a/Makefile
+++ b/Makefile
@@ -3,27 +3,51 @@ ifeq (3.81,$(MAKE_VERSION))
     install make, then invoke gmake instead of make)
 endif
 
-all: build-tests-verify
+all: build
 
-CHARON_HOME = ../charon
-DEST_DIR = tests
+####################################
+# Variables customizable by the user
+####################################
 
-# We use those variables, whose definition depends on the rule we apply
-CHARON_TESTS_DIR =
-CHARON_OPTIONS =
-CHARON_TESTS_SRC =
+# Set this variable to any value to call Charon to regenerate the .llbc source
+# files before running the tests
+REGEN_LLBC ?=
+
+# The path to Charon
+CHARON_HOME ?= ../charon
+
+# The paths to the test directories in Charon (Aeneas will look for the .llbc
+# files in there).
+CHARON_TESTS_REGULAR_DIR ?= $(CHARON_HOME)/tests
+CHARON_TESTS_POLONIUS_DIR ?= $(CHARON_HOME)/tests-polonius
 
 AENEAS_DRIVER = driver.exe
 
-# The user can specify additional translation options for Aeneas:
-OPTIONS += -unfold-monads
+# The path to the Aeneas executable to run the tests - we need the ability to
+# change this path for the Nix package.
+AENEAS_EXE ?= compiler/_build/default/$(AENEAS_DRIVER)
 
-# Default translation options:
+# The user can specify additional translation options for Aeneas.
+# By default we do:
+# - unfold all the monadic let bindings to matches (required by F*)
 # - insert calls to the normalizer in the translated code to test the
 #   generated unit functions
-TRANS_OPTIONS := -test-trans-units $(OPTIONS)
+OPTIONS += -unfold-monads -test-trans-units
+
+#
+# The rules use (and update) the following variables
+#
+# The Charon test directory where to look for the .llbc files
+CHARON_TEST_DIR =
+# The options with which to call Charon
+CHARON_OPTIONS =
+# The directory in which to extract the result of the translation
 SUBDIR :=
 
+####################################
+# The rules
+####################################
+
 # Build the project, test it and verify the generated files
 .PHONY: build-test-verify
 build-tests-verify: build tests verify
@@ -50,7 +74,7 @@ clean:
 
 # Test the project by translating test files to F*
 .PHONY: tests
-tests: build trans-no_nested_borrows trans-paper \
+tests: trans-no_nested_borrows trans-paper \
 	trans-hashmap trans-hashmap_main \
 	trans-external trans-constants \
 	trans-polonius-betree_polonius trans-polonius-betree_main \
@@ -67,41 +91,45 @@ format:
 	cd compiler && dune promote
 
 # The commands to run Charon to generate the .llbc files
-CHARON_CMD = cd $(CHARON_HOME)/$(CHARON_TEST_SUBFOLDER) && NOT_ALL_TESTS=1 $(MAKE) test-$*
+ifeq (, $(REGEN_LLBC))
+else
+CHARON_CMD = cd $(CHARON_TEST_DIR) && NOT_ALL_TESTS=1 $(MAKE) test-$*
+endif
 
 # The command to run Aeneas on the proper llbc file
-AENEAS_CMD = cd compiler && dune exec -- ./$(AENEAS_DRIVER) ../$(CHARON_TESTS_DIR)/$(FILE).llbc -dest ../$(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
+AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest ../tests/$(SUBDIR) $(OPTIONS)
+
 
 # Add specific options to some tests
 trans-no_nested_borrows trans-paper: \
-	TRANS_OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses
+	OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses
 trans-no_nested_borrows trans-paper: SUBDIR:=misc
 
-trans-hashmap: TRANS_OPTIONS += -template-clauses -no-state
+trans-hashmap: OPTIONS += -template-clauses -no-state
 trans-hashmap: SUBDIR:=hashmap
 
-trans-hashmap_main: TRANS_OPTIONS += -template-clauses
+trans-hashmap_main: OPTIONS += -template-clauses
 trans-hashmap_main: SUBDIR:=hashmap_on_disk
 
-trans-polonius-betree_polonius: TRANS_OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses
+trans-polonius-betree_polonius: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses
 trans-polonius-betree_polonius: SUBDIR:=misc
 
-trans-constants: TRANS_OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses
+trans-constants: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses
 trans-constants: SUBDIR:=misc
 
-trans-external: TRANS_OPTIONS +=
+trans-external: OPTIONS +=
 trans-external: SUBDIR:=misc
 
 BETREE_OPTIONS = -template-clauses
-trans-polonius-betree_main: TRANS_OPTIONS += $(BETREE_OPTIONS) -backward-no-state-update
+trans-polonius-betree_main: OPTIONS += $(BETREE_OPTIONS) -backward-no-state-update
 trans-polonius-betree_main: SUBDIR:=betree
 
 # Additional test on the betree: translate it without `-backward-no-state-update`.
 # This generates very ugly code, but is good to test the translation.
 test-trans-polonius-betree_main: trans-polonius-betree_main
-test-trans-polonius-betree_main: TRANS_OPTIONS += $(BETREE_OPTIONS)
+test-trans-polonius-betree_main: OPTIONS += $(BETREE_OPTIONS)
 test-trans-polonius-betree_main: SUBDIR:=betree_back_stateful
-test-trans-polonius-betree_main: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc
+test-trans-polonius-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
 test-trans-polonius-betree_main: FILE = betree_main
 test-trans-polonius-betree_main:
 	$(AENEAS_CMD)
@@ -110,21 +138,22 @@ test-trans-polonius-betree_main:
 # We use the rules in Charon's Makefile to generate the .llbc files: the options
 # vary with the test files.
 .PHONY: gen-llbc-polonius-%
-gen-llbc-polonius-%: CHARON_TEST_SUBFOLDER = tests-polonius
-gen-llbc-polonius-%: build
+gen-llbc-polonius-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
+gen-llbc-polonius-%:
 	$(CHARON_CMD)
 
 .PHONY: gen-llbc-%
-gen-llbc-%: CHARON_TEST_SUBFOLDER = tests
-gen-llbc-%: build
+gen-llbc-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
+gen-llbc-%:
 	$(CHARON_CMD)
 
 # Generic rule to test the translation of an LLBC file.
 # Note that the files requiring the Polonius borrow-checker are generated
 # in the tests-polonius subdirectory.
 .PHONY: trans-%
-trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc
-trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc
+trans-%:
+trans-polonius-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
+trans-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
 
 trans-polonius-%: FILE = $*
 trans-polonius-%: gen-llbc-polonius-%
@@ -133,3 +162,8 @@ trans-polonius-%: gen-llbc-polonius-%
 trans-%: FILE = $*
 trans-%: gen-llbc-%
 	$(AENEAS_CMD)
+
+# Nix
+.PHONY: nix
+nix:
+	nix build .#checks.x86_64-linux.aeneas-tests --show-trace -L
diff --git a/README.md b/README.md
index f3c8a480..6e60657d 100644
--- a/README.md
+++ b/README.md
@@ -63,6 +63,12 @@ if [ -e charon ]; then echo "valid"; else echo "invalid"; fi
 Finally, building the project simply requires to run `make` in the top
 directory.
 
+You can also use `make tests` and `make verify` to run the tests, and check
+the generated files. As `make tests` will run tests which use the Charon tests,
+you will need to regenerate the `.llbc` files. You have the following options:
+- run `make tests` in the Charon repository
+- run `REGEN_LLBC=1 make tests` in the Aeneas repository
+
 ## Documentation
 
 If you run `make`, you will generate a documentation accessible from [`doc.html`](./doc.html).
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index 304d0f2f..3059ec2f 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -140,17 +140,18 @@ let () =
   pure_micro_passes_log#set_level EL.Info;
   pure_to_extract_log#set_level EL.Info;
   translate_log#set_level EL.Info;
+  let log = main_log in
 
   (* Load the module *)
   let json = Yojson.Basic.from_file filename in
   match crate_of_json json with
   | Error s ->
-      main_log#error "error: %s\n" s;
+      log#error "error: %s\n" s;
       exit 1
   | Ok m ->
       (* Logging *)
-      main_log#linfo (lazy ("Imported: " ^ filename));
-      main_log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n"));
+      log#linfo (lazy ("Imported: " ^ filename));
+      log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n"));
 
       (* Apply the pre-passes *)
       let m = PrePasses.apply_passes m in
diff --git a/flake.nix b/flake.nix
index 712bc604..a67e2e18 100644
--- a/flake.nix
+++ b/flake.nix
@@ -26,7 +26,7 @@
         aeneas = ocamlPackages.buildDunePackage {
           pname = "aeneas";
           version = "0.1.0";
-          src = ./.;
+          src = ./compiler;
           buildInputs = [ easy_logging charon.packages.${system}.charon-ml ]
             ++ (with ocamlPackages; [
               calendar
@@ -36,11 +36,38 @@
               yojson
               zarith
             ]);
+          afterBuild = ''
+          echo charon.packages.${system}.tests
+          '';
+        };
+        # Make sure we don't need to recompile the package whenever we make
+        # unnecessary changes - we list the exact files and folders the package
+        # depends upon.
+        aeneas-tests = pkgs.stdenv.mkDerivation {
+          name = "aeneas_tests";
+          src = pkgs.lib.cleanSourceWith {
+            src = ./.;
+            filter = path: type:
+              path == toString ./Makefile
+              || pkgs.lib.hasPrefix (toString ./compiler) path
+              || pkgs.lib.hasPrefix (toString ./fstar) path
+              || pkgs.lib.hasPrefix (toString ./tests) path;
+          };
+          buildPhase = ''
+          export CHARON_TESTS_REGULAR_DIR=${charon.checks.${system}.tests}
+          export CHARON_TESTS_POLONIUS_DIR=${charon.checks.${system}.tests-polonius}
+          export AENEAS_EXE=${aeneas}/bin/aeneas_driver
+
+          make tests
+          '';
+          installPhase = "touch $out";
         };
       in {
         packages = {
           inherit aeneas;
           default = aeneas;
         };
+        checks = { inherit aeneas aeneas-tests; };
+        hydraJobs = { inherit aeneas aeneas-tests; };
       });
 }
diff --git a/compiler/fstar/Primitives.fst b/fstar/Primitives.fst
index 96138e46..96138e46 100644
--- a/compiler/fstar/Primitives.fst
+++ b/fstar/Primitives.fst