From 61e0964d3deb0b964015b554be724c11bd07fda7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 2 May 2024 10:51:50 +0200 Subject: Update charon --- Makefile | 91 +++++++++++++------------------------------------------------- flake.lock | 7 ++--- flake.nix | 3 +-- 3 files changed, 23 insertions(+), 78 deletions(-) diff --git a/Makefile b/Makefile index f4bb8f9e..414f562d 100644 --- a/Makefile +++ b/Makefile @@ -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: diff --git a/flake.lock b/flake.lock index 014b0af1..e901898b 100644 --- a/flake.lock +++ b/flake.lock @@ -9,15 +9,16 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1714483898, - "narHash": "sha256-R9c3HgcKZQq6VF7ZBjidiJTtxB2mYNJYxctD1JI7As0=", + "lastModified": 1714656338, + "narHash": "sha256-+ksk7i8Kzm1V1rR/auH2EGlzGefPYgiuWMfAEH1Efjk=", "owner": "aeneasverif", "repo": "charon", - "rev": "eb48f4a62ce7c330d44c1e3c870b2a7271bba73b", + "rev": "c54e6dc374fd77b0da8328f34f17a5b44e8d6ed0", "type": "github" }, "original": { "owner": "aeneasverif", + "ref": "main", "repo": "charon", "type": "github" } diff --git a/flake.nix b/flake.nix index 6f868e3b..fd94d1d0 100644 --- a/flake.nix +++ b/flake.nix @@ -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 -- cgit v1.2.3 From 36a8151507356a8253a1bf244b213f297ab0220e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 2 May 2024 18:46:51 +0200 Subject: Update charon --- flake.lock | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/flake.lock b/flake.lock index e901898b..fd118ae3 100644 --- a/flake.lock +++ b/flake.lock @@ -9,16 +9,15 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1714656338, - "narHash": "sha256-+ksk7i8Kzm1V1rR/auH2EGlzGefPYgiuWMfAEH1Efjk=", + "lastModified": 1714668124, + "narHash": "sha256-66QkLemEGCWI+XnGYOA666XLMdrV5PU6Oew2B1fil+4=", "owner": "aeneasverif", "repo": "charon", - "rev": "c54e6dc374fd77b0da8328f34f17a5b44e8d6ed0", + "rev": "9d08aa01e4c2b94c24c7c79e47191d626a1a03b4", "type": "github" }, "original": { "owner": "aeneasverif", - "ref": "main", "repo": "charon", "type": "github" } -- cgit v1.2.3 From 4e8394f288ffec87c89a1c4238b3da859a906103 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 3 May 2024 15:11:48 +0200 Subject: Prepare CI for merge queue --- .github/workflows/ci.yml | 6 ++++++ 1 file changed, 6 insertions(+) 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 -- cgit v1.2.3 From 5dd789c4962efc698da6d3fd50f3a165720b2e42 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Mon, 6 May 2024 12:52:43 +0200 Subject: Add menhir and ocamlformat to list of required opam packages --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 74de4500..3775ad9c 100644 --- a/README.md +++ b/README.md @@ -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 -- cgit v1.2.3