Lasm 0.3.0

Lasm 0.3.0

Lasm compiles ordinary Lean 4.35.0 programs ahead of time to WebAssembly. This is
the launch release. 0.3.0 adds:

• browser apps in Lean, with a UI framework whose DOM diff is proved correct;
• full-stack apps: one Lean project for the server, the browser and the API
  between them;
• pure-WebAssembly hosts: WASI, wasi-http/Spin and Fastly Compute;
• a pure-Lean HTTP handler that runs on every server target;
• a Fastify template;
• a faster edit loop and a faster cold start;
• editor support for Lasm's own libraries.

Upgrade with npm install -D @lasm/cli@0.3.0, or start a new project with
npm create @lasm@latest my-app -- --template fullstack (or web, fetch,
fastify, hono, …).

What's new

• Browser apps. lasm build Main.lean --target browser writes dist/, a
  static site:

  • an ES-module loader of a few KiB and the Wasm, with content hashes and
    precompressed .br/.gz copies;
  • index.html and lasm-manifest.json.

  Mount the app with mount(element, { flags, hydrate }), or let it mount itself
  on <div data-lasm-app>. It runs in Chrome, Edge, Firefox and Safari.

  • Vite: import lasm from '@lasm/cli/vite', then
    import app from './Main.lean?lasm'. The plugin rebuilds on save and
    hot-reloads; it ships inside @lasm/cli.
  • Template: --template web (a counter).

• Lasm.Web: typed bindings for the web platform: DOM nodes and events,
  fetch, timers, requestAnimationFrame, storage, history and location, URL,
  FormData, WebSocket, crypto, console and basic canvas 2D.

• Lasm.UI: a framework in the Elm architecture:

  • a pure update and view, commands, subscriptions and routing;
  • JSX-like html! markup whose tags and attributes are checked while Lean
    elaborates;
  • server-side rendering (Html.render) and hydration;
  • ports to JavaScript.

  The diff runs in Lean, and one binary patch per frame crosses to a small
  JavaScript applier. The diff is proved correct: applying the patch it
  computes to a model of the DOM gives exactly the new view, keyed moves included
  (Lasm.UI.Proofs.diff_correct, about 1,260 lines, no sorry, checked in CI).
  Measured in CI:

  • the counter template is 152 KiB brotli in total and draws its first frame
    30 ms after the module loads in Chromium (run 40288509500);
  • on js-framework-benchmark operations it stays within 1.7× of hand-written
    JavaScript on every operation, and within 1.2× on most (run 40302274897).

• Full stack: Lasm.RPC, --template fullstack, Lasm.KV.

  • One API, checked on both sides. Endpoints, request types and validation
    are declared once in a module that both sides import. The browser checks a
    request before sending it; a theorem says an invalid one is never sent. The
    server checks it again and passes the handler a proof that the check passed,
    so server code can require that proof in its types (Store.add in the
    template).
  • One page, rendered twice. The server renders the first page from the same
    view code the browser runs, and the browser hydrates it.
  • One server, many hosts. The same Server.lean builds for Node, Workers,
    the other edge targets, Bun, Deno, Fastly and wasi-http, with the browser app
    and public/ embedded.
  • npm run dev serves everything from one URL with live reload.
  • Lasm.KV (get/put/delete) uses the platform's store: Workers KV,
    Deno KV, Fastly's KV Store, or memory elsewhere.

• WASI, wasi-http and Fastly Compute. --target wasi, wasi-http and fastly
  emit standard modules with no JavaScript at all:

  • wasi (wasi_snapshot_preview1) for wasmtime, wasmer and Node's node:wasi;
  • wasi-http, a component for wasmtime serve and Spin;
  • fastly, a Fastly Compute package, tested with Viceroy.

  A Lasm.Fetch handler is a 0.90 MiB module. It answers in about a millisecond
  on Viceroy and wasmtime serve, with a fresh instance per request
  (run 40293231963).

• Lasm.Fetch: HTTP in pure Lean. One handler,
  Request → Async Response (Lasm.Fetch.serve), serves every server target:

  • Node, on $HOST:$PORT;
  • the edge targets, Bun and Deno;
  • Fastly, WASI and wasi-http, and Spin.

  It supports streaming and outbound requests. Template: --template fetch.

• Fastify template: --template fastify, a Fastify 5 server with Lean route
  handlers.

• lasm dev: it watches the Lean sources and the Lake and npm configuration,
  rebuilds after every change and restarts the server (or reloads the browser
  app). A one-function edit is rebuilt in about 1.5–2.5 s on the Linux CI runner:

  • 1.5–1.8 s inside a running lasm dev;
  • 2.5–2.7 s as a new lasm build --dev process.

  Apple Silicon and Windows runners are slower (docs/BENCHMARKS.md, "Edit loop").

• Faster cold start on Node. main now runs on the program's main thread, and
  fewer Lean threads start up front. On a 0.29 vCPU share (AWS Lambda at 512 MB),
  a Hono app now answers its first request in about 1.3 s instead of 1.8 s; it
  uses 0.38 s of CPU, down from 0.54 s (run 40336699599). Tune the pool with
  LASM_THREAD_POOL (0–64, default 1).

• Editor support. npx lasm editor links Lasm's own Lean as an elan
  toolchain and sets it as the project's override. lasm dev, lasm build and
  lasm init do the same automatically, but lasm init only when Lean is
  already cached: it never downloads. After that, VS Code's Lean 4 extension (or
  any Lean language server client) resolves import Lasm.UI, Lasm.Fetch and the
  other Lasm.* libraries, with hovers and completion.

  • It changes nothing else in elan. elan override unset undoes it, and
    LASM_EDITOR=0 turns the automatic setup off.

• Fixed an intermittent hang in programs whose JavaScript calls a Lean
  function synchronously (present since 0.1.0). Every release now also runs
  Lasm.JS programs many times on four platforms and fails on any hang.

• Licensing notices fixed forward for 0.2.0's edge outputs. In 0.2.0, the
  notices for edge outputs were in the output directory but not in the files a
  platform uploads. From 0.3.0, every target's output carries accurate notices:

  • server-side Wasm (edge, WASI, Fastly, wasi-http) embeds the whole notices
    file;
  • JavaScript that a platform bundles carries a short licence banner;
  • browser builds and Vite builds ship the notices file.

  The edge runtime (lean-4.35.0-edge-v2) carries Lasm's full MIT text and the
  list of its Lean patches. CI checks every built output for notices and for
  copyleft code. Built apps contain no copyleft code. 0.2.0 is not deprecated:
  only permissive licences were involved, and their texts were in every output
  directory. Rebuild with 0.3.0 to get the complete notices.

Limits

These are the honest limits.

• Ahead of time only, Lean 4.35.0 exactly. A deployed program cannot elaborate
  or evaluate new Lean or use Lean's kernel at run time. There are no prebuilt
  native libraries; C source that a package bundles is compiled for you.

• The browser, the edge, Bun/Deno and WASI are single-threaded. Tasks are
  cooperative. In the browser, blocking waits (Task.get on unfinished work,
  IO.sleep, Async.block) stop with a clear message unless you build with
  --suspend jspi (only browsers with JSPI; Safari has none); use Async, Cmd and events instead.
  These targets have no files beyond a read-only UTC zone, no sockets and no
  processes.

• WASI:

  • preview 1 (--target wasi) has no sockets; use wasi-http for HTTP;
  • the wasi-http component targets the proxy world, so it has no
    environment, arguments or files;
  • on Fastly, only requests and the stores are supported (no cache,
    geolocation or logging endpoints).

• What is proved, and what is not. These are proved:

  • the Lasm.UI diff, against a model of the DOM;
  • the Lasm.RPC validation theorems;
  • your application's theorems.

  These are tested in Chromium, Firefox and WebKit, Node, workerd and the WASI
  engines, but not proved:

  • the binary patch encoding and the JavaScript applier;
  • the JSON and HTTP between client and server;
  • Lasm's compiler and runtime;
  • the browsers.

  Lean's compiler is trusted, as in any Lean program.

• Lasm.KV: on wasi-http, each request is a new instance, so the memory
  store does not outlive a request there; bind a real store. Vercel KV, Netlify
  Blobs and Upstash are not included; call them through Lasm.JS.

• Node servers:

  • cold start is CPU-bound: about 0.28 s on 4 CPUs, about 1.3 s at 0.29
    vCPU;
  • throughput: a Hono server with Lean handlers serves about 0.18× the
    requests of a plain Node http server, because each JavaScript call from Lean
    crosses threads;
  • memory: give an app 512 MB.

  Pure-Lean Std.Http is much slower; use a Node framework or Lasm.Fetch in
  production.

• Install size: @lasm/cli is a large package of about 63 MiB, and the first
  build fetches about 250–275 MB of tools once.

• Tested, not deployed. Every platform is tested in CI with its own local
  runtime, image or emulator. CI never deploys to a real cloud account.

Upgrade notes

• Existing projects build unchanged. For the new pieces, add
  --target browser|wasi|wasi-http|fastly, import Lasm.Fetch or
  import Lasm.UI. To get the new template files, scaffold a new project with
  lasm init --template web|fullstack|fetch|fastify.
• Editor setup touches elan. If you use elan, the first lasm dev or
  lasm build in a Lake project links Lasm's Lean and sets the project's override
  (it prints what it did once). To opt out, set LASM_EDITOR=0.
• Deno on release day. Deno ignores npm versions published in the last 24
  hours. Pass --minimum-dependency-age=0 to deno run and deno install for
  the first day.
• LASM_THREAD_POOL changes the Lean worker threads started before main
  (default 1; the previous behaviour started more).
• No new npm packages. The Vite plugin is @lasm/cli/vite, and the tool
  packages are unchanged.

Validation

Before release, release-checks passed for the released commit:

• Candidate checks: installed acceptance on five platforms, platform support,
  the templates and the Lasm.JS examples.
• Workflows called on the commit:
  • edge and Bun/Deno (workers.yml);
  • the browser (browser.yml: Chromium, Firefox, and WebKit on Linux and
    macOS);
  • Lasm.UI's proofs and applier (ui.yml);
  • WASI, wasi-http, Spin and Fastly (wasi.yml);
  • the fullstack template on every host (fullstack.yml);
  • the unit suite (unit.yml);
  • the dev loop, editor and cold start (dx-dev-loop.yml);
  • the Lasm.JS hang stress (lasm-js-stress.yml: 50 runs per program on four platforms).
• npm rehearsal of the exact packages on five platforms, from a loopback
  registry:
  • the web, fetch, fastify and fullstack templates, built and served;
  • --target browser|wasi|fastly|wasi-http;
  • a Vite build with @lasm/cli/vite;
  • lasm editor with Lean already cached;
  • Bun and Deno with no Node or npm on PATH.

After publication, published-templates.yml creates, builds and serves the web,
fullstack and hono templates from the public registry, and
bun-deno-published.yml repeats the Bun and Deno checks.

Licence

MIT. Built apps carry the notices of everything they contain (Lean, Emscripten,
LLVM libraries, musl, mimalloc, libuv; Wasmtime's adapter in wasi-http
components): permissive licences only. See LICENSING.md.