Lean VIR IR interpreter · WebAssembly

Lean 4 IR 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.

Official support covers the runtime, packages, object API and minimal JS/Lean interop. DOM, React/JSX and editor widgets are experimental conveniences.

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 a Lean function, publish its files, and call it from JavaScript.

  1. 1
    Mark@[vir_export]
  2. 2
    Publishlake exe publish _site
  3. 3
    Callprogram.call("QuickstartApp.Program.greet", "world")

04

Inspect

Comparisons and reports generated alongside the runtime.