From f2fa29e5ef5c8c7d7375e4c8a37dbba1012fb95c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 3 May 2024 11:32:44 +0200 Subject: `./charon-pin` stores the current charon commit It is kept up-to-date in CI --- .github/workflows/ci.yml | 1 + Makefile | 11 +++++++++++ charon-pin | 2 ++ flake.nix | 24 ++++++++++++++++++++---- scripts/update-charon-pin.sh | 7 +++++++ 5 files changed, 41 insertions(+), 4 deletions(-) create mode 100644 charon-pin create mode 100755 scripts/update-charon-pin.sh diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4826114e..eeb423b6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -36,6 +36,7 @@ jobs: steps: - uses: actions/checkout@v4 - run: nix build -L .#checks.x86_64-linux.aeneas-check-tidiness + - run: nix build -L .#checks.x86_64-linux.check-charon-pin - run: nix build -L .#aeneas - run: nix build -L .#checks.x86_64-linux.aeneas-tests - run: nix build -L .#checks.x86_64-linux.aeneas-verify-fstar diff --git a/Makefile b/Makefile index 414f562d..cf97e548 100644 --- a/Makefile +++ b/Makefile @@ -77,6 +77,17 @@ build-bin-dir: build-bin build-lib doc: cd compiler && dune build @doc +# Fetches the latest commit from charon and updates `flake.lock` accordingly. +.PHONY: update-charon-pin +update-charon-pin: + nix flake lock --update-input charon + $(MAKE) charon-pin + +# Keep the commit revision in `./charon-pin` as well so that non-nix users can +# know which commit to use. +./charon-pin: flake.lock + nix-shell -p jq --run './scripts/update-charon-pin.sh' >> ./charon-pin + .PHONY: clean clean: clean-generated cd compiler && dune clean diff --git a/charon-pin b/charon-pin new file mode 100644 index 00000000..d2e70db4 --- /dev/null +++ b/charon-pin @@ -0,0 +1,2 @@ +# This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. +1a205c55b02f3dff1ae238dfdac5a58d58de6006 diff --git a/flake.nix b/flake.nix index fd94d1d0..13b8795e 100644 --- a/flake.nix +++ b/flake.nix @@ -2,8 +2,8 @@ description = "Aeneas"; inputs = { - # Remark: when adding inputs here, don't forget to also add them in the list - # of outputs below! + # Remark: when adding inputs here, don't forget to also add them in the + # arguments to `outputs` below! charon.url = "github:aeneasverif/charon"; flake-utils.follows = "charon/flake-utils"; nixpkgs.follows = "charon/nixpkgs"; @@ -41,7 +41,7 @@ ]; buildPhase = '' if ! dune build @fmt; then - echo 'ERROR: Code is not formatted. Run `make format` to format the project files'. + echo 'ERROR: Code is not formatted. Run `make format` to format the project files.' exit 1 fi ''; @@ -163,6 +163,21 @@ # The build doesn't generate anything installPhase = "touch $out"; }; + + check-charon-pin = pkgs.runCommand "aeneas-check-charon-pin" { + buildInputs = [ pkgs.jq ]; + } '' + CHARON_REV_FROM_FLAKE="$(jq -r .nodes.charon.locked.rev ${./flake.lock})" + CHARON_REV_FROM_PIN="$(tail -1 ${./charon-pin})" + if [[ "$CHARON_REV_FROM_FLAKE" != "$CHARON_REV_FROM_PIN" ]]; then + echo 'ERROR: The charon version in `flacke.lock` differs from the one in `charon-pin`.' + echo ' In `flake.lock`: '"$CHARON_REV_FROM_FLAKE" + echo ' In `charon-pin`: '"$CHARON_REV_FROM_PIN" + echo 'Use `make charon-pin` to update the `./charon-pin` file.' + exit 1 + fi + touch $out + ''; in { packages = { inherit aeneas; @@ -186,6 +201,7 @@ aeneas-verify-fstar aeneas-verify-coq aeneas-verify-hol4 - aeneas-check-tidiness; }; + aeneas-check-tidiness + check-charon-pin; }; }); } diff --git a/scripts/update-charon-pin.sh b/scripts/update-charon-pin.sh new file mode 100755 index 00000000..418602b8 --- /dev/null +++ b/scripts/update-charon-pin.sh @@ -0,0 +1,7 @@ +#!/usr/bin/env bash +if ! which jq 2> /dev/null 1>&2; then + echo 'Error: command `jq` not found.' + exit 1 +fi +echo '# This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.' > ./charon-pin +jq -r .nodes.charon.locked.rev flake.lock >> ./charon-pin -- cgit v1.2.3 From b923f7232a9e98a0b039b722ffedcf91051edbe6 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 3 May 2024 13:29:27 +0200 Subject: Ensure `./charon` points to a valid charon clone --- .gitignore | 3 ++ Makefile | 21 ++++++++++--- README.md | 28 ++++++++--------- compiler/.gitignore | 1 - compiler/charon | 1 + scripts/check-charon-install.sh | 69 +++++++++++++++++++++++++++++++++++++++++ 6 files changed, 103 insertions(+), 20 deletions(-) delete mode 100644 compiler/.gitignore create mode 120000 compiler/charon create mode 100755 scripts/check-charon-install.sh diff --git a/.gitignore b/.gitignore index 36809c43..7703c3fd 100644 --- a/.gitignore +++ b/.gitignore @@ -15,6 +15,9 @@ _build/ *.byte *.native +# Charon installation +/charon + # We group everything here bin diff --git a/Makefile b/Makefile index cf97e548..3b3e3e64 100644 --- a/Makefile +++ b/Makefile @@ -18,7 +18,7 @@ all: build-tests-verify nix REGEN_LLBC ?= # The path to Charon -CHARON_HOME ?= ../charon +CHARON_HOME ?= ./charon # The path to the Aeneas executable to run the tests - we need the ability to # change this path for the Nix package. @@ -56,11 +56,11 @@ build-test-verify: build test verify build-dev: build-bin build-lib build-bin-dir doc .PHONY: build-bin -build-bin: +build-bin: check-charon cd compiler && dune build .PHONY: build-lib -build-lib: +build-lib: check-charon cd compiler && dune build aeneas.cmxs .PHONY: build-bin-dir @@ -88,6 +88,19 @@ update-charon-pin: ./charon-pin: flake.lock nix-shell -p jq --run './scripts/update-charon-pin.sh' >> ./charon-pin +# Checks that `./charon` contains a clone of charon at the required commit. +# Also checks that `./charon/bin/charon` exists. +.PHONY: check-charon +check-charon: charon-pin + @echo "Checking the charon installation" + @./scripts/check-charon-install.sh + +# Sets up the charon repository on the right commit. +.PHONY: setup-charon +setup-charon: + @./scripts/check-charon-install.sh --force + + .PHONY: clean clean: clean-generated cd compiler && dune clean @@ -125,7 +138,7 @@ format: # The commands to run Charon to generate the .llbc files ifeq (, $(REGEN_LLBC)) else -CHARON_CMD = cd $(CHARON_TEST_DIR) && NOT_ALL_TESTS=1 $(MAKE) test-$* +CHARON_CMD = cd $(CHARON_TEST_DIR) && $(MAKE) test-$* endif # The command to run Aeneas on the proper llbc file diff --git a/README.md b/README.md index 3775ad9c..afb5bcbc 100644 --- a/README.md +++ b/README.md @@ -44,27 +44,25 @@ opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc \ unionFind ocamlgraph menhir ocamlformat ``` -Moreover, Aeneas requires the Charon ML library, defined in the -[Charon](https://github.com/AeneasVerif/charon) project. -The simplest way is to clone Charon, then go to [`compiler`](./compiler) and -create a symbolic link to the Charon library: -`cd AENEAS_REPO/compiler && ln -s PATH_TO_CHARON_REPO/charon-ml charon` -(the symbolic link should be placed inside the `aeneas/compiler/` folder). - -**Remark:** if you want to test if the symbolic link is valid, copy-paste the -following script in your terminal (from the `compiler` directory): -```bash -if [ -e charon ]; then echo "valid"; else echo "invalid"; fi -``` +Moreover, Aeneas uses the [Charon](https://github.com/AeneasVerif/charon) project and library. +For Aeneas to work, `./charon` must contain a clone of the [Charon](https://github.com/AeneasVerif/charon) +repository, at the commit specified in `./charon-pin`. The easiest way to set this up is to call +`make setup-charon` +(this uses [rustup](https://rustup.rs/) or [nix](https://nixos.org/download/) to build Charon). +In case of version mismatch, the various `make` scripts will instruct you to update. + +If you're also developing on Charon, you can instead set up `./charon` to be a symlink to your local version: +`ln -s PATH_TO_CHARON_REPO charon`. In this case, the scripts will not check that your Charon +installation is on a compatible commit. When you pull a new version of Aeneas, you will occasionally +need to update your Charon repository so that Aeneas builds and runs correctly. Finally, building the project simply requires to run `make` in the top directory. You can also use `make test` and `make verify` to run the tests, and check the generated files. As `make test` will run tests which use the Charon tests, -you will need to regenerate the `.llbc` files. You have the following options: -- run `make test` in the Charon repository -- run `make test` in the Aeneas repository +you will need to regenerate the `.llbc` files. To do this, run `make setup-charon` before `make +test`. Alternatively, call `REGEN_LLBC=1 make test-...` to regenerate only the needed files. ## Documentation diff --git a/compiler/.gitignore b/compiler/.gitignore deleted file mode 100644 index 8357dae7..00000000 --- a/compiler/.gitignore +++ /dev/null @@ -1 +0,0 @@ -charon diff --git a/compiler/charon b/compiler/charon new file mode 120000 index 00000000..0cd9e85a --- /dev/null +++ b/compiler/charon @@ -0,0 +1 @@ +../charon/charon-ml/ \ No newline at end of file diff --git a/scripts/check-charon-install.sh b/scripts/check-charon-install.sh new file mode 100755 index 00000000..4f7a79d7 --- /dev/null +++ b/scripts/check-charon-install.sh @@ -0,0 +1,69 @@ +#!/usr/bin/env bash +# This script checks that `./charon` contains a correctly set-up charon. Pass `--force` to execute the suggested commands. + +FORCE= +if [[ "$1" == "--force" ]]; then + FORCE=1 +fi + +rebuild() { + if which rustup 2> /dev/null 1>&2; then + make test + elif which nix 2> /dev/null 1>&2; then + nix develop --command bash -c "make test" + else + echo 'Error: Neither `rustup` nor `nix` appears to be installed. Install one or the other in order to build `charon`.' + exit 1 + fi +} + +PINNED_COMMIT="$(tail -1 charon-pin)" +if [ ! -e ./charon ]; then + if [[ "$FORCE" == "1" ]]; then + git clone https://github.com/AeneasVerif/charon + cd charon && git checkout "$PINNED_COMMIT" && rebuild + exit 0 + else + echo 'Error: `charon` not found. Please clone the charon repository into `./charon` at the commit specified '\ + 'in `./charon-pin`, or make a symlink to an existing clone of charon:' + echo ' $ git clone https://github.com/AeneasVerif/charon' + echo ' $ cd charon && git checkout '"$PINNED_COMMIT"' && make test' + echo 'To do this automatically, run `make setup-charon`.' + exit 1 + fi +fi + +# If charon is a symlink, we assume it's a working copy so we won't check +# commit hashes. +CHARON_IS_SYMLINK= +if [ -L charon ]; then + echo 'Warning: `./charon` is a symlink; we assume it is a working copy and will not check commit hashes.' + CHARON_IS_SYMLINK=1 +fi + +cd charon + +ACTUAL_COMMIT="$(git rev-parse HEAD)" +if [[ "$CHARON_IS_SYMLINK" != "1" && "$ACTUAL_COMMIT" != "$PINNED_COMMIT" ]]; then + if [[ "$FORCE" == "1" ]]; then + git checkout "$PINNED_COMMIT" && rebuild + exit 0 + else + echo 'Error: `charon` commit is not the pinned commit. Update the charon repository to the commit specified in `./charon-pin`:' + echo ' $ cd charon && git checkout '"$PINNED_COMMIT"' && make test' + echo 'To do this automatically, run `make setup-charon`.' + exit 1 + fi +fi + +if [[ "$FORCE" == "1" ]]; then + rebuild + exit 0 +else + if [ ! -f bin/charon ]; then + echo 'Error: `./bin/charon` not found. The charon binary is needed to run aeneas tests; please build it:' + echo ' $ cd charon && make test' + echo 'To do this automatically, run `make setup-charon`.' + exit 1 + fi +fi -- cgit v1.2.3 From 50f5794587c56be833bd2fc0f48d008a46fc69a0 Mon Sep 17 00:00:00 2001 From: Guillaume Boisseau Date: Tue, 14 May 2024 14:49:56 +0200 Subject: Tweak wording Co-authored-by: Son HO --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index afb5bcbc..be5122b0 100644 --- a/README.md +++ b/README.md @@ -48,15 +48,15 @@ Moreover, Aeneas uses the [Charon](https://github.com/AeneasVerif/charon) projec For Aeneas to work, `./charon` must contain a clone of the [Charon](https://github.com/AeneasVerif/charon) repository, at the commit specified in `./charon-pin`. The easiest way to set this up is to call `make setup-charon` -(this uses [rustup](https://rustup.rs/) or [nix](https://nixos.org/download/) to build Charon). -In case of version mismatch, the various `make` scripts will instruct you to update. +(this uses either [rustup](https://rustup.rs/) or [nix](https://nixos.org/download/) to build Charon, depending on which one is installed). +In case of version mismatch, you will be instructed to update Charon. If you're also developing on Charon, you can instead set up `./charon` to be a symlink to your local version: `ln -s PATH_TO_CHARON_REPO charon`. In this case, the scripts will not check that your Charon installation is on a compatible commit. When you pull a new version of Aeneas, you will occasionally need to update your Charon repository so that Aeneas builds and runs correctly. -Finally, building the project simply requires to run `make` in the top +Finally, building the project simply requires running `make` in the top directory. You can also use `make test` and `make verify` to run the tests, and check -- cgit v1.2.3