diff options
| -rw-r--r-- | README.md | 12 |
1 files changed, 11 insertions, 1 deletions
@@ -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 |