Installation
Recommended: the installation should only take a few minutes:
- Clone this repo
- Install Visual Studio Code Warning: VS Codium doesn't work for this tutorial (people who tried had issues with the Lean4 extension).
- Install the Lean 4 extension (warning: do not confuse it with the Lean 3 extension)
- Open this folder inside of VS Code (
File
>Open folder
) - Open the file
Tutorial/Exercises.lean
(by using the explorer on the left) - Wait for Lean to download and build the project dependencies.
You may have to click on the
Restart file
button (on the bottom right)
If you do not want to use VS Code, you can directly install
Lean, then run lake build
and finally open
the file Tutorial/Exercises.lean
.
Zulip
If you have questions, do not hesitate to join the Zulip!
Generating the .lean files
In order to minimize the setup time, we will not install Charon and Aeneas during this session, which means we will not regenerate the .lean files. If you want to regenerate the .lean files, do the following:
- Clone the repos:
git clone git@github.com:AeneasVerif/aeneas.git
git clone git@github.com:AeneasVerif/charon.git
- Build the projects (see their READMEs to get the list of dependencies):
cd aeneas && make
cd charon && make
- Goto the
icfp-tutorial
repo and create symbolic links to the Charon and Aeneas clones. For instance:
cd icfp-tutorial
ln -s ../aeneas aeneas
ln -s ../charon charon
- Run
make
Note: make
will simply run the following commands:
- We first need to call Charon to retrieve the AST of the program.
The following command generates the
tutorial.llbc
file, which contains the LLBC of the program (LLBC is a cleaned up version of MIR, one of the intermediate languages used by the Rust compiler - Charon links itself to the Rust compiler to retrieve this AST):cd source && ../charon/bin/charon --hide-marker-traits --dest ../
- Then, we need to call Aeneas to actually perform the translation to Lean:
aeneas/bin/aeneas -backend lean tutorial.llbc