LeanUI

Web user interfaces written in Lean 4. An app is a pure Elm-architecture program (a model, an update function and a view) whose views are ordinary Lean values, or JSX-style templates that compile to the same code. It runs in the browser as single-threaded wasm64, drives the DOM through a compact binary command buffer, and the same program renders on a native Lean server, which can also drive the page remotely for browsers without WebAssembly Memory64.

module
public import LeanUI
meta import LeanUI.Syntax          -- templates are compile-time only: zero runtime cost
public section
open LeanUI

inductive Msg | inc | dec

def view (n : Int) : Html Msg :=
  <p>
    <button onClick={.dec}>−</button>
    <output class={if n < 0 then "neg" else "pos"}>{n}</output>
    <button onClick={.inc}>+</button>
  </p>

def program : Program Int Msg where
  init _ := (0, .none)
  update msg n := (match msg with | .inc => n + 1 | .dec => n - 1, .none)
  view := view

What is in the box

Core (LeanUI.Html, Diff, Patch, App, Effect, Input)	views, keyed and positional reconciliation, exact lazy/memo subtrees, repeated subtrees created by cloning DOM templates, delegated events with browser-extracted payloads (values, keys, forms, files, pointers with capture, the wheel), commands (fetch, timers, storage, history, focus, title, animation frames, pixels to a canvas straight from wasm memory, file bytes and decoded images into Lean, downloads) and subscriptions (intervals, URL, keys), all as commands in one buffer per update
Templates (LeanUI.Syntax, docs/SYNTAX.md)	JSX-style syntax with components, fragments, conditional children, class/style parts, SVG and MathML namespaces, precise compile errors; the generated C equals the hand-written view's
Kit (LeanUI.Json, LeanUI.Router)	JSON on Init alone with exact numbers and deriving ToJson, FromJson; typed bidirectional routes (path or fragment) whose links cannot drift from the parser
Server (LeanUI.Server)	a native Std.Http server: static files, server-side rendering with hydration, server-driven sessions, the leanui command (serve, build, new)
Proofs (docs/PROOFS.md)	the keyed reconciliation planner is machine-checked correct and optimal (fewest moves); TodoMVC's model keeps its list keys unique under every message; the Roster app never shows an answer its proved checker did not accept
Testing (LeanUI.Testing)	a pure DOM model that applies command buffers exactly as the browser does, property tests and fuzzing against a reference model, a strict protocol checker, SSR parser checks, browser suites in Chromium and Firefox
Examples	a counter, TodoMVC (the full spec, proved invariants), the LeanUI site (routed pages, components, fetch, SVG; server-rendered), a photo editor (layers, filters, painting, PNG; every pixel in Lean), Roster (an untrusted solver whose answers a proved checker decides, rosters notarized by Lean's kernel and verified again in the browser), the js-framework-benchmark app, an effects lab, a pixels lab, the guide's notes app

How it works

An app is built twice from the same Lean code. Emscripten is used only at build time: the browser receives its output, never the compiler.

flowchart LR
  app["Your app in Lean<br/>model, update, view"]
  app -->|"lake"| c["C code"]
  c -->|"Emscripten, in Docker,<br/>at build time"| wasm["app.wasm + app.js<br/>the app as wasm64"]
  app -->|"lake, native"| server["Server binary<br/>optional"]
  rt["runtime/leanui.js<br/>about 6 KB, the same for every app"]
  wasm --> browser(("Browser"))
  rt --> browser
  server -.->|"serves pages and files"| browser

At run time, Lean does all the computing and a small fixed JavaScript runtime makes the DOM calls, because WebAssembly cannot reach the DOM directly. One page, from the first request to the user's clicks:

sequenceDiagram
  autonumber
  actor U as User
  participant B as Browser DOM
  participant J as leanui.js
  participant W as App in wasm (Lean)
  participant S as Lean server (native)

  B->>S: GET /examples
  S->>S: init and view run natively, Html.render
  S-->>B: complete HTML, visible before any script runs
  B->>J: load leanui.js, LeanUI.boot
  alt Browser has WebAssembly Memory64 (Chrome, Firefox)
    J->>W: load app.wasm, leanui_boot(flags, hydrate)
    W-->>J: command buffer: claim the existing nodes, attach listeners
    J->>B: adopt the server-rendered nodes (hydration)
    loop every interaction
      U->>B: click, type, submit
      B->>J: one delegated listener per event type
      J->>W: leanui_event(listener slot, payload)
      W->>W: update, view, diff
      W-->>J: command buffer, read in place from wasm memory
      J->>B: DOM calls: create or clone, set attribute, insert, remove
      opt the update asked for an effect, such as fetch
        J->>S: GET /data/benchmarks.json
        S-->>J: response
        J->>W: leanui_callback(id, ok, body)
      end
    end
  else No Memory64 (Safari): the server runs the same program
    J->>S: POST /leanui/session: h (hydrate)
    S->>S: a session starts the program natively
    S-->>J: command buffer
    J->>B: adopt the server-rendered nodes
    loop every interaction
      U->>B: click, type, submit
      B->>J: one delegated listener per event type
      J->>S: POST /leanui/session: e, listener slot, payload
      S->>S: update, view, diff
      S-->>J: command buffer
      J->>B: DOM calls
    end
  end

The server is optional. Served by any static file host (leanui serve), a page starts empty and the wasm mounts the app, with every interaction as in the first branch above.

This is the beginning of the README. Read the rest at the original. Read the full README ↗