summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRyan Lahfa2024-04-18 14:26:59 +0200
committerGuillaume Boisseau2024-05-29 10:44:47 +0200
commit2d8310261ac4d19bd441de271505a0f0004028b8 (patch)
tree7064753272d96417482ec5ce512061a3782270f6
parente9d124d80f781521a817da9784084d66788c7b3c (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 '')
-rw-r--r--README.md19
-rw-r--r--flake.nix1
2 files changed, 20 insertions, 0 deletions
diff --git a/README.md b/README.md
index 82f1da55..76d1720f 100644
--- a/README.md
+++ b/README.md
@@ -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
diff --git a/flake.nix b/flake.nix
index 3e8b88de..cb3f84ea 100644
--- a/flake.nix
+++ b/flake.nix
@@ -217,6 +217,7 @@
{
packages = {
inherit aeneas;
+ inherit (charon.packages.${system}) charon-ml charon;
default = aeneas;
};
devShells.default = pkgs.mkShell {