From 3151e373d64f9bce6146a44cd2d3cc64cac84cbf Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 4 Sep 2023 00:59:39 +0200 Subject: Fix minor issues --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index a0111b37..807352f8 100644 --- a/Makefile +++ b/Makefile @@ -166,7 +166,7 @@ tleanp-polonius_list: OPTIONS += thol4p-polonius_list: SUBDIR := misc-polonius_list thol4p-polonius_list: OPTIONS += -trans-constants: OPTIONS += -test-units -test-trans-units -no-split-files -no-state +trans-constants: OPTIONS += -test-trans-units -no-split-files -no-state trans-constants: SUBDIR := misc tfstar-constants: OPTIONS += tcoq-constants: OPTIONS += -- cgit v1.2.3 From a2183bf48773d078a9372847f1715fd38b84819d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 24 Oct 2023 11:15:33 +0200 Subject: Deactivate the concrete interpreter tests --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 807352f8..2c996345 100644 --- a/Makefile +++ b/Makefile @@ -115,7 +115,7 @@ AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BA # Add specific options to some tests trans-no_nested_borrows trans-paper: \ - OPTIONS += -test-units -test-trans-units -no-split-files -no-state + OPTIONS += -test-trans-units -no-split-files -no-state trans-no_nested_borrows trans-paper: SUBDIR := misc tfstar-no_nested_borrows tfstar-paper: tlean-no_nested_borrows: SUBDIR := @@ -157,7 +157,7 @@ tcoq-hashmap_main: OPTIONS += -use-fuel tlean-hashmap_main: SUBDIR := thol4-hashmap_main: OPTIONS += -transp-polonius_list: OPTIONS += -test-units -test-trans-units -no-split-files -no-state +transp-polonius_list: OPTIONS += -test-trans-units -no-split-files -no-state transp-polonius_list: SUBDIR := misc tfstarp-polonius_list: OPTIONS += tcoqp-polonius_list: OPTIONS += -- cgit v1.2.3 From 81b7a7d706bc1a0f2f57bc254a8af158039a10cf Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 25 Oct 2023 18:44:28 +0200 Subject: Make the hashmap files typecheck again in Lean --- Makefile | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 2c996345..958ae8d7 100644 --- a/Makefile +++ b/Makefile @@ -142,7 +142,8 @@ tcoq-loops: OPTIONS += -use-fuel -no-split-files tlean-loops: SUBDIR := thol4-loops: SUBDIR := misc-loops -trans-hashmap: OPTIONS += -no-state -test-trans-units +# TODO: reactivate -test-trans-units +trans-hashmap: OPTIONS += -no-state trans-hashmap: SUBDIR := hashmap tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap: OPTIONS += -use-fuel @@ -150,7 +151,8 @@ tlean-hashmap: SUBDIR := tlean-hashmap: OPTIONS += -no-gen-lib-entry # We add a custom import in the Hashmap.lean file: we do not want to overwrite it thol4-hashmap: OPTIONS += -trans-hashmap_main: OPTIONS += -test-trans-units +# TODO: reactivate -test-trans-units +trans-hashmap_main: OPTIONS += trans-hashmap_main: SUBDIR := hashmap_on_disk tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap_main: OPTIONS += -use-fuel -- cgit v1.2.3 From 4ba7d73fa3bfbf9ef41b2d9d5595f28fb67b8e47 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 6 Nov 2023 18:11:24 +0100 Subject: Update following some changes in Charon --- Makefile | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 958ae8d7..694b47a3 100644 --- a/Makefile +++ b/Makefile @@ -91,7 +91,7 @@ tests: trans-no_nested_borrows trans-paper \ transp-polonius_list transp-betree_main \ test-transp-betree_main \ trans-loops \ - trans-array # TODO: generalize to all backends + trans-array trans-traits # TODO: generalize to all backends # Verify the F* files generated by the translation .PHONY: verify @@ -131,6 +131,14 @@ tlean-array: SUBDIR := tlean-array: OPTIONS += thol4-array: OPTIONS += +trans-traits: OPTIONS += -no-state +trans-traits: SUBDIR := traits +tfstar-traits: OPTIONS += -decreases-clauses -template-clauses +tcoq-traits: OPTIONS += -use-fuel +tlean-traits: SUBDIR := +tlean-traits: OPTIONS += +thol4-traits: OPTIONS += + # TODO: activate the arrays for all the backends thol4-array: echo "Ignoring the array test for HOL4" -- cgit v1.2.3 From 530a5ae56209061f091bbcafee82de07039a8124 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 8 Nov 2023 14:28:44 +0100 Subject: Update the Makefile and regenerate some tests --- Makefile | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 694b47a3..486ba40e 100644 --- a/Makefile +++ b/Makefile @@ -143,6 +143,10 @@ thol4-traits: OPTIONS += thol4-array: echo "Ignoring the array test for HOL4" +# TODO: activate the traits for all the backends +thol4-traits: + echo "Ignoring the traits test for HOL4" + trans-loops: OPTIONS += -no-state trans-loops: SUBDIR := misc tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -- cgit v1.2.3 From 9754c65c76cc48f9d3feab410dfe18273ae08c05 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 9 Nov 2023 11:24:56 +0100 Subject: Update the Makefile to rename the "trans-" rules to "test-" --- Makefile | 92 ++++++++++++++++++++++++++++++++-------------------------------- 1 file changed, 46 insertions(+), 46 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 486ba40e..bdabe878 100644 --- a/Makefile +++ b/Makefile @@ -85,13 +85,13 @@ clean: # Test the project by translating test files to F* .PHONY: tests -tests: trans-no_nested_borrows trans-paper \ - trans-hashmap trans-hashmap_main \ - trans-external trans-constants \ - transp-polonius_list transp-betree_main \ - test-transp-betree_main \ - trans-loops \ - trans-array trans-traits # TODO: generalize to all backends +tests: test-no_nested_borrows test-paper \ + test-hashmap test-hashmap_main \ + test-external test-constants \ + testp-polonius_list testp-betree_main \ + ctest-testp-betree_main \ + test-loops \ + test-array test-traits # TODO: generalize to all backends # Verify the F* files generated by the translation .PHONY: verify @@ -114,25 +114,25 @@ AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BA # Add specific options to some tests -trans-no_nested_borrows trans-paper: \ +test-no_nested_borrows test-paper: \ OPTIONS += -test-trans-units -no-split-files -no-state -trans-no_nested_borrows trans-paper: SUBDIR := misc +test-no_nested_borrows test-paper: SUBDIR := misc tfstar-no_nested_borrows tfstar-paper: tlean-no_nested_borrows: SUBDIR := tlean-paper: SUBDIR := thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows thol4-paper: SUBDIR := misc-paper -trans-array: OPTIONS += -no-state -trans-array: SUBDIR := array +test-array: OPTIONS += -no-state +test-array: SUBDIR := array tfstar-array: OPTIONS += -decreases-clauses -template-clauses tcoq-array: OPTIONS += -use-fuel tlean-array: SUBDIR := tlean-array: OPTIONS += thol4-array: OPTIONS += -trans-traits: OPTIONS += -no-state -trans-traits: SUBDIR := traits +test-traits: OPTIONS += -no-state +test-traits: SUBDIR := traits tfstar-traits: OPTIONS += -decreases-clauses -template-clauses tcoq-traits: OPTIONS += -use-fuel tlean-traits: SUBDIR := @@ -147,16 +147,16 @@ thol4-array: thol4-traits: echo "Ignoring the traits test for HOL4" -trans-loops: OPTIONS += -no-state -trans-loops: SUBDIR := misc +test-loops: OPTIONS += -no-state +test-loops: SUBDIR := misc tfstar-loops: OPTIONS += -decreases-clauses -template-clauses tcoq-loops: OPTIONS += -use-fuel -no-split-files tlean-loops: SUBDIR := thol4-loops: SUBDIR := misc-loops # TODO: reactivate -test-trans-units -trans-hashmap: OPTIONS += -no-state -trans-hashmap: SUBDIR := hashmap +test-hashmap: OPTIONS += -no-state +test-hashmap: SUBDIR := hashmap tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap: OPTIONS += -use-fuel tlean-hashmap: SUBDIR := @@ -164,15 +164,15 @@ tlean-hashmap: OPTIONS += -no-gen-lib-entry # We add a custom import in the Hash thol4-hashmap: OPTIONS += # TODO: reactivate -test-trans-units -trans-hashmap_main: OPTIONS += -trans-hashmap_main: SUBDIR := hashmap_on_disk +test-hashmap_main: OPTIONS += +test-hashmap_main: SUBDIR := hashmap_on_disk tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap_main: OPTIONS += -use-fuel tlean-hashmap_main: SUBDIR := thol4-hashmap_main: OPTIONS += -transp-polonius_list: OPTIONS += -test-trans-units -no-split-files -no-state -transp-polonius_list: SUBDIR := misc +testp-polonius_list: OPTIONS += -test-trans-units -no-split-files -no-state +testp-polonius_list: SUBDIR := misc tfstarp-polonius_list: OPTIONS += tcoqp-polonius_list: OPTIONS += tleanp-polonius_list: SUBDIR := @@ -180,8 +180,8 @@ tleanp-polonius_list: OPTIONS += thol4p-polonius_list: SUBDIR := misc-polonius_list thol4p-polonius_list: OPTIONS += -trans-constants: OPTIONS += -test-trans-units -no-split-files -no-state -trans-constants: SUBDIR := misc +test-constants: OPTIONS += -test-trans-units -no-split-files -no-state +test-constants: SUBDIR := misc tfstar-constants: OPTIONS += tcoq-constants: OPTIONS += tlean-constants: SUBDIR := @@ -189,8 +189,8 @@ tlean-constants: OPTIONS += thol4-constants: SUBDIR := misc-constants thol4-constants: OPTIONS += -trans-external: OPTIONS += -test-trans-units -trans-external: SUBDIR := misc +test-external: OPTIONS += -test-trans-units +test-external: SUBDIR := misc tfstar-external: OPTIONS += tcoq-external: OPTIONS += tlean-external: SUBDIR := @@ -199,25 +199,25 @@ thol4-external: SUBDIR := misc-external thol4-external: OPTIONS += BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses -transp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -transp-betree_main: SUBDIR:=betree +testp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units +testp-betree_main: SUBDIR:=betree tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) tcoqp-betree_main: OPTIONS += -use-fuel tleanp-betree_main: SUBDIR := tleanp-betree_main: OPTIONS += thol4-betree_main: OPTIONS += -# Additional test on the betree: translate it without `-backward-no-state-update`. +# Additional, *c*ustom test on the betree: translate it without `-backward-no-state-update`. # This generates very ugly code, but is good to test the translation. -.PHONY: test-transp-betree_main -test-transp-betree_main: transp-betree_main -test-transp-betree_main: OPTIONS += -backend fstar -test-trans-units -test-transp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) -test-transp-betree_main: BACKEND_SUBDIR := "fstar" -test-transp-betree_main: SUBDIR:=betree_back_stateful -test-transp-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) -test-transp-betree_main: FILE = betree_main -test-transp-betree_main: +.PHONY: ctest-testp-betree_main +ctest-testp-betree_main: testp-betree_main +ctest-testp-betree_main: OPTIONS += -backend fstar -test-trans-units +ctest-testp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) +ctest-testp-betree_main: BACKEND_SUBDIR := "fstar" +ctest-testp-betree_main: SUBDIR:=betree_back_stateful +ctest-testp-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) +ctest-testp-betree_main: FILE = betree_main +ctest-testp-betree_main: $(AENEAS_CMD) # Generic rules to extract the LLBC from a rust file @@ -234,20 +234,20 @@ gen-llbcp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) gen-llbcp-%: $(CHARON_CMD) -# Generic rules to test the translation of an LLBC file. +# Generic rules to test the testlation of an LLBC file. # Note that the files requiring the Polonius borrow-checker are generated # in the tests-polonius subdirectory. -.PHONY: trans-% -trans-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR) -trans-%: FILE = $* -trans-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-% +.PHONY: test-% +test-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR) +test-%: FILE = $* +test-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-% echo "# Test $* done" # "p" stands for "Polonius" -.PHONY: transp-% -transp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) -transp-%: FILE = $* -transp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-% +.PHONY: testp-% +testp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) +testp-%: FILE = $* +testp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-% echo "# Test $* done" .PHONY: tfstar-% -- cgit v1.2.3 From c57dec640d4e12c3dc66969d626bbbca2eb733fd Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 9 Nov 2023 11:43:47 +0100 Subject: Modify some options and update the Makefile --- Makefile | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index bdabe878..19992442 100644 --- a/Makefile +++ b/Makefile @@ -115,7 +115,7 @@ AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BA # Add specific options to some tests test-no_nested_borrows test-paper: \ - OPTIONS += -test-trans-units -no-split-files -no-state + OPTIONS += -test-trans-units test-no_nested_borrows test-paper: SUBDIR := misc tfstar-no_nested_borrows tfstar-paper: tlean-no_nested_borrows: SUBDIR := @@ -123,7 +123,7 @@ tlean-paper: SUBDIR := thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows thol4-paper: SUBDIR := misc-paper -test-array: OPTIONS += -no-state +test-array: OPTIONS += test-array: SUBDIR := array tfstar-array: OPTIONS += -decreases-clauses -template-clauses tcoq-array: OPTIONS += -use-fuel @@ -131,7 +131,7 @@ tlean-array: SUBDIR := tlean-array: OPTIONS += thol4-array: OPTIONS += -test-traits: OPTIONS += -no-state +test-traits: OPTIONS += test-traits: SUBDIR := traits tfstar-traits: OPTIONS += -decreases-clauses -template-clauses tcoq-traits: OPTIONS += -use-fuel @@ -147,15 +147,15 @@ thol4-array: thol4-traits: echo "Ignoring the traits test for HOL4" -test-loops: OPTIONS += -no-state +test-loops: OPTIONS += test-loops: SUBDIR := misc -tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -tcoq-loops: OPTIONS += -use-fuel -no-split-files +tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -split-files +tcoq-loops: OPTIONS += -use-fuel tlean-loops: SUBDIR := thol4-loops: SUBDIR := misc-loops # TODO: reactivate -test-trans-units -test-hashmap: OPTIONS += -no-state +test-hashmap: OPTIONS += -split-files test-hashmap: SUBDIR := hashmap tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap: OPTIONS += -use-fuel @@ -164,14 +164,14 @@ tlean-hashmap: OPTIONS += -no-gen-lib-entry # We add a custom import in the Hash thol4-hashmap: OPTIONS += # TODO: reactivate -test-trans-units -test-hashmap_main: OPTIONS += +test-hashmap_main: OPTIONS += -state -split-files test-hashmap_main: SUBDIR := hashmap_on_disk tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap_main: OPTIONS += -use-fuel tlean-hashmap_main: SUBDIR := thol4-hashmap_main: OPTIONS += -testp-polonius_list: OPTIONS += -test-trans-units -no-split-files -no-state +testp-polonius_list: OPTIONS += -test-trans-units testp-polonius_list: SUBDIR := misc tfstarp-polonius_list: OPTIONS += tcoqp-polonius_list: OPTIONS += @@ -180,7 +180,7 @@ tleanp-polonius_list: OPTIONS += thol4p-polonius_list: SUBDIR := misc-polonius_list thol4p-polonius_list: OPTIONS += -test-constants: OPTIONS += -test-trans-units -no-split-files -no-state +test-constants: OPTIONS += -test-trans-units test-constants: SUBDIR := misc tfstar-constants: OPTIONS += tcoq-constants: OPTIONS += @@ -189,7 +189,7 @@ tlean-constants: OPTIONS += thol4-constants: SUBDIR := misc-constants thol4-constants: OPTIONS += -test-external: OPTIONS += -test-trans-units +test-external: OPTIONS += -test-trans-units -state -split-files test-external: SUBDIR := misc tfstar-external: OPTIONS += tcoq-external: OPTIONS += @@ -199,7 +199,7 @@ thol4-external: SUBDIR := misc-external thol4-external: OPTIONS += BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses -testp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units +testp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files testp-betree_main: SUBDIR:=betree tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) tcoqp-betree_main: OPTIONS += -use-fuel @@ -211,7 +211,7 @@ thol4-betree_main: OPTIONS += # This generates very ugly code, but is good to test the translation. .PHONY: ctest-testp-betree_main ctest-testp-betree_main: testp-betree_main -ctest-testp-betree_main: OPTIONS += -backend fstar -test-trans-units +ctest-testp-betree_main: OPTIONS += -backend fstar -test-trans-units -state -split-files ctest-testp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) ctest-testp-betree_main: BACKEND_SUBDIR := "fstar" ctest-testp-betree_main: SUBDIR:=betree_back_stateful -- cgit v1.2.3 From 7853ddf29773d42d41df7a915e1d19c9cfd98ac7 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 9 Nov 2023 13:52:31 +0100 Subject: Update the Makefile for the F* array test --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 19992442..78ddb87c 100644 --- a/Makefile +++ b/Makefile @@ -125,7 +125,7 @@ thol4-paper: SUBDIR := misc-paper test-array: OPTIONS += test-array: SUBDIR := array -tfstar-array: OPTIONS += -decreases-clauses -template-clauses +tfstar-array: OPTIONS += -decreases-clauses -template-clauses -split-files tcoq-array: OPTIONS += -use-fuel tlean-array: SUBDIR := tlean-array: OPTIONS += -- cgit v1.2.3 From 9157959cc421c481cf584ada69f51d58da82e8f9 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 9 Nov 2023 14:22:06 +0100 Subject: Deactivate the HOL4 tests --- Makefile | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 78ddb87c..b67bd08b 100644 --- a/Makefile +++ b/Makefile @@ -290,17 +290,25 @@ tleanp-%: BACKEND_SUBDIR := lean tleanp-%: $(AENEAS_CMD) +# TODO: reactivate HOL4 once traits are parameterized by their associated types .PHONY: thol4-% thol4-%: OPTIONS += -backend hol4 thol4-%: BACKEND_SUBDIR := hol4 thol4-%: - $(AENEAS_CMD) + echo Ignoring the $* test for HOL4 + +#thol4-%: +# $(AENEAS_CMD) +# TODO: reactivate HOL4 once traits are parameterized by their associated types .PHONY: thol4p-% thol4p-%: OPTIONS += -backend hol4 thol4p-%: BACKEND_SUBDIR := hol4 thol4p-%: - $(AENEAS_CMD) + echo Ignoring the $* test for HOL4 + +#thol4p-%: +# $(AENEAS_CMD) # Nix - TODO: add the lean tests .PHONY: nix -- cgit v1.2.3 From 3a22c56e026ee4488bc5e2d16d2066853ae7ccb9 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 9 Nov 2023 16:22:09 +0100 Subject: Make the traits work for Coq --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index b67bd08b..427a5751 100644 --- a/Makefile +++ b/Makefile @@ -134,7 +134,7 @@ thol4-array: OPTIONS += test-traits: OPTIONS += test-traits: SUBDIR := traits tfstar-traits: OPTIONS += -decreases-clauses -template-clauses -tcoq-traits: OPTIONS += -use-fuel +tcoq-traits: OPTIONS += tlean-traits: SUBDIR := tlean-traits: OPTIONS += thol4-traits: OPTIONS += -- cgit v1.2.3 From cc61ce2217339f24a8cc8951ee15abc5fd90b47b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 9 Nov 2023 18:51:43 +0100 Subject: Update the rule build-bin-dir in the Makefile --- Makefile | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 427a5751..4660ac83 100644 --- a/Makefile +++ b/Makefile @@ -27,7 +27,7 @@ CHARON_TESTS_POLONIUS_DIR ?= $(CHARON_HOME)/tests-polonius # The path to the Aeneas executable to run the tests - we need the ability to # change this path for the Nix package. -AENEAS_EXE ?= bin/aeneas.exe +AENEAS_EXE ?= bin/aeneas # The user can specify additional translation options for Aeneas. # By default we do: @@ -71,9 +71,12 @@ build-lib: .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 cp -f compiler/_build/default/driver.exe bin/aeneas.cmxs - cp -rf backends bin + mkdir -p bin/backends/fstar + mkdir -p bin/backends/coq + cp -rf backends/fstar/*.fst* bin/backends/fstar/ + cp -rf backends/coq/*.v bin/backends/coq/ .PHONY: doc doc: -- cgit v1.2.3