Lean 4 ( Rust Backend )

Fork of Lean 4.27.0 with an experimental bytecode compiler targeting a Rust VM.

Building

make -j -C build/release

Bytecode Compilation

Use the -Y flag to emit bytecode:

export LEAN_PATH="$(pwd)/build/release/stage1/lib/lean"
./build/release/stage1/bin/lean -Y output.leanbc input.lean

Lake Integration

Set backend := .vm in your lakefile:

@[default_target]
lean_exe myapp where
  root := `Main
  backend := .vm

Then lake build produces .leanbc files in .lake/build/ir/.

Running Bytecode

Use lean4-vm to execute bytecode:

lean4-vm program.leanbc
lean4-vm -L ./bc/ program.leanbc  # Load dependencies from directory

Environment Variables

Variable	Description
LEAN_PATH	Search path for .olean files during compilation

License

Apache 2.0