Skip to content

Repository navigation

Lasm 0.2.0

Choose a tag to compare

View all tags
@github-actions github-actions released this 26 Oct 12:35
· 333 commits to main since this release
v0.2.0
544d1dd
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

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.

Assets 2
Loading