diff options
| -rw-r--r-- | Makefile | 10 | ||||
| -rw-r--r-- | backends/fstar/Primitives.fst (renamed from fstar/Primitives.fst) | 0 | ||||
| -rw-r--r-- | compiler/Translate.ml | 2 |
3 files changed, 8 insertions, 4 deletions
@@ -3,7 +3,11 @@ ifeq (3.81,$(MAKE_VERSION)) install make, then invoke gmake instead of make) endif -all: build +.PHONY: default +default: build + +.PHONY: all +all: build-test-verify nix #################################### # Variables customizable by the user @@ -67,7 +71,7 @@ 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 + cp -rf backends bin .PHONY: doc doc: @@ -87,7 +91,7 @@ tests: trans-no_nested_borrows trans-paper \ # Verify the F* files generated by the translation .PHONY: verify -verify: build tests +verify: cd tests && $(MAKE) all # Reformat the project diff --git a/fstar/Primitives.fst b/backends/fstar/Primitives.fst index 96138e46..96138e46 100644 --- a/fstar/Primitives.fst +++ b/backends/fstar/Primitives.fst diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 959ea5ac..dbf14e97 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -662,7 +662,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : let _ = (* 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 src = open_in (exe_dir ^ "/backends/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... *) |