Lasm 0.3.5

Lasm 0.3.5

A documentation and example release, so that the npm page shows the current
README. Upgrade with npm install -D @lasm/cli@0.3.5. The compiler, the runtimes
and the library are unchanged from 0.3.4: nothing changes in how programs build
or run.

Documentation

• Support Lasm. The README and llms.txt have a section on sponsoring the
  project through GitHub Sponsors.
• README for Conduit. The README now features Conduit's complete app, the
  Lean frontend and the proved theorems, as the flagship example.

Conduit (examples/conduit)

• The frontend is written in Lean with Lasm.UI, rendered on the server and
  hydrated in the browser. It passes the official RealWorld end-to-end suite
  without retries: on Node with Chromium, Firefox and WebKit, and on Workers and
  Bun with Chromium.
• Proofs. Theorems about the code the server runs and about the browser app
  and its Markdown are checked in CI (examples/conduit/PROOFS.md).
• The example uses @lasm/cli 0.3.4 or later.

CI

• fullstack.yml uses the pinned edge runtime from its release instead of
  rebuilding it. The rebuild was being stopped by the resource guard on
  standard runners. workers.yml still rebuilds it and checks it against the
  catalog.

Lasm 0.3.4

Lasm 0.3.4

A patch release. Upgrade with npm install -D @lasm/cli@0.3.4. Nothing changes
in how programs build.

0.3.3 was never published: its release checks failed on CI problems (fixed
here), so its changes ship in 0.3.4.

Fixes

• Lasm.UI: the address and the page change together. A same-origin link
  click now renders the new page in the same task as its pushState.
  Cmd.pushUrl and Cmd.replaceUrl create their history entry in the same frame
  that shows the new page. Before, the address changed one animation frame
  before the page, so a test waiting for the new URL could still see the old
  page. This was found by the RealWorld end-to-end suite on Conduit.
• A second UDP receive fails at once. UDP.Socket.recv and waitReadable
  on a socket that already has a receive pending now fail immediately with the
  error native Lean gives: an IO error from libuv's EALREADY, "connection already
  in progress". Before, they returned a promise that failed later with a
  different message. A failure to start receiving is reported the same way.

Examples and documentation

• Conduit (examples/conduit): the RealWorld API in Lean. It runs on Node
  (node:sqlite), Cloudflare Workers (D1) and Bun (bun:sqlite), and passes
  the official Hurl suite.
• The README is rewritten for people and coding agents. It now has quick
  facts, a start-here table, recipes and the examples up front, plus llms.txt
  and docs/AI.md.

Release and CI tooling

• The check that runs npm create @lasm from the public registry after a
  release no longer skips itself by mistake. For 0.3.2 it read the release run's
  job list before GitHub had filled it in. It now waits until the run and all of
  its jobs have finished (scripts/release/published-gate.mjs).
• The edge runtime's system libraries get the same member names on every build
  machine, so the archive CI rebuilds matches the pinned one.
• Playwright installs in CI run within one 25-minute budget, inside 30-minute
  steps.
• The candidate cache step evicts its own stale caches (unused for 24 hours)
  instead of failing at the 8 GiB cache ceiling.

Runtime

The Node runtime is rebuilt with the host-bridge change. Only the host bridge
object (node-async.cpp.o) differs from 0.3.2's runtime. The edge runtime is
rebuilt on it (lean-4.35.0-edge-v4). See docs/DECISIONS.md (2026-10-27).

Lasm 0.3.2

Lasm 0.3.2

A patch release that fixes how deployed programs handle Std.Internal.UV
sockets, timers and signals, so that they match native Lean 4.35. Upgrade with
npm install -D @lasm/cli@0.3.2. Nothing changes in how programs build.

Fixes

• A second accept on a TCP socket fails at once. Before, it returned a
  promise that later failed with a different error. It now fails with the same
  error native Lean gives (otherError, EALREADY).
  • The same applies to tryAccept, which now reports failures as IO errors, not
    inside its Except result.
• accept on a socket that is not listening fails at once with
  invalidArgument ("socket is not listening"). It used to fail only later.
• Std.Internal.UV.Loop.alive and Loop.configure work. alive used to
  stop the program and configure used to fail with "not supported". alive
  returns true, as native Lean 4.35 does, and configure succeeds.
• Cancelling no longer stalls other asynchronous work. Cancelling or
  stopping an operation drops its pending promise:
  • The operations: Timer.stop/cancel, Signal.stop/cancel,
    TCP.Socket.cancelAccept/cancelRecv and UDP.Socket.cancelRecv.
  • The promise is now released on the thread that cancels, after the handle is
    unlocked, as libuv does.
  • Before, a (sync := true) continuation on that promise ran on the thread
    that completes every asynchronous operation. A continuation that blocked
    there held up every timer and socket.
  • Before, a continuation that stopped the same timer or signal again
    deadlocked.

These behaviours are pinned by Lean 4.36's new upstream tests (elab/uv_*,
compile/uv_*). Where Lean 4.36 changes behaviour on purpose, Lasm keeps
Lean 4.35's for 4.35 and switches when it moves to Lean 4.36:

• truncated UDP datagrams fail with EMSGSIZE;
• System.osHomedir and System.osTmpdir return values longer than PATH_MAX;
• cancelled signal waiters keep listening.

Runtime

The Node runtime is 79968781… (CI build 40471483055). Only the event-loop
object and the host bridge changed, and no initialization path changed. The edge
runtime is rebuilt on it (lean-4.35.0-edge-v3). See docs/DECISIONS.md
(2026-10-27).

Lasm 0.3.1

Lasm 0.3.1

A small release after the 0.3.0 launch: the starter code is now MIT-0, and Lasm
points you to a bug report when it hits an internal error. Upgrade with
npm install -D @lasm/cli@0.3.1. Nothing changes in how programs build or run.

What's new

• Starter code under MIT No Attribution (MIT-0). Everything that lasm init
  and npm create @lasm put in a new project, templates/, examples/, and the
  code samples in the README and docs/ are now also under MIT-0. The code is
  yours to use without keeping Lasm's notice. Lasm itself stays MIT.
  • @lasm/cli carries LICENSE-MIT-0, templates/LICENSE and
    examples/LICENSE.
  • Its license field names MIT-0 next to MIT and the bundled components.
  • Built apps' THIRD_PARTY_NOTICES.txt is unchanged: it still lists Lean,
    Emscripten and the other runtime components that a build contains.
• lasm --version (also -v) prints the version, the Lean release, the
  JavaScript runtime and the platform, for example
  lasm 0.3.1 (@lasm/cli; Lean 4.35.0; Node 26.12.1; linux-x64).
• Bug reports. After an unexpected internal error, the CLI and lasm dev
  print the error's stack and then one line:
  If this looks like a Lasm bug, please report it: https://github.com/Millillion/lasm/issues/new?template=bug.yml.
  An internal error is a programming error inside Lasm, such as a TypeError or
  a failed internal assertion. Lean errors in your code, usage errors and the
  messages Lasm gives on purpose (a missing tool, an unsupported platform) never
  print it.
• Issue templates on GitHub:
  • a bug report form, which asks for lasm --version, the operating system, the
    Node/Bun/Deno version, the target, a template or project, and the output;
  • a feature request form;
  • links to the documentation and to Lean's Zulip for questions about Lean
    itself.

Fixes

• The post-release template check (published-templates.yml) now skips when the
  release run that triggered it published nothing. Before, a release run that
  only waited for the checks started it against the previous release.

Limits

Unchanged from 0.3.0: see the 0.3.0 notes.

Validation

Before release, release-checks passed for the released commit, with the same
gates as 0.3.0:

• the five-platform candidate checks;
• the edge and Bun/Deno checks;
• the browser, Lasm.UI, WASI/Fastly, fullstack, unit and dev-loop checks;
• the Lasm.JS hang stress;
• the npm rehearsal of the exact packages on five platforms, which now also
  checks that the installed CLI carries the MIT-0 texts and names MIT-0 in its
  licence.

After publication, published-templates.yml and bun-deno-published.yml check
the release from the public registry.

Licence

MIT, plus MIT-0 for the starter code. See LICENSING.md.

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_T...

Lasm edge runtime lean-4.35.0-edge-v4

Lean's runtime built single-threaded for edge isolates (docs/EDGE.md), the archive pinned by src/edge-runtimes.json. A draft until Lasm 0.2.0 publishes it. Source revision: 4261b3f

Lasm edge runtime lean-4.35.0-edge-v3

Lean's runtime built single-threaded for edge isolates (docs/EDGE.md), the archive pinned by src/edge-runtimes.json. A draft until Lasm 0.2.0 publishes it. Source revision: 4c35758

Lasm 0.2.0

Lasm 0.2.0

Lasm compiles ordinary Lean 4.35.0 programs ahead of time to WebAssembly. 0.2.0
adds two things: programs now run on edge isolates (Cloudflare Workers, Vercel
Edge, Netlify Edge, Deno Deploy, Supabase Edge Functions), and the compiler and its
programs run on Bun and Deno, with no Node or npm installed. Node builds are
unchanged. Upgrade with npm install -D @lasm/cli@0.2.0, or start a new project with
npm create @lasm@latest my-app -- --template hono.

What's new

• Edge targets. lasm build Main.lean --target workers|vercel-edge|netlify-edge|deno-deploy|supabase-edge
  builds dist/ as before. It then relinks the program with a single-threaded Lean
  runtime and a pure-JavaScript host made of web-standard APIs, and writes the
  platform's files:

  • workers/: a Worker with wrangler.toml;
  • api/lasm.mjs: a Vercel Edge function;
  • netlify/edge-functions/lasm.mjs: a Netlify Edge Function;
  • deno/main.mjs: Deno Deploy;
  • supabase/functions/<name>/: a Supabase Edge Function with a deno.json
    that pins its npm imports.

  lasm init --template hono --deploy <target> adds the platform files and
  npm run build:<target>. One Main.lean serves on Node and on the edge.

  • Use Lasm.JS.exportDefault to export a fetch handler, and Lasm.JS.onEdge
    to tell which runtime you are on.
  • The edge runtime ships inside @lasm/cli, so nothing more is downloaded.
  • Edge builds need no Emscripten SDK, and an unchanged edge build takes a few
    seconds (the linked program is cached).

• Bun and Deno.

  • The compiler runs with Bun or Deno as its only JavaScript runtime:
    bunx --bun @lasm/cli Main.lean, deno run -A npm:@lasm/cli build Main.lean,
    bun create @lasm my-app --template hono,
    deno run -A npm:@lasm/create my-app --template hono.
  • It produces the same bytes as on Node.
  • Under Bun or Deno the default target is that runtime: bun/main.mjs or
    deno/main.mjs, using the portable (edge) profile. A command-line main
    gets its arguments and exit code. A Lasm.JS.exportDefault handler is served
    with Bun.serve or Deno.serve.
  • The plain and hono templates get dev:bun, build:bun, build:deno and
    start:* scripts.
  • Without npm, on-demand tool packages come straight from the registry, with
    the same checksums.

Supported platforms and their limits

Everything here is supported. It is tested in CI with each platform's own local
tools or runtime image; nothing is ever deployed, and no account is used.

Target	Tested with	Limits to know
Cloudflare Workers	wrangler dev 4.152.0 (workerd), Free-plan budgets gated	128 MB per isolate; Free plan 10 ms CPU per request; 1 s to evaluate the global scope. The Hono template is 1.40 MiB (245 KiB gzip), against the 64 MiB limit. Bindings other than string variables (KV, D1, R2, Durable Objects) reach Lean only as Lasm.JS values through env.
Vercel Edge	vercel build offline, then the function bundled with esbuild and run in Vercel's edge-runtime 4.0.1	Gzip limit 1 MB on Hobby (the Hono template is 244 KiB). Less faithful than the others: Vercel bundles at deployment and vercel dev needs a login, so the deployed bundle and Vercel's production V8 are not reproduced. Vercel itself recommends Node over its edge runtime.
Netlify Edge	netlify build --offline (Netlify's bundler, the eszip it deploys) and netlify dev --offline	20 MB compressed (the Hono eszip is 1.82 MiB), 512 MB memory, 50 ms CPU. The Wasm is embedded as a JavaScript module.
Deno Deploy	Deno 2.9.6 running deno/main.mjs	Deploy's own Deno version and isolate limits are not reproduced.
Supabase Edge Functions	Supabase's edge-runtime v1.77.8 image in Docker, with the Supabase CLI's worker options and limits	Supabase's runtime (V8 11.6) has no JSPI, so this target uses Asyncify. Blocking waits still work. The cost: program.wasm is 2.9–3.2× larger (Hono 2.18 MiB, against the 20 MB limit), compute is up to about 1.8× slower, and a cold worker takes 440–580 ms. Limits: 256 MB memory, 2 s CPU.
Bun 1.4.4 and Deno 2.9.6 (compiler and programs)	All five platforms: an installed candidate, and the release's own packages from a loopback registry, with no Node or npm on PATH	Programs need JSPI: Bun 1.3.14 or newer, Deno 2.x, or Node 26. Node 24 cannot run bun/main.mjs or deno/main.mjs.

The edge and portable profile (all of the targets above, plus --target bun|deno)
is single-threaded Lean:

• What works:
  • pure Lean, including big numbers without GMP;
  • tasks, which are cooperative and interleave at waits;
  • Std.Async, timers and IO.Promise;
  • blocking waits (Task.get, IO.wait, IO.sleep, Async.block), which run
    other Lean work while they wait;
  • Std.Mutex, Lasm.JS, clocks, Std.Time in UTC, environment variables and
    IO.getRandomBytes.
• What is not available:
  • threads and parallel speed-up;
  • the file system, beyond a read-only UTC zone;
  • standard input, sockets and Std.Http servers (use fetch through
    Lasm.JS), processes and signals;
  • koffi, and native C that needs threads or POSIX;
  • the Express template.
• Other limits:
  • Recursion depth is about 10,000–30,000 frames (the engine's stack).
  • On Workers, random bytes during startup are not cryptographic.

For any of these, use the Node build (--target node, the default under Node). The
full profile (threads, files, processes, koffi, wasm64) stays Node-only. Details:
EDGE.md and BUN_DENO.md.

Upgrade notes

• Nothing changes for Node builds. 0.1.x projects build unchanged. To add an
  edge target, run lasm build Main.lean --target <target>. For the platform files,
  scaffold a new project with lasm init --template hono --deploy <target>, or
  copy them from one.
• Deno on release day. Deno 2.9 ignores npm versions published in the last 24
  hours. For the first day after this release, pass --minimum-dependency-age=0 to
  deno run and deno install, for example
  deno run -A --minimum-dependency-age=0 npm:@lasm/cli@0.2.0 Main.lean. Otherwise
  Deno resolves to 0.1.0, which has no Bun or Deno support, or to nothing. You can
  also set "minimumDependencyAge" in deno.json. Bun has no such default.
• Use --bun with bunx (bunx --bun @lasm/cli …). Without it, Bun runs Lasm
  with Node when Node is installed.
• The package is about 1.7 MB larger, because it carries the single-threaded
  edge runtime. No new npm package is needed.

Validation

Before release, the exact commit passed release-checks:

• the five-platform candidate checks, as for 0.1.0: installed acceptance,
  platform support, templates and the Lasm.JS examples;
• the edge and Bun/Deno checks: the edge runtime rebuilt and byte-compared with
  its pin; every edge target served and checked by its local tool; the compiler
  under Bun and Deno; an installed candidate under Node, Bun and Deno on all five
  platforms, with the same program.wasm everywhere;
• an npm rehearsal of the exact packages on all five platforms from a loopback
  registry. It covers every edge target built from the installed CLI with nothing
  downloaded, and Bun and Deno installing, building and serving with no Node or
  npm on PATH.

After publication, bun-deno-published.yml repeats the Bun and Deno checks
against the public registry.

Licence

MIT. The edge runtime in @lasm/cli holds:

• Lean's runtime (Apache-2.0);
• Lasm's host bridge (MIT);
• Emscripten's system libraries, under the Emscripten, musl, mimalloc and LLVM
  licences, which were already in 0.1.0.

Its notices are in licenses/edge-runtime/. Built edge apps carry
THIRD_PARTY_NOTICES.txt as Node builds do.

Lasm 0.1.0

Lasm 0.1.0

Lasm compiles ordinary Lean 4.35.0 programs ahead of time to WebAssembly that runs
in Node. This is the first npm release: npm create @lasm@latest my-app -- --template hono,
npm install -D @lasm/cli (bin lasm) or npx @lasm/cli init my-app. You need only
Node 24 or newer and npm; Lasm brings Lean, Lake and its build tools as npm packages.

Highlights

• lasm Main.lean builds and runs; lasm build Main.lean writes a self-contained
  dist/ that needs only Node. Lake projects and their dependencies work.
• lasm build --target lambda|lambda-edge|vercel|netlify|azure|gcf builds and packages
  for a function platform in one step (lasm package re-packages an existing build):
  AWS Lambda zips (API Gateway, function URLs, ALB, CloudFront/Lambda@Edge), Vercel
  (Build Output API), Netlify Functions, Azure Functions and Google Cloud Functions.
• lasm init with templates plain, express, hono and std-http, a Dockerfile,
  and --deploy targets that add the platform's files and npm run build:<target>.
• import Lasm.JS: call npm packages and Node APIs from Lean with typed bindings,
  promises as Lean tasks, and Lean request handlers in Express or Hono. npm
  dependencies are deployed in dist/node_modules.
• Lake projects with C code build without a system C compiler (Lean's clang and C
  library headers are provided; macOS needs the Xcode Command Line Tools SDK).
• Builds from any supported machine also run on Linux x64/arm64, glibc 2.28+ or
  musl (Alpine). Without a time zone database, or when a sandbox denies it, apps
  fall back to UTC instead of failing.
• A dev build profile (lasm Main.lean, lasm build --dev) builds faster; release
  builds are byte-reproducible.

Supported

Compiler and apps: Linux x64/arm64, macOS x64/arm64, Windows x64; Node 24+
(tested: Node 24.0.0, 24.22.1 and 26.12.1). Deployment: Docker/Kubernetes images
(Debian, Ubuntu, Amazon Linux 2023, Alpine), AWS Lambda (zip and container image),
Lambda@Edge, Vercel, Netlify, Azure Functions, Google Cloud Functions, gVisor-based
hosts such as DigitalOcean App Platform, and container recipes for Cloud Run, Fly.io,
Railway, Render and Heroku. Every claim names the CI job that backs it in the
README; hosted platforms are tested only
through their own local tools, images and emulators, never with real accounts.

Validation

Before release, the candidate passed the full launch gate: the upstream
runtime-capable Lean 4.35.0 suite and 19 ecosystem projects on all five targets,
with zero regressions against the previous accepted release. It also passed three
back-to-back cold installations, server robustness and fault tests, the release
benchmarks and an npm rehearsal. Big-number results match native Lean.
Details, run IDs and the classified non-passes: 0.1.0-gate.md.

Known limitations

Ahead of time only (no run-time elaboration, evaluation, plugins or Lean as a
library beyond data), no prebuilt native libraries, no Windows ARM64 and no edge
isolates (Cloudflare Workers, Vercel/Netlify Edge) yet, at least 512 MB of memory
per app, waiting Lean handlers bounded by Lean's worker threads, and
arbitrary-precision arithmetic beyond a few hundred digits that is slower than GMP
(at 10,000 digits multiplication about 5× and Nat.gcd about 60×). Full list:
README, Known limitations.

Licence

MIT. Built apps carry THIRD_PARTY_NOTICES.txt (Lean, Emscripten, LLVM libraries,
musl, mimalloc, libuv: permissive licences only; the Wasm runtime uses Lean's own
big-number code, not GNU MP) and their npm packages' own licences.

Lasm runtime input 40332716905

Pinned runtime handoff; no package acceptance or npm publication is implied. Preserve the recorded SHA-256 when updating scripts/ci/node-runtime-source.json. Source revision: e5eb6b9