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.

以上為 README 的開頭部分。其餘內容請閱讀原文。 檢視完整 README ↗