diff options
| -rw-r--r-- | .github/workflows/ci.yml | 6 | ||||
| -rw-r--r-- | Makefile | 91 | ||||
| -rw-r--r-- | README.md | 2 | ||||
| -rw-r--r-- | flake.nix | 3 |
4 files changed, 26 insertions, 76 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 0ccc74e0..4826114e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,7 +1,13 @@ on: + # Run the checks on any push to any branch of the repo that doesn't start with `_`. push: branches-ignore: [ '_**' ] + # Run the check for any pull request. The check is run on a merge between the + # PR commit and the `main` branch at the time of running the check. pull_request: + # Runs the check when a PR is added to the merge queue. + merge_group: + # Makes it possible to run the forkflow by hand from GItHub's interface. workflow_dispatch: # Minimum permissions required by skip-duplicate-actions @@ -20,11 +20,6 @@ REGEN_LLBC ?= # The path to Charon CHARON_HOME ?= ../charon -# The paths to the test directories in Charon (Aeneas will look for the .llbc -# files in there). -CHARON_TESTS_REGULAR_DIR ?= $(CHARON_HOME)/tests -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 @@ -36,7 +31,7 @@ OPTIONS ?= # The rules use (and update) the following variables # # The Charon test directory where to look for the .llbc files -CHARON_TEST_DIR = +CHARON_TEST_DIR ?= $(CHARON_HOME)/tests # The options with which to call Charon CHARON_OPTIONS = # The backend sub-directory in which to generate the files @@ -94,8 +89,8 @@ test: build-dev test-all test-all: test-no_nested_borrows test-paper \ test-hashmap test-hashmap_main \ test-external test-constants \ - test-polonius_list testp-betree_main \ - ctest-testp-betree_main \ + test-polonius_list test-betree_main \ + ctest-test-betree_main \ test-loops \ test-arrays test-traits test-bitwise test-demo @@ -220,97 +215,57 @@ thol4-bitwise: SUBDIR := misc-bitwise thol4-bitwise: OPTIONS += BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses -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 -tleanp-betree_main: SUBDIR := -tleanp-betree_main: OPTIONS += +test-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files +test-betree_main: SUBDIR:=betree +tfstar-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) +tcoq-betree_main: OPTIONS += -use-fuel +tlean-betree_main: SUBDIR := +tlean-betree_main: OPTIONS += thol4-betree_main: OPTIONS += # 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: ctest-testp-betree_main -ctest-testp-betree_main: testp-betree_main -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 -ctest-testp-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) -ctest-testp-betree_main: FILE = betree_main -ctest-testp-betree_main: +.PHONY: ctest-test-betree_main +ctest-test-betree_main: test-betree_main +ctest-test-betree_main: OPTIONS += -backend fstar -test-trans-units -state -split-files +ctest-test-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) +ctest-test-betree_main: BACKEND_SUBDIR := "fstar" +ctest-test-betree_main: SUBDIR:=betree_back_stateful +ctest-test-betree_main: FILE = betree_main +ctest-test-betree_main: $(AENEAS_CMD) # Generic rules to extract the LLBC from a rust file # We use the rules in Charon's Makefile to generate the .llbc files: the options # vary with the test files. .PHONY: gen-llbc-% -gen-llbc-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR) gen-llbc-%: $(CHARON_CMD) -# "p" stands for "Polonius" -.PHONY: gen-llbcp-% -gen-llbcp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) -gen-llbcp-%: - $(CHARON_CMD) - -# 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. +# Generic rules to test the translation of an LLBC file. .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: testp-% -testp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) -testp-%: FILE = $* -testp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-% - echo "# Test $* done" - .PHONY: tfstar-% tfstar-%: OPTIONS += -backend fstar tfstar-%: BACKEND_SUBDIR := fstar tfstar-%: $(AENEAS_CMD) -# "p" stands for "Polonius" -.PHONY: tfstarp-% -tfstarp-%: OPTIONS += -backend fstar -tfstarp-%: BACKEND_SUBDIR := fstar -tfstarp-%: - $(AENEAS_CMD) - .PHONY: tcoq-% tcoq-%: OPTIONS += -backend coq tcoq-%: BACKEND_SUBDIR := coq tcoq-%: $(AENEAS_CMD) -# "p" stands for "Polonius" -.PHONY: tcoqp-% -tcoqp-%: OPTIONS += -backend coq -tcoqp-%: BACKEND_SUBDIR := coq -tcoqp-%: - $(AENEAS_CMD) - .PHONY: tlean-% tlean-%: OPTIONS += -backend lean tlean-%: BACKEND_SUBDIR := lean tlean-%: $(AENEAS_CMD) -# "p" stands for "Polonius" -.PHONY: tleanp-% - -tleanp-%: OPTIONS += -backend lean -tleanp-%: BACKEND_SUBDIR := lean -tleanp-%: - $(AENEAS_CMD) - # TODO: reactivate HOL4 once traits are parameterized by their associated types .PHONY: thol4-% thol4-%: OPTIONS += -backend hol4 @@ -321,16 +276,6 @@ thol4-%: #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-%: - echo Ignoring the $* test for HOL4 - -#thol4p-%: -# $(AENEAS_CMD) - # Nix - TODO: add the lean tests .PHONY: nix nix: @@ -41,7 +41,7 @@ The dependencies can then be installed with the following command: ``` opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc \ - unionFind ocamlgraph + unionFind ocamlgraph menhir ocamlformat ``` Moreover, Aeneas requires the Charon ML library, defined in the @@ -85,8 +85,7 @@ }; 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 CHARON_TEST_DIR=${charon.checks.${system}.tests} # Copy the Aeneas executable, and update the path to it cp ${aeneas}/bin/aeneas aeneas |