Ensure `./charon` points to a valid charon clone

6 files changed, 103 insertions, 20 deletions

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