Lean VIR

Lean VIR runs selected Lean 4 declarations in the browser through Lean's real IR interpreter compiled to wasm32-wasip1. It packages compiled module IR; it is not a general Lean-to-Wasm compiler.

VIR officially supports the runtime, package workflow, low-level object API and minimal two-way JS/Lean interop. DOM, React/JSX and editor/widget integrations are experimental conveniences, including when available through default imports. See support scope for the boundary, including the experimental JSON-safe codecs.

See CHANGES.md for release notes.

Try it

Open the hosted demos, including experimental React Tamagotchi and Format.pretty. No local Lean or Wasm build is needed to try the hosted site.

Use VIR in an application

After adding the lean_vir dependency to your Lake project, make three changes:

1. Mark the Lean functions JavaScript may call with @[vir_export].

   module
   meta import Vir.Attributes
   
   @[vir_export]
   public def QuickstartApp.Program.greet (name : String) : String :=
     "Hello, " ++ name

2. Create or reuse a resource library, separate from the program's library. In its resource module, include the program's assets:

   module
   public import Vir.Resources.Assets
   
   public def QuickstartApp.Resources.resources : Vir.Resources.ResourceSet :=
     include_vir_assets (modules := #[QuickstartApp.Program])

3. In lakefile.lean, register the modules and add needs to the resource library:

   lean_lib QuickstartProgram where
     roots := #[`QuickstartApp.Program]
   
   lean_lib QuickstartResources where
     roots := #[`QuickstartApp.Resources]
     needs := #[`+QuickstartApp.Program:virResourcePack]

Lake prepares the program before compiling the resource module and downloads the matching prebuilt interpreter. Your application writes resources.forSite's files with its normal asset writer; JavaScript calls program.call("QuickstartApp.Program.greet", "world"). No producer paths, packaging scripts or Wasm build are needed.

The runnable Quickstart supplies the complete dependency setup, publisher and browser page:

cd examples/tutorials/quickstart
lake exe publish _site
python3 -m http.server --directory _site 8000

Open http://localhost:8000/ to see Lean's greeting. The application setup guide explains these three changes and how to publish and call the program. Use the Lean toolchain selected by your VIR dependency; HTTPS runtime acquisition needs curl. See support scope for supported behavior and limitations.

Experimental

DOM helpers, React and JSX, and editor widgets and RPC are available to try outside the official support scope. Editor widgets use live environments, including unsaved code. Their presence in the library or demos does not extend the support promise.

Develop VIR

The default lake build builds the Lean library. To work on VIR itself:

npm install
npm run setup
npm run doctor

See CONTRIBUTING.md and the harness before running broader builds or tests. Ordinary client applications should not run this setup sequence.

Build internals documents the compiler, runtime distribution and repository tooling behind the application workflow. For custom JavaScript hosts and explicit object/host-binding APIs, see the runtime API reference and SDK acquisition.

Documentation links the API guides, implementation references, examples, and validation instructions.

License

Apache-2.0; see LICENSE and NOTICE. Generated Wasm can contain Lean 4 object code and retains its upstream notices.