From fcbb06f1b32c42b42d6bde501a4bc29a661ec23b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 3 Aug 2023 00:24:09 +0200 Subject: Update the Makefile to add the array test --- Makefile | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 1b11592f..8865746d 100644 --- a/Makefile +++ b/Makefile @@ -90,7 +90,8 @@ tests: trans-no_nested_borrows trans-paper \ trans-external trans-constants \ transp-polonius_list transp-betree_main \ test-transp-betree_main \ - trans-loops + trans-loops \ + trans-array # TODO: generalize to all backends # Verify the F* files generated by the translation .PHONY: verify @@ -122,6 +123,20 @@ 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 +tfstar-array: OPTIONS += +tcoq-array: OPTIONS += +tlean-array: SUBDIR := +tlean-array: OPTIONS += +thol4-array: OPTIONS += + +# TODO: activate the arrays for all the backends +tcoq-array: + echo "Ignoring the array test for Coq" +thol4-array: + echo "Ignoring the array test for HOL4" + trans-loops: OPTIONS += -no-state trans-loops: SUBDIR := misc tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -- cgit v1.2.3 From 5e38184af1b99a307271f738329cd96cb364fc1d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 4 Aug 2023 22:31:48 +0200 Subject: Update the Makefile and regenerate the test files --- Makefile | 28 +++++++++++++--------------- 1 file changed, 13 insertions(+), 15 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 8865746d..c94544be 100644 --- a/Makefile +++ b/Makefile @@ -125,15 +125,13 @@ thol4-paper: SUBDIR := misc-paper trans-array: OPTIONS += -no-state trans-array: SUBDIR := array -tfstar-array: OPTIONS += -tcoq-array: OPTIONS += +tfstar-array: OPTIONS += -decreases-clauses -template-clauses +tcoq-array: OPTIONS += -use-fuel tlean-array: SUBDIR := tlean-array: OPTIONS += thol4-array: OPTIONS += # TODO: activate the arrays for all the backends -tcoq-array: - echo "Ignoring the array test for Coq" thol4-array: echo "Ignoring the array test for HOL4" @@ -144,7 +142,7 @@ tcoq-loops: OPTIONS += -use-fuel -no-split-files tlean-loops: SUBDIR := thol4-loops: SUBDIR := misc-loops -trans-hashmap: OPTIONS += -no-state +trans-hashmap: OPTIONS += -no-state -test-trans-units trans-hashmap: SUBDIR := hashmap tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap: OPTIONS += -use-fuel @@ -152,7 +150,7 @@ tlean-hashmap: SUBDIR := tlean-hashmap: OPTIONS += thol4-hashmap: OPTIONS += -trans-hashmap_main: OPTIONS += +trans-hashmap_main: OPTIONS += -test-trans-units trans-hashmap_main: SUBDIR := hashmap_on_disk tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap_main: OPTIONS += -use-fuel @@ -177,7 +175,7 @@ tlean-constants: OPTIONS += thol4-constants: SUBDIR := misc-constants thol4-constants: OPTIONS += -trans-external: OPTIONS += +trans-external: OPTIONS += -test-trans-units trans-external: SUBDIR := misc tfstar-external: OPTIONS += tcoq-external: OPTIONS += @@ -187,7 +185,7 @@ thol4-external: SUBDIR := misc-external thol4-external: OPTIONS += BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses -transp-betree_main: OPTIONS += -backward-no-state-update +transp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units transp-betree_main: SUBDIR:=betree tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) tcoqp-betree_main: OPTIONS += -use-fuel @@ -239,20 +237,20 @@ transp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-% echo "# Test $* done" .PHONY: tfstar-% -tfstar-%: OPTIONS += -backend fstar -test-trans-units +tfstar-%: OPTIONS += -backend fstar tfstar-%: BACKEND_SUBDIR := fstar tfstar-%: $(AENEAS_CMD) # "p" stands for "Polonius" .PHONY: tfstarp-% -tfstarp-%: OPTIONS += -backend fstar -test-trans-units +tfstarp-%: OPTIONS += -backend fstar tfstarp-%: BACKEND_SUBDIR := fstar tfstarp-%: $(AENEAS_CMD) .PHONY: tcoq-% -tcoq-%: OPTIONS += -backend coq -test-trans-units +tcoq-%: OPTIONS += -backend coq tcoq-%: BACKEND_SUBDIR := coq tcoq-%: $(AENEAS_CMD) @@ -265,7 +263,7 @@ tcoqp-%: $(AENEAS_CMD) .PHONY: tlean-% -tlean-%: OPTIONS += -backend lean -test-trans-units +tlean-%: OPTIONS += -backend lean tlean-%: BACKEND_SUBDIR := lean tlean-%: $(AENEAS_CMD) @@ -273,19 +271,19 @@ tlean-%: # "p" stands for "Polonius" .PHONY: tleanp-% -tleanp-%: OPTIONS += -backend lean -test-trans-units +tleanp-%: OPTIONS += -backend lean tleanp-%: BACKEND_SUBDIR := lean tleanp-%: $(AENEAS_CMD) .PHONY: thol4-% -thol4-%: OPTIONS += -backend hol4 -test-trans-units +thol4-%: OPTIONS += -backend hol4 thol4-%: BACKEND_SUBDIR := hol4 thol4-%: $(AENEAS_CMD) .PHONY: thol4p-% -thol4p-%: OPTIONS += -backend hol4 -test-trans-units +thol4p-%: OPTIONS += -backend hol4 thol4p-%: BACKEND_SUBDIR := hol4 thol4p-%: $(AENEAS_CMD) -- cgit v1.2.3 From cb603d47be46a6957ec16b9bc68176694542e99a Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 4 Aug 2023 22:46:48 +0200 Subject: Add an option to not override Hashmap.lean --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index c94544be..a0111b37 100644 --- a/Makefile +++ b/Makefile @@ -147,7 +147,7 @@ trans-hashmap: SUBDIR := hashmap tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap: OPTIONS += -use-fuel tlean-hashmap: SUBDIR := -tlean-hashmap: OPTIONS += +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 -- cgit v1.2.3