Lasm：在 Lean 中编写经形式化验证的 Node、serverless 与 edge Web 应用

面向 JavaScript 和 WebAssembly 世界的 Lean 4。Lasm 可以将普通的 Lean 4 程序提前（Ahead-of-Time）编译为 WebAssembly。单一的 Lean 代码库可以变成 Node 服务器、无服务器或边缘函数、WASI/Fastly 模块或浏览器应用。由于它是 Lean，你可以证明所部署代码的属性。旗舰示例 Conduit 是包含 117 个已证明定理的 RealWorld 应用。Lasm 在 npm 上发布，并自带 Lean、Lake 及其构建工具；你只需要 Node（或 Bun 或 Deno）。

npm create @lasm@latest my-app -- --template hono    # then: cd my-app && npm install && npm run dev

AI 代理：此 README 本身是完整的。llms.txt 是简短的索引，docs/AI.md 列出了能帮你避免走弯路的规则。

如果 Lasm 对你有所帮助，我将不胜感激你的赞助（详情见下文）。

快速事实

平台

每一行都在 CI 中使用平台的本地运行时、镜像或模拟器进行测试。 根据项目策略，CI 绝不会部署到真实的云账户中 （各个平台的测试方式）。

Node 构建拥有 Lean 的完整运行时（线程、文件、进程、套接字）。边缘、Bun/Deno、WASI 和浏览器构建运行单线程的 Lean，没有套接字或进程（也没有文件，WASI 除外）；Lean 的其余部分均可正常工作。

从这里开始

每个示例都包含一个带有一条命令运行说明的 README；examples/README.md 列出了所有这些示例。

旗舰示例：Conduit，包含 117 个已证明的定理

examples/conduit 是 Conduit，即 RealWorld 应用（一个 Medium 克隆版），完全用 Lean 编写：包括 REST API、服务端渲染的浏览器应用以及证明。

• 关于实际运行代码的 117 个定理，经检查不包含 sorry，且仅使用 Lean 的标准公理（npm run proofs；PROOFS.md 用通俗易懂的英文列出了每一个定理）。它们涵盖了授权（只有作者可以修改自己的文章和评论）、关注与收藏、永不冲突的 slug、永不跳过或重复的分页、客户端与服务器共享的验证（应用绝不会发送服务器会拒绝的内容）、JSON 往返以及 Markdown 链接安全性。这些端点是针对函数的 Store 编写的，并且证明在表格模型上运行了相同的代码。
• 受信任但未证明的部分：每个 SQL 语句都符合其模型所描述的行为、JSON 文本层、请求并发性，以及 Lean、Lasm 和 JavaScript 运行时。对整个 RealWorld 规范的符合性是通过测试而非证明来保证的。
• API：官方 RealWorld API 套件在 Node（node:sqlite）、Cloudflare Workers（D1）和 Bun（bun:sqlite）上未作修改即可通过（13 个文件中的 13 个，154 个请求）。每个目标都有一个手写的 @[js] 绑定模块。
• 前端：在 RealWorld 官方模板上的 Lasm.UI，具备服务端渲染、水合作用（hydration）以及在 Lean 中解析的 Markdown。官方的 Playwright 端到端套件在配备 Chromium、Firefox 和 WebKit 的 Node 上，以及配备 Chromium 的 Workers 和 Bun 上通过，无需重试。

所有这些都在 CI 中运行（conduit.yml，运行编号 40615274657，使用 @lasm/cli 0.3.4）。

cd examples/conduit
npm install                                   # @lasm/cli, Hurl and Playwright (the official suites' runners)
npm run build && npm start                    # http://localhost:3000: the app and its API on Node
npm run proofs                                # check all 117 theorems
npm test                                      # the official API suite (also test:workers, test:bun)
npx playwright install chromium && npm run test:e2e   # the official end-to-end suite
npm run build:workers && npx wrangler dev     # Cloudflare Workers with local D1
npm run build:bun && npm run start:bun        # Bun with bun:sqlite

60 秒快速开始

单文件无需项目。将这个完整的程序保存为 Main.lean：

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

npx @lasm/cli Main.lean          # builds and runs: Hello from Lean! 2 + 3 = 5
npx @lasm/cli build Main.lean    # writes dist/; run it with: node dist/main.mjs

在新机器上的首次构建会获取一次 Lean 和构建工具（大约 250–275 MB；在 Linux CI 运行器上首次构建耗时 19 秒）。后续对单行代码更改的开发构建大约需要 1–2 秒。

操作指南

每个指南都是完整的：创建、开发、构建、部署。Lasm 从不安装或启动平台自身的 CLI（wrangler、vercel、fastly 等）；这些需要由你来运行。npm run dev 是 lasm dev：它在每次保存后大约 2 秒重新构建并重启服务器，并且在出现类型错误时保持上一个良好的构建继续运行。

Node 服务器（Hono；同时支持 express、fastify、std-http、fetch）。

npm create @lasm@latest my-api -- --template hono
cd my-api && npm install
npm run dev                                   # http://localhost:3000/hello/Ada
npm run build && npm start                    # dist/ needs only Node 24+
docker build -t my-api . && docker run -p 8080:8080 my-api   # the generated Dockerfile

AWS Lambda / Vercel / Netlify / Azure / Google Cloud Functions。

npm create @lasm@latest my-fn -- --template hono --deploy lambda-zip   # or vercel, netlify, azure, gcf, lambda-edge
cd my-fn && npm install
npm run build:lambda                          # dist/ and lambda.zip (handler lasm-lambda.handler)
# deploy lambda.zip with the AWS console, aws CLI or SAM; recipes: docs/deploy/lambda.md

Cloudflare Workers（以及 Vercel Edge、Netlify Edge、Deno Deploy、Supabase）。

npm create @lasm@latest my-edge -- --template hono --deploy workers
cd my-edge && npm install
npm run build:workers                         # workers/ (wrangler.toml came from lasm init)
npx wrangler dev                              # local workerd; npx wrangler deploy to publish

Fastly Compute、WASI、Spin。

npm create @lasm@latest my-svc -- --template fetch --deploy fastly --deploy spin
cd my-svc && npm install
npm run build:fastly && fastly compute serve  # Viceroy on http://127.0.0.1:7676
npm run build:wasi-http && spin up            # or: wasmtime serve wasi-http/main.wasm

浏览器应用。

npm create @lasm@latest my-web -- --template web
cd my-web && npm install
npm run dev                                   # http://127.0.0.1:5173, live reload
npm run build                                 # dist/: a static site for any host or CDN

全栈（服务端 + 浏览器 + 已验证 API）。

npm create @lasm@latest my-app -- --template fullstack
cd my-app && npm install
npm run dev                                   # one URL: http://127.0.0.1:3000
npm run build && npm start                    # Node; also build:workers, build:bun, build:deno

编辑器。每个项目运行一次 npx lasm editor；lasm init、lasm dev 和 lasm build 也会这样做。随后 Lean 编辑器（VS Code 的 Lean 4 扩展）会解析 import Lasm.*（详情）。

Lean 中的整个栈，经过验证

fullstack 模板是一个包含服务端（Lasm.Fetch）、浏览器应用（Lasm.UI）以及两者间 API（Lasm.RPC）的 Lean 项目。请求必须满足的规则在 Shared.lean 中编写并证明了一次，双方都会导入该文件（templates/fullstack）：

-- Shared.lean
@[irreducible] def checkTitle (title : String) : Except String Unit :=
  let n := (clean title).length
  if n = 0 then .error "Write something first."
  else if n > maxTitle then .error s!"Keep it under {maxTitle} characters."
  else .ok ()

/-- Proved once, holds in the browser and on the server. -/
theorem checkTitle_ok {title : String} (h : checkTitle title = .ok ()) :
    0 < (clean title).length ∧ (clean title).length ≤ maxTitle := by
  unfold checkTitle at h
  by_cases h0 : (clean title).length = 0
  · simp [h0] at h
  · by_cases h1 : (clean title).length > maxTitle
    · simp [h0, h1] at h
    · omega

def addTodo : Endpoint NewTodo Todo := { name := "addTodo", validate := fun r => checkTitle r.title }

-- Server.lean: storing a todo demands the proof that its title passed the check,
-- and `addTodo.serve` hands the handler that proof (`ok`) after re-validating.
def Store.add (s : Store) (title : String) (_ : checkTitle title = .ok ()) : Store × Todo :=
  let t := { id := s.next, title := clean title, done := false }
  ({ todos := s.todos.push t, next := s.next + 1 }, t)

  addTodo.serve fun req ok => do
    let (s, t) := (← load kv).add req.title ok
    save kv s
    return .ok t

-- Client.lean: a theorem about the browser app: it never sends an invalid title.
theorem add_invalid (m : Model) (e : String) (h : checkTitle m.draft = .error e) :
    (update .add m).2.effects = [.msg (.added (.error (.invalid e)))] :=
  addTodo.call_invalid { title := m.draft } Msg.added "" e h

证明所在的位置以及如何进行检查。

未经验证，在 CI 中进行测试：客户端与服务端之间的 JSON/HTTP 传输、将补丁应用到真实 DOM 的 JavaScript、Lasm 编译器与运行时、以及浏览器。Lean 自身的编译器是受信任的，如同任何 Lean 程序一样（UI.md、RPC.md）。

从 Lean 调用 JavaScript 和 npm

用单行代码声明你调用的每个 JavaScript 函数；Lean 类型说明了值的转换方式。一个完整的程序（Node 的全局 fetch）：

import Lasm.JS
open Lasm.JS

/-- `await fetch(url, init)` (Node's global fetch) -/
@[js "globalThis" "fetch"] opaque fetch : String → Data → IO Value

def main : IO Unit := do
  let response ← fetch "https://example.com" (obj [])
  IO.println s!"{← response.get "status" Nat}: {(← response.callMethodAwait "text" #[] String).length} characters"

编写绑定（bindings）的规则：

• @[js "module" "export"] opaque name : A → B → IO R 绑定 module.export。该模块是一个 npm 包（"marked"）、Node 内置模块（"node:fs"），或者是用于全局变量的 "globalThis"。"new Hono" 调用构造函数，而 "" 是模块自身的值。
• 对于立即返回的值，类型以 IO R 结尾；对于 Promise，以 Async R 结尾。Async 绑定在等待（awaited）时不会占用 Lean 线程。
• 使用 String、Nat、Int、Float、Bool、ByteArray、Array、List、Option、元组、Data（任何 JS 数据）或 Value（JS 对象引用：get、callMethod、callMethodAwait）。你自己的结构体可以通过 deriving ToJS, FromJS 进行转换。
• Function.ofFn / Function.ofFnReply 将 Lean 函数转换为 JS 回调。框架处理程序会使用它们（参见 hono、express 和 fastify 模板）。
• npm install 是 lakefile 旁边的包。lasm build 针对已安装的包（Lasm.JS binding check failed: … export "x" is missing）检查每个绑定，并将生产依赖项复制到 dist/node_modules 中。
• 每次调用都会从 Lean 线程跨越到 Node 的主线程（约 24 µs），因此请倾向于使用一个粗粒度调用，而不是多个小调用。

完整指南，包含 Express、Hono、pg、jose 和 fetch 示例以及代理检查清单：docs/JS_BINDINGS.md。

测得的数据

所有数据均来自免费 GitHub 运行器（4-CPU AMD EPYC，Linux x64）上的 CI，候选版本 0.1.0-experimental.40494203854 (2026-10-27)，除非另有说明。完整表格、方法与注意事项：BENCHMARKS.md。

Node 上的 Lean 需要为 WebAssembly 及其线程付出开销。冷启动是 CPU 密集型的，因此它在小型无服务器 CPU 份额上会增长，并且每个 JavaScript 调用都会跨越线程。纯 Lean Std.Http 在 Node 上较慢（1,290 req/s），因此生产环境 HTTP 请使用 Hono、Express、Fastify 或 Lasm.Fetch。带有数千位数字的算术运算比原生 Lean 慢（无 GMP）。

已知限制

• 仅限 AOT（预先编译）。已部署的程序在运行时不能进行 Lean 的精化（elaborate）、求值或编译，不能加载模块数据或插件，也不能使用 Lean 的 C++ 编译器/内核（确切列表）。证明、策略、宏和 #eval 照常在编译时运行。
• 仅限 Lean 4.35.0。其他 lean-toolchain 版本会被拒绝并显示提示信息。
• Node：请给应用至少 512 MB 内存；它预留约 22 GB 虚拟地址空间。无法链接预构建的原生库（-l、共享库）；软件包中自带的 C 源码会为你进行编译。
• Edge、Bun/Deno、浏览器、WASI：单线程 Lean；无套接字、进程或信号；除 WASI 外无文件。在浏览器中，阻塞等待会停止应用，除非它是为带有 JSPI 的浏览器使用 --suspend jspi 构建的；请使用 Async。
• 无预制绑定（针对 npm 软件包）；Lasm.Web 涵盖核心 Web 平台。
• 编辑器：在进行上述 npx lasm editor 操作后，编辑器中的 Lasm.* 导入才能解析。
• 平台：不支持 Windows ARM64 以及 Alpine/musl 构建机器（构建的应用可在 Alpine 上运行）。托管平台使用其本地工具进行测试，从不使用真实账户。

文档

• 开始：入门指南 · 所有文档 · 面向 AI 代理 · llms.txt
• 指南：服务器与 npm 互操作 · 无服务器与容器 · edge · Bun 和 Deno · 浏览器与 Lasm.UI · 全栈 (Lasm.RPC) · Lasm.Fetch · WASI 和 Fastly · 编辑循环
• 证据：基准测试 · 应用运行位置 · 语言覆盖率 · 兼容的 Lean 软件包 · 决策

支持 Lasm

如果 Lasm 对你有所帮助，或者你希望看到它成功，我将不胜感激你的赞助：github.com/sponsors/lastmjs。这支持了我以及针对 Lasm 和其他 Millillion 项目的工作。我的第一个目标是每月 250 美元，这足够为一个 Lasm 专用的 Claude Code 账户提供资金。你也可以通过给仓库点星、试用它以及报告崩溃问题来提供帮助。

参考

以下所有内容都是精确的契约：每个命令和选项、支持的机器和平台，以及已部署的 Lean 程序绝对无法执行的操作。

CLI 参考

使用 npm install -D @lasm/cli 在项目中安装（bin 为 lasm），或直接运行而无需安装：npx @lasm/cli Main.lean。npm create @lasm 运行相同 lasm init 版本的 @lasm/cli，参数保持不变。使用来自 快速入门 的 Main.lean：

npx lasm Main.lean                          # build (dev profile) and run: Hello from Lean! 2 + 3 = 5
npx lasm build Main.lean                    # write dist/ (release profile)
npx lasm --version                          # version, Lean, runtime and platform (for bug reports)
node dist/main.mjs                          # run the deployment: only Node is needed
npx lasm build Main.lean --target lambda    # dist/ and an AWS Lambda zip

--rebuild 和 --verbose 适用于运行和构建。--output 和 --target 仅用于 构建；-- 之后的参数仅用于运行。应用程序的退出状态会 予以保留。npx lasm --version（-v）打印版本、Lean 发行版、JavaScript 运行时和平台（请将其包含在错误报告中）。没有 install、clean 或 uninstall 子命令。

构建配置文件。两者使用相同的库链接相同的程序，且都是 确定性的。release（lasm build、lasm Main.lean --release）：完整的 Binaryen 大小优化；字节级可复现；用于部署的版本。dev （lasm Main.lean、lasm dev、lasm build --dev）：省略这些优化通道，并在 -O1 下编译您的模块；其行为相同，构建速度快几秒钟， 且其 program.wasm 大约大 15–20%。开发版重新构建从 项目的上一次构建开始，因此其字节可能取决于该次构建。build-info.json 记录了 "profile"。除非您传入 --allow-dev，否则 lasm package 和 lasm build --dev --target <platform> 会拒绝开发版构建。

环境变量（全部可选）：

源码中的其他 LASM_* 变量属于维护者诊断信息，并非受支持的 接口。

安装。 npm install @lasm/cli 通过您自己的注册表、代理和缓存，为您的平台将 Lean 和构建工具作为精确锁定的 @lasm/… npm 包引入。Lake/Lean-import 数据，以及仅针对包含 C 代码的 Lake 项目的 C 层（@lasm/lean-c-<platform>），在首次使用时通过您的 npm 获取。 终端会显示进度；后续构建会复用已验证的工具和未更改的输出。在一台没有下载缓存的新机器上，CI 运行器上的首次 Hono 构建耗时为 25.7 秒（Linux x64）、27.8 秒（Linux arm64）、44.4 秒（Windows）、58.7 秒（Apple Silicon）和 141.9 秒（Intel Mac） （构建时间，运行 40131930601）。 缓存位置与恢复：NODE_SUPPORT.md、 INSTALLATION_HARDENING.md。 仅当 Lake 项目具有 Git 或 Reservoir 依赖项时才需要 Git；Lasm 使用您 PATH 上的 git，并在缺少时提示如何安装。

现有的 Lake 项目可以直接在项目目录中使用 npx lasm build Main.lean 进行构建。在 lean-toolchain 中锁定 leanprover/lean4:v4.35.0；其他版本会被 Unsupported Lean toolchain … Lasm supports Lean v4.35.0 拒绝。按软件包列出的兼容性列表涵盖了 Batteries、Cli、LSpec、Plausible、Aesop、Qq、leansqlite、UnicodeBasic、MD4Lean、lean-zip、lean4-parser、lean-redis 等；未列出的软件包未经测试。

支持的环境

使用 Lasm（编译器）构建的机器：

Node 24 或更高版本（已测试：24.0.0、24.22.1、26.12.1）。无引擎标志。精确测试的产物：NODE_ACCEPTANCE.md。

支持的平台

Node dist/ 需要 Node 24 或更新版本（Node 22 及更早版本会通过 This application requires Node 24.0.0 or newer 终止）以及至少 512 MB 内存。它可在 Linux x64 和 arm64（glibc 2.28+ 或 musl/Alpine）上运行（这些平台可以由任何支持的平台构建，也可以在其自身的构建机器平台上运行）。复制 dist/ 的所有内容；那里不需要 Lean 源码、npm install 或构建工具。下方的每个平台都在 CI 中通过命名的本地运行时、镜像或模拟器进行了测试；均未使用真实的云账号。完整矩阵：DEPLOYMENT.md。

在 Windows 上构建并复制到 Linux（非通过 docker build 复制）的 dist/ 需要 chmod 755 dist/host/native/process/linux-*。Node 的 --jitless 无法工作（它会禁用 WebAssembly）。限制虚拟内存的主机（ulimit -v、vm.overcommit_memory=2）会拒绝需要预留约 22 GB 地址空间的 Node 构建。Node 26 的官方二进制文件在自行安装 tarball 的极简镜像上需要 libatomic1。

Lean 支持与限制

构建强制执行提前（ahead-of-time）执行。 支持普通函数、递归、闭包、归纳类型、模式匹配、类型类、依赖类型和编译后的 IO。导入、宏、 elaboration、tactic、deriving、证明和 #eval 在托管的 native Lean 中在编译期间运行。初始化程序算作运行时依赖项：宽泛的 import Lean 可能会保留编译器；当只有宏或 tactic 需要它时使用 meta import Lean，对于运行时数据库则使用更窄的导入（具有 Lean.Json 的 import Lean，以及 deriving ToJson, FromJson，构建并运行）。每一次拒绝都会有解释：Lasm 会打印从你的代码到编译器代码的链，当起因是宽泛的导入时，还会打印你的代码所使用的更窄的模块。部署的程序会像 native Lean 一样遵循 LEAN_ABORT_ON_NONLINEAR=1。各平台结果：language coverage。

部署的应用程序不能使用：

构建会检查可达的运行时依赖项，包括导入的库和间接调用；即使您的输入不会走该分支，可达的禁用调用也会被拒绝，并且链接器移除的死代码不计入内。在加载应用程序之前，启动程序还会拒绝丢失、陈旧或不兼容的功能记录（这是一个一致性检查，而不是安全沙箱）。不存在庞大的兼容性回退机制。

Lake 包。仅为编译而导入的模块（例如用于宏的战术、细化器，例如 Aesop、Qq 或 import Lean）不会将 Lean 编译器留在部署中。Lasm 仅在程序使用其定义或注册的内容时，或者当它们是程序自身编写的代码执行 IO 或调用 C 时（--verbose 显示了跳过了多少个），才会运行模块的初始化程序。包捆绑的 C 源代码（extern_lib、moreLinkObjs，例如 leansqlite 的 SQLite）使用 Lean 自己的 clang 进行编译，作为 C 层获取一次（39–52 MB）；不需要系统的 C 编译器（macOS 需要用于 C 库头文件的 Xcode Command Line Tools SDK）。无法链接预构建的原生库（共享库、-l 选项：libcurl、OpenSSL、libpq、BLAS）；构建会指明库和包的名称。

非发布保证。控制台输出、参数、退出码、本地 Lake 导入以及选定的语言/文件系统测试拥有原生与 Node 的对比测试，并且在 0.1.0 之前，Lean 具备运行时能力的上游套件和 19 个生态系统项目在所有五个平台上运行，与上一个接受的候选版本相比零回归（0.1.0 门禁）。不保证完整的 IO.FS、并发性、子进程/信号/终端奇偶校验、每个第三方库以及完整的主流套件（IO 差距）。大数字（超出 63 位的 Nat/Int）使用 Lean 自己的任意精度代码来代替 GNU MP，因此应用不包含 LGPL 代码；结果与原生 Lean 相同，但在 Wasm 中，在 1,000 位时，乘法比使用 GMP 慢约 5 倍，Nat.gcd 慢约 60 倍（数字）。Lake 依赖项使用您的系统 Git（系统 Git）。

发布版本与来源

0.1.0 是第一个 npm 版本（说明）；0.2.0 添加了边缘目标和 Bun/Deno（说明）；0.3.0 添加了浏览器、Lasm.UI、全栈应用、WASI/Fastly 和编辑器支持（说明）；0.3.1 将启动代码置于 MIT-0 许可证下并添加了错误报告指针（说明）；0.3.2 修复了 Std.Internal.UV 套接字、定时器和信号（说明）；0.3.3 从未发布，其更改随 0.3.4 发布（说明）；0.3.5 更新了 README 和 Conduit 示例（说明）。Lasm 的 npm 包（@lasm/cli、@lasm/create 和 @lasm/… 工具包）仅通过 release.yml 工作流发布，通过带有来源证明的 npm 可信发布：不存在 npm 令牌。一个发布版本是一个提升 package.json 版本的拉取请求（pull request），并且只有在发布提交的 release-checks 状态（五平台候选检查；边缘、Bun/Deno、浏览器、Lasm.UI、WASI/Fastly、全栈、单元和开发循环检查；以及确切包的 npm 排练）通过后才会发布。发现了 Bug？npx lasm --version 提供了bug 报告表单所要求的版本行。npm view @lasm/cli@<version> 显示了来源证明，项目中的 npm audit signatures 可以对其进行验证。详情：RELEASING.md。

许可协议

Lasm 的源码采用 MIT License（版权所有 Jordan Last）。 初始代码——在新建项目中放入的一切 lasm init 和 npm create @lasm、templates/、examples/，以及本 README 和 docs/ 中的代码示例——在所有版本中同样采用 MIT No Attribution (MIT-0)：它们完全归你所有，无需署名。@lasm/create 采用 MIT，并且 @lasm/cli 的 license 字段是 Lasm 的 MIT、MIT-0 及其打包的所有组件的 SPDX 表达式，其文本位于 licenses/ 中。许可证审计列出了每个发布的组件、其许可证以及各项义务的履行方式。

• 构建 dist/。 THIRD_PARTY_NOTICES.txt 以 Lasm 的 MIT 声明以及 Lasm 修改的 Lean 文件列表开头，随后是构建所包含内容的许可证：Lean 的运行时与标准库（Apache-2.0）、Emscripten（MIT OR NCSA）、musl、LLVM libc++、libc++abi、libunwind 和 compiler-rt、mimalloc、libuv、koffi 以及 Lasm 的宿主（MIT）。应用不包含任何 copyleft 代码。licenses/<package>/ 保存了编译进 program.wasm 的所有 Lake 依赖项的许可证文件；通过 npm 互操作，node_modules/ 保存了带有各自许可证的每个软件包。当你分发 dist/ 时，请保留这些文件。
• Edge、浏览器、WASI、Fastly 和 wasi-http 输出采用相同的声明，经自动重写以说明其文件包含的内容：每个输出目录中的一个 THIRD_PARTY_NOTICES.txt、平台捆绑的 JavaScript 上的简短 /*! … */ 许可证横幅（edge 胶水代码、浏览器加载器）、位于服务器端输出的 Wasm 内部的完整声明文件（一个 lasm.notices 自定义节，因此它会随每次部署一起传输）、Fastly 软件包中的文件，以及 Vite 构建中的 THIRD_PARTY_NOTICES.lasm.txt。这对你的应用意味着什么：docs/LICENSING.md。
• 工具包与发布归档。每个 @lasm/… 工具包都包含一个 SPDX license 字段和归档的许可证文件。Lean 归档包含的 (L)GPL 部分（GNU MP、GNU C 库、GCC 运行时库、Linux UAPI 头文件、MinGW-w64）以及 Lean 自身源码的具体来源，均作为发布它们的发行版的资产进行镜像（lean-4.35.0-tiers-v2）。 Lasm 不发布任何 Git 和 Apple SDK 文件。
• Lean 名称和标志是 Lean FRO 的商标。Lasm 与 Lean FRO 无隶属关系，亦未经其背书。