Add a `bin` folder

4 files changed, 24 insertions, 9 deletions

diff --git a/Makefile b/Makefile
index 7f1edf7a..47721ac5 100644
--- a/Makefile
+++ b/Makefile
@@ -21,11 +21,9 @@ CHARON_HOME ?= ../charon
 CHARON_TESTS_REGULAR_DIR ?= $(CHARON_HOME)/tests
 CHARON_TESTS_POLONIUS_DIR ?= $(CHARON_HOME)/tests-polonius
 
-AENEAS_DRIVER = driver.exe
-
 # 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)
+AENEAS_EXE ?= bin/aeneas.exe
 
 # The user can specify additional translation options for Aeneas.
 # By default we do:
@@ -54,7 +52,7 @@ build-tests-verify: build tests verify
 
 # Build the project
 .PHONY: build
-build: build-driver build-lib doc
+build: build-driver build-lib build-bin-dir doc
 
 .PHONY: build-driver
 build-driver:
@@ -64,6 +62,13 @@ build-driver:
 build-lib:
 	cd compiler && dune build aeneas.cmxs
 
+.PHONY: build-bin-dir
+build-bin-dir: build-driver build-lib
+	mkdir -p bin
+	cp -f compiler/_build/default/driver.exe bin/aeneas.exe
+	cp -f compiler/_build/default/driver.exe bin/aeneas.cmxs
+	cp -rf fstar bin
+
 .PHONY: doc
 doc:
 	cd compiler && dune build @doc
diff --git a/README.md b/README.md
index 6e60657d..e3a7e0e9 100644
--- a/README.md
+++ b/README.md
@@ -75,7 +75,7 @@ If you run `make`, you will generate a documentation accessible from [`doc.html`
 
 ## Usage
 
-The simplest way to run Aeneas is to execute `dune exec -- src/main.exe [OPTIONS] LLBC_FILE`,
+The Aeneas binary is in `bin`; you can run: `./bin/aeneas.exe [OPTIONS] LLBC_FILE`,
 where `LLBC_FILE` is an .llbc file generated by Charon.
 
 Aeneas provides a lot of flags and options to tweak its behaviour: you can use `--help`
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index c4185f41..959ea5ac 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -658,12 +658,14 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
     (* Create a directory with *default* permissions *)
     Core_unix.mkdir_p dest_dir);
 
-  (* Copy "Primitives.fst" - I couldn't find a "cp" function in the OCaml
-   * libraries... *)
+  (* Copy "Primitives.fst" *)
   let _ =
-    let src = open_in "fstar/Primitives.fst" in
+    (* Retrieve the executable's directory *)
+    let exe_dir = Filename.dirname Sys.argv.(0) in
+    let src = open_in (exe_dir ^ "/fstar/Primitives.fst") in
     let tgt_filename = Filename.concat dest_dir "Primitives.fst" in
     let tgt = open_out tgt_filename in
+    (* Very annoying: I couldn't find a "cp" function in the OCaml libraries... *)
     try
       while true do
         (* We copy line by line *)
diff --git a/flake.nix b/flake.nix
index a67e2e18..664cf1c2 100644
--- a/flake.nix
+++ b/flake.nix
@@ -54,12 +54,20 @@
               || pkgs.lib.hasPrefix (toString ./tests) path;
           };
           buildPhase = ''
+          # We need to provide the paths to the Charon tests derivations
           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
 
+          # Copy the Aeneas executable, and update the path to it
+          cp ${aeneas}/bin/aeneas_driver aeneas.exe
+          export AENEAS_EXE=./aeneas.exe
+
+          # Run the tests
           make tests
           '';
+          # Tests don't generate anything new as the generated files are
+          # versionned, but the installation phase still needs to prodocue
+          # something, otherwise Nix will consider the build has failed.
           installPhase = "touch $out";
         };
       in {