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.