Skip to content

Commit

Permalink
chore: explain a Nix-powered workflow
Browse files Browse the repository at this point in the history
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>
  • Loading branch information
Ryan Lahfa authored and Nadrieril committed May 29, 2024
1 parent e9d124d commit 2d83102
Show file tree
Hide file tree
Showing 2 changed files with 20 additions and 0 deletions.
19 changes: 19 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions flake.nix
Original file line number Diff line number Diff line change
Expand Up @@ -217,6 +217,7 @@
{
packages = {
inherit aeneas;
inherit (charon.packages.${system}) charon-ml charon;
default = aeneas;
};
devShells.default = pkgs.mkShell {
Expand Down

0 comments on commit 2d83102

Please sign in to comment.