From 0de27f0b88c12d210e840de0ad18eccf11b5ef1d Mon Sep 17 00:00:00 2001
From: Zyad Hassan
Date: Mon, 29 Jan 2024 16:21:25 -0800
Subject: Add instructions on using files generated by the Lean backend

---
 README.md | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3


From 4f619ca103e91d31ef18535e1d7a8e1f157206c3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 31 Jan 2024 16:14:03 +0100
Subject: Make a minor modification to the README

---
 README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index 82ff3944..0530a0da 100644
--- a/README.md
+++ b/README.md
@@ -83,9 +83,9 @@ to display a detailed documentation.
 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`:
+and add `Base` as a dependency in the `lakefile.lean`:
 ```
-require base from "PATH_TO_AENEAS_REPO/backends/lean"
+require Base from "PATH_TO_AENEAS_REPO/backends/lean"
 ```
 
 ## Targeted Subset And Current Limitations
-- 
cgit v1.2.3