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 --- README.md | 28 +++++++++++++--------------- 1 file changed, 13 insertions(+), 15 deletions(-) (limited to 'README.md') 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 -- 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(-) (limited to 'README.md') 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