Lasm

Write ordinary Lean. Compile it ahead of time and run it in Node. Node.js is the only supported JavaScript runtime.

Prerequisites: stock Node 26.12.0 with npm 11.20.0 for accepted candidate .54 (current source and its Phase 3 candidates pin Node 26.12.1, same npm). Lasm downloads its matching Lean 4.35.0, Lake, and build tools; you do not install them yourself (the older candidate .46 used Node 26.10.0 / Lean 4.34.1). The package is experimental and has not been published to npm.

Get started

On a supported Linux, Mac, or Windows machine, get the tested .46 tarball in the acceptance report from a maintainer (repository access may be required). Copy it into an empty directory:

npm install ./lasm-compiler-0.1.0-experimental.46.tgz

Save this complete program as Main.lean:

def main : IO Unit := do
  IO.println s!"Hello from Lean! 2 + 3 = {2 + 3}"

Run, build, and deploy:

npx lasm Main.lean           # Compile and run: Hello from Lean! 2 + 3 = 5
npx lasm build Main.lean     # Create dist/ without running main
node dist/main.mjs          # Run the deployment

The first build needs internet access and downloads about 250–275 MB for an ordinary program (tiered Lean and a minimal compiler toolchain, no Python); Lake projects and programs importing Lean download more. Measured first builds of a small program took 42–60 seconds on Linux and Apple Silicon and about 3 minutes on the slower Intel Mac and Windows CI machines. Candidate .54 passed acceptance and three consecutive cold installations on all five targets (see toolchain slimming). Candidate .46 downloaded 0.9–1.3 GB and took 5–16 minutes. The terminal shows progress and elapsed time. Later builds reuse verified tools and unchanged outputs. See cache locations, requirements, and recovery. Candidate .46 requires rerunning failed downloads. Current source adds bounded retries, safe resume, crash recovery, offline repair, and bundled installer dependencies. The hardened candidate also passed installed, offline, deployment, and proxy/CA acceptance on all six native targets then tested (including Windows ARM64, since removed), alongside the installer fault checks, and its repeated-installation gate (three consecutive clean cold installations on every target) passed on 2026-10-16. See installation hardening for settings and progress. New candidates must also pass three consecutive cold installations on every target before meeting the additional robustness gate; one successful run alone is insufficient.

Copy all of dist/ to a supported machine with the same OS, architecture, and Node version. No Lean source, npm install, build tools, or development cache is needed there. Build separately on each platform. Include your application's external assets yourself.

An existing Lake project can use local imports normally. To pin Lean, put leanprover/lean4:v4.34.1 (candidate .46) or leanprover/lean4:v4.35.0 (current source) in its lean-toolchain file. A package supports exactly one Lean release; other versions are rejected with Unsupported Lean toolchain … Supported managed versions: … and the pin is left unchanged. Current source has a per-package compatibility list (Batteries, Cli, LSpec, Plausible, Aesop, Qq, leansqlite, UnicodeBasic, MD4Lean, lean-zip, lean4-parser, lean-redis and others); packages not on it are untested. After an authorized npm release, installation will be npm install @lasm/cli (or npx @lasm/cli Main.lean without installing); the bin stays lasm. That registry command is not available yet. Current source, not yet in a candidate, can take its build tools from exact-pinned @lasm/… npm packages instead of downloading them, and fetches the Lake/Lean-import data and Git with your own npm on first use; this was validated only against a local test registry (npm distribution). LASM_ARTIFACT_SOURCE=npm forbids direct downloads; https ignores the packages.

CLI reference

These are all commands and options in the ordinary Node application interface:

--rebuild and --verbose work with both run and build. --output is build-only; arguments after -- are run-only. The application's exit status is preserved. There is currently no Lasm install, clean, uninstall, or version subcommand. Candidate .46 also accepts a redundant --target node; current source removed that option, and passing it is an error. The source installer also accepts the documented download environment settings.

The source checkout also retains experimental interfaces. They are unavailable in the Node release candidate: node bin/lasm.mjs build examples/basic/lasm.json dist builds callable bindings from a JSON configuration; node lasm-node.js [--rebuild] [--verbose] Main.lean [--] [arguments…] is a source-only compatibility launcher. These interfaces have no current release support guarantee.

Supported environments

Other OS releases and Node/npm/Lean versions are unverified. No engine flags are needed. Linux requires its ordinary OS libraries and shell, but no developer SDK. The acceptance report identifies exact tested artifacts; the plan records the completed milestone and deferred work. Lasm supports five targets: Linux and macOS on x86-64 and ARM64, and Windows on x86-64. The same .46 archive passed on all five (and historically on Windows ARM64, which current source no longer supports). These passes use native x86-64 and ARM64 execution.

Lean support and restrictions

Candidate .46 and current source builds enforce ahead-of-time execution. The older .34 candidate predates these restrictions; do not use it to enforce this policy.

Ordinary functions, recursion, closures, inductive types, pattern matching, type classes, dependent types, and compiled IO are not excluded by this policy. Imports, macros, elaboration, tactics, deriving, proofs, and #eval can run during compilation in managed native Lean. Generated code must meet the same runtime restrictions as handwritten code. Import names are not banned, but initializers count as runtime dependencies: a broad import Lean can retain the compiler. Use ordinary Lean meta import Lean when it is needed only by macros or tactics in a module; use narrower imports for runtime data libraries. For example, accepted candidates reject import Lean with Lean.Json.compress, while import Lean.Data.Json builds and runs (current source accepts both; see below). Current source (not yet in a candidate) explains each rejection: it prints the chain from your code to the compiler code and, when a broad import is the cause, the narrower modules your code uses (here import Lean.Data.Json.Basic and import Lean.Data.Json.Printer). Current source also links Lean 4.35's LeanExport library (candidates fail with an undefined initialize_LeanExport_… symbol). Its parser, LeanExport.parseStream, builds Lean.Expr values, whose constructors call Lean's C++ kernel, so programs using it are still rejected. Current source also fixes the following (in candidate .39500947696, which passed installed acceptance; its cold-installation gate is pending; accepted candidates behave as described in parentheses): deployed programs honor LEAN_ABORT_ON_NONLINEAR=1 as native Lean does (ignored); on macOS and Windows a standalone source directory containing a file such as init.lean or std.lean no longer hides the standard Init/Std libraries (Cyclic Lean module imports …/Init.lean); on Windows, IO.Process.spawn with piped stdin/stdout/stderr works (fails with "bad file descriptor"), DNS lookups and Std.Net.interfaceAddresses work (fail), handle misuse reports the same error as native Lean, and projects in deep directories build. On Windows a project whose delivered dist\program.wasm path would exceed 260 characters still fails to build. Per-platform results: language coverage.

Lake packages (current source, Phase 3 and its wrap-up; candidate .39815056197 passed installed acceptance and the cold-installation gate):

• Modules imported only for compilation (tactics, elaborators, attributes, for example Aesop, Qq or import Lean for macros) no longer keep Lean's compiler in the deployment. In particular import Lean with Lean.Json (and deriving ToJson, FromJson) now builds and runs; runtime elaboration and evaluation stay unavailable. Lasm runs a module's initializers only when the program uses something they define, when they register state the program uses, or when they are the program's own code doing console, file, process or environment IO or calling C. Other initialization side effects of unused modules (for example a library printing while it initializes) do not happen, as with Lean's own meta import. --verbose shows how many initializers were skipped.
• C source that a package bundles (extern_lib, moreLinkObjs, for example leansqlite's SQLite) is compiled for Node with Lasm's compiler. Lake still builds that C natively first; Lasm then downloads a "C tier" once (39–52 MB): Lean's own clang, which becomes Lake's default cc, its linker and headers, and C library headers. No system C compiler is needed. On Linux and Windows nothing else is needed either; on macOS the C library headers come from the Xcode Command Line Tools SDK (xcode-select --install), which Lasm may not redistribute, and the build says so when it is missing. C code that calls dlopen gets an implementation that always fails.
• Prebuilt native libraries (shared libraries or -l link options, for example libcurl, OpenSSL, libpq, hiredis, BLAS) cannot be linked. When the program's code needs one, the build stops and names the library and the package that declares it; a library used only during compilation (a tactic's solver) is left out.
• Outbound HTTP: today a Lasm program makes HTTP requests by running the curl tool with IO.Process (where curl is installed), as natively. Calling Node's own fetch (and npm packages) through JS/npm interop is planned for Phase 4. The experimental Millillion/fetch library tested in Phase 3 is superseded, archived and was never released.

The deployed application cannot use the following capabilities:

The build checks reachable runtime dependencies, including imported libraries and indirect calls, before producing a deployment. A reachable forbidden call is rejected even if your current input would not take that branch. Dead code removed by the linker is not a runtime dependency. The check is conservative: live Lean C++ compiler/kernel code or mutable state is rejected, apart from audited initialization-independent inline helpers and read-only data. A dependency may therefore need refactoring to keep compiler operations at build time.

The launcher also rejects missing, stale, or incompatible capability records before loading the application. This checks the declared build capabilities; it is not a security sandbox against someone rewriting JavaScript or Wasm. There is no large compatibility fallback in current source builds.

This restriction does not imply full compatibility for everything else. Console output, arguments, exit codes, local Lake imports, and selected language/filesystem fixtures have native-versus-Node tests. Complete IO.FS, Std.Http, concurrency, subprocess/signal/terminal parity, every third-party library, and the full Lean upstream suite are not release guarantees. See IO gaps and deployment-size evidence for the remaining work. Long-running Std.Http servers are not yet production-ready: with candidate .54, a server's memory grows with every request until the process is stopped (see the Server MVP robustness results). Native Lean's memory stays flat under the same load.