jcreinhold/lean-fmt

# lean-fmt 一个用于 Lean 4 的格式化工具和 linter。 该格式化工具会将 Lean 源码重写为一种标准规范风格 (`docs/style.md`)；行宽是唯一的设置项。 在任何结果被报告或写入之前，都会对结果重新进行解析，并与原始内容逐 token 进行比对检查 —— 任何未通过检查的内容都会被拒绝，绝不会输出。linter 在此基础上增加了更多规则（重复和冗余的 import、未使用的变量、游离的 `set_option`、双向控制字符），其中一些支持自动修复。`lean-fmt rules` 会列出这些规则。 ## 安装说明 **预编译二进制文件** (Linux 和 macOS，x86-64 和 ARM)，安装至 `~/.local/bin`： ``` curl -sSfL https://raw.githubusercontent.com/jcreinhold/lean-fmt/main/install.sh | sh ``` `PREFIX` 和 `VERSION` 可覆盖安装路径和发布版本。暂无 Windows 构建版本；在 Windows 上请使用下文提到的 Lake 依赖。 **从源码构建** (使用 `PREFIX=/usr/local` 进行覆盖，使用 `DESTDIR` 进行暂存)： ``` git clone https://github.com/jcreinhold/lean-fmt.git cd lean-fmt make install ``` 如果 `PATH` 中存在 elan，首次构建时会安装指定的 toolchain。在运行时，`lean-fmt` 会使用*目标*项目自身的 Lean toolchain。`make uninstall` 会移除由 `make install` 安装的内容。 ## 快速开始 ``` lean-fmt check --root . # report findings, write nothing lean-fmt fix --root . # rewrite files in place, atomically lean-fmt diff --root . # preview formatting changes lean-fmt format --root . # format files in place, atomically ``` `check` 和 `diff` 不会写入任何内容；`format` 会以就地方式应用标准布局 (`--check` 用于预览而不实际写入)，而 `fix` 会应用规则修复，但不会重新排版布局。退出码 `0` 表示无误，`1` 表示发现问题，`2` 表示运行失败。`--json` 会在 stdout 打印一个 JSON 对象；统计信息会输出到 stderr。 其他命令：`organize` (标准化 import 头部)，`rules`，`lsp` (语言服务器)，`compiler setup`/`status`/`build` (插件)，`clean` (清除缓存)。可以通过 `lean-fmt --help` 列出指定命令的选项。 批量运行时，如果 stderr 是终端，则会显示 tqdm 风格的进度条；通过管道传输或使用 `--json` 时则不会显示该进度条。 结果会被缓存在 `.lean-fmt-cache/` 中；如果在一次完整的运行中没有任何更改，则会完全跳过 Lean 前端。`organize` 也会利用缓存：对于已经验证过的候选内容，既不会重新进行 elaboration 也不会再次拒绝；而它所发布输出的文件可以直接供下一次 `check` 或 `format` 使用。只有当存在消费者时——无论是当前目标的字节还是当前的 organize 候选内容——缓存条目才会被保留；否则在下一次写入时就会被丢弃；缓存没有大小上限。可以使用 `--no-cache` 禁用缓存。 `--workers N` 会针对大量文件并行执行冷启动运行；无论 N 为何值，报告的结果都是一致的。它默认使用 `LEAN_NUM_THREADS`，如果未设置，则使用机器的核心数——这与 Lake 用于自身构建的设置相同。 默认情况下，缓存条目的有效性会跟踪构建产物，因此任何重新构建——即使是仅涉及证明（proof-only）的构建——都会使依赖项失效。通过设置 `[cache] closure = "interface"` 并集成 compiler plugin，有效性将改为跟踪对 elaboration 可见的接口，此时仅涉及证明的重新构建将不再改变其有效性；请参阅 `docs/configuration.md` 了解导致默认值仍保留为 `"artifacts"` 的两个已知遗留问题。 ## 配置说明 此项为可选；如果没有配置文件，所有内容都将使用默认值进行检查。如需配置，请添加 `.lean-fmt.toml`： ``` exclude = ["Generated/**"] [format] line-width = 100 # the only style setting, 1..1000 [lint] select = ["all"] ignore = ["FMT004"] ``` 距离每个源文件**最近**的配置文件会对其进行管理；各配置文件之间不会合并。Git ignore 文件会得到遵循。未知的键和规则代码会引发错误。`lean-fmt config show PATH` 会打印出针对某个文件的有效设置及其来源。完整参考请见：`docs/configuration.md`。 ## 在其他项目中使用 lean-fmt 要作为 Lake 构建的一部分运行 lean-fmt，请添加该依赖（从源码构建；首次运行需要几分钟，之后 Lake 的缓存会使其不再产生额外开销）： ``` require «lean-fmt» from git "https://github.com/jcreinhold/lean-fmt" @ "v0.2.1" ``` ``` lake update «lean-fmt» # add it to the manifest lake exe lean-fmt check --root . ``` 如果你的项目保留了一些故意无法编译的文件（linter 测试用例、草稿笔记），lean-fmt 会将它们报告为 `broken`；请在 `.lean-fmt.toml` 中排除它们 (`docs/configuration.md`)。 要让 `lake lint` 运行它，在你的 package 中加入这两行（一个 package 只能有一个 lint 驱动；如果你已经有一个了，请保留它，并改为作为独立步骤运行 `lake exe lean-fmt check`）： ``` package myproject where lintDriver := "«lean-fmt»/«lean-fmt»" lintDriverArgs := #["check"] ``` （前后两部分都需要使用书名号（Guillemets）——因为 `lean-fmt` 不是一个合法的 Lean 标识符。） 一个可选的 compiler plugin 可以加快依赖语法的规则执行速度；如果不使用它，产出的检查结果也是相同的。关于安装、开销以及 CI 方案，请参见：`docs/ci.md`。 ## 编辑器 `lean-fmt lsp` 是一个语言服务器，除了 Lean 自带的服务器外，它还提供格式化、范围格式化、代码操作和诊断功能。针对 VS Code、Neovim 和 Emacs 的配置说明请见：`docs/editor-setup.md`。 ## 更多信息 - `docs/style.md` — 标准规范风格，包括 `format-ignore-next` 忽略指令。 - `docs/adding-a-rule.md` — 编写 lint 规则。 - `docs/toolchain-upgrade.md` — 维护者升级 toolchain 的检查清单。 - `docs/configuration.md` — 配置发现、选择门控、流式处理与范围、内存与 worker、缓存内部机制。 ## 开发说明 ``` lake build lake test # unit tier plus non-slow suites lake test -- --all # everything lake lint # the formatter on itself ```

标签：Lean, SOC Prime, 代码格式化, 开发工具, 语言服务器, 静态检查