Merge pull request #169 from AeneasVerif/charon-pin

10 files changed, 146 insertions, 26 deletions

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/.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 414f562d..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
@@ -77,6 +77,30 @@ 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
+
+# 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
@@ -114,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..be5122b0 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
-```
-
-Finally, building the project simply requires to run `make` in the top
+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 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 running `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/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/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/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/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
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