Lurk Compilation Tutorial

Step 1. Install pre-requisites

• 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 with elan show and lake --version. This will also ensure you are using the correct toolchain, specified by the lean-toolchain file.

Step 2. Run the setup script with lake run setup

This will install the yatima binary, compile the typechecker to Lurk, and store the relevant files on disk.

Step 3. Content-address a given Lean file

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.

Step 4. Generate Lurk code for typechecking

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.

Performance Notes

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.

Troubleshooting

• Permissions denied on yatima binary
  Find its location ($HOME/.local/bin by default) and run chmod +x yatima
• yatima prove hanging
  See the performance notes and/or try running a smaller file