diff options
| author | Ryan Lahfa | 2024-04-18 14:26:59 +0200 |
|---|---|---|
| committer | Guillaume Boisseau | 2024-05-29 10:44:47 +0200 |
| commit | 2d8310261ac4d19bd441de271505a0f0004028b8 (patch) | |
| tree | 7064753272d96417482ec5ce512061a3782270f6 /README.md | |
| parent | e9d124d80f781521a817da9784084d66788c7b3c (diff) | |
chore: explain a Nix-powered workflow
To avoid divergence between Charon and Aeneas, we should re-export
Charon via our Flake and tell users to use this as a source of truth.
Here's an appendix on how I do refresh of my files, which can serve as
inspiration for a quick start workflow.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 19 |
1 files changed, 19 insertions, 0 deletions
@@ -116,6 +116,25 @@ and tactics specialized for monadic programs (see A tutorial for the Lean backend is available [here](./tests/lean/Tutorial.lean). +## Quick start for Nix users + +Assuming Nix is installed, with a support for Flakes (`*`): + +```console +$ # Run Charon with the exact same version required by Aeneas +$ nix run github:aeneasverif/aeneas#charon -L +$ nix run github:aeneasverif/aeneas -L -- -backend your_preferred_backend your_llbc.file +``` + +To regenerate the extraction, just run step 2 and step 3 again. + +`(*)` : Flakes are not necessary, here is an example of how to do similar steps without it: + +```console +$ nix-shell '<aeneas>' -A packages.x86_64-linux.charon --run "charon" -I aeneas=https://github.com/AeneasVerif/aeneas/archive/main.tar.gz +$ nix-shell '<aeneas>' -A packages.x86_64-linux.default --run "aeneas --backend your_preferred_backend your_llbc.file" -I aeneas=https://github.com/AeneasVerif/aeneas/archive/main.tar.gz +``` + ## Formalization The translation has been formalized and published at ICFP2022: [Aeneas: Rust |