summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorZyad Hassan2024-01-29 16:21:25 -0800
committerZyad Hassan2024-01-29 16:21:25 -0800
commit0de27f0b88c12d210e840de0ad18eccf11b5ef1d (patch)
tree80cc28a963f36613ba122ad347c0e22b0de37b8a
parent689954a5c84c29c9b86f02e5009f286d909c355c (diff)
Add instructions on using files generated by the Lean backend
Diffstat (limited to '')
-rw-r--r--README.md12
1 files changed, 11 insertions, 1 deletions
diff --git a/README.md b/README.md
index 64100410..82ff3944 100644
--- a/README.md
+++ b/README.md
@@ -72,12 +72,22 @@ If you run `make`, you will generate a documentation accessible from [`doc.html`
## Usage
-The Aeneas binary is in `bin`; you can run: `./bin/aeneas.exe [OPTIONS] LLBC_FILE`,
+The Aeneas binary is in `bin`; you can run: `./bin/aeneas -backend {fstar|coq|lean|hol4} [OPTIONS] LLBC_FILE`,
where `LLBC_FILE` is an .llbc file generated by Charon.
Aeneas provides a lot of flags and options to tweak its behaviour: you can use `--help`
to display a detailed documentation.
+### Additional Steps for Lean Backend
+
+Files generated by the Lean backend import the `Base` package from Aeneas.
+To use those files in Lean, create a new Lean package using `lake new`,
+overwrite the `lean-toolchain` with the one inside `./backends/lean`,
+and add `base` as a dependency in the `lakefile.lean`:
+```
+require base from "PATH_TO_AENEAS_REPO/backends/lean"
+```
+
## Targeted Subset And Current Limitations
We target **safe** Rust. This means we have no support for unsafe Rust, though we plan to