-
Notifications
You must be signed in to change notification settings - Fork 9
Lurk Compilation Tutorial
- Install Rust
- Install the
lurkrs
binary- Clone the lurk-rs repo
- Checkout a compatible Lurk version:
git checkout 011bfc50128c18e35a711e4ebcb413d907515cd0
- Install with
cargo install --path .
- Make sure it's in the PATH by running
lurkrs
. If not, refresh the terminal or run the following:export PATH=$PATH:$HOME/.cargo/bin
- Clone the Yatima repo
-
Install Lean
Check it worked withelan show
andlake --version
. This will also ensure you are using the correct toolchain, specified by thelean-toolchain
file.
This will install the yatima
binary, compile the typechecker to Lurk, and store the relevant files on disk.
yatima ca /path/to/file
Ex:
yatima ca Fixtures/Debug/AddComm.lean
This will generate an environment file (out.env
by default) which stores the content-addressed Yatima IR.
yatima prove <decl> -e <env> -r
where decl
is the name of the Lean declaration to be typechecked and env
is the environment created in Step 3.
Ex:
yatima prove add_comm -e out.env -r
This should output some evaluation number (a proxy for performance) and a value. It will also create a .ldstore
Lurk store and .lurk
Lurk file corresponding to the input Lean program. Run yatima prove --help
for more options.
Due to the overhead of evaluating a program as large as a typechecker in Lurk, in most cases it is impractical to run compiled Lurk code in the lurk-rs
REPL with the yatima prove --rs
flag for the time being. Try running with -r
for the custom evaluator instead.
- Permissions denied on
yatima
binary
Find its location ($HOME/.local/bin by default) and runchmod +x yatima
-
yatima prove
hanging
See the performance notes and/or try running a smaller file