diff options
| -rw-r--r-- | Makefile | 13 | ||||
| -rw-r--r-- | README.md | 2 | ||||
| -rw-r--r-- | compiler/Translate.ml | 8 | ||||
| -rw-r--r-- | flake.nix | 10 |
4 files changed, 24 insertions, 9 deletions
@@ -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 @@ -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 *) @@ -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 { |