Lean VIR IR interpreter · WebAssembly

Experimental Lean 4 runtime

Lean VIR

Lean VIR packages selected executable Lean declarations as focused .irpkg files and runs them in the browser with Lean’s IR interpreter compiled to wasm32-wasip1.

This is a proof of concept for selected declarations, not a general browser target. Unsupported dependencies and JavaScript boundary types are reported during packaging.

01

Try Lean in the browser

Edit an array. Lean’s merge sort produces the result through VIR.

Ready

SortDemo.sortArray : Array Nat → Array Nat

02

Examples

Applications that show a reason to run Lean in a browser.

03

Use from a Lean project

Mark an export, build its package, and call it by Lean name.

  1. 1
    Mark@[vir_export]
  2. 2
    Buildlake build +MyApp:vir
  3. 3
    Callvir.call("MyApp.answer")

04

Inspect

Comparisons and reports generated alongside the runtime.