Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add instructions on using files generated by the Lean backend #67

Merged
merged 2 commits into from
Feb 1, 2024
Merged

Add instructions on using files generated by the Lean backend #67

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0de27f0
Add instructions on using files generated by the Lean backend
zhassan-aws Jan 30, 2024
4f619ca
Make a minor modification to the README
sonmarcho Jan 31, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 11 additions & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down