mm0-rs

这是 mm0-hs 的 MM1 服务器的一个替代实现，使用 Rust 编写。 mm0-rs 服务器 作为 LSP 服务器的方式与 mm0-hs 服务器 相同，这意味着如果您已安装 vscode-mm0 扩展，可以选择任意一个程序作为您的 LSP 服务器，它将提供实时诊断、转到定义支持、悬停等功能。它不支持其他所有命令（暂时！）如 mm0-hs verify 或 mm0-hs from-mm，但作为语言服务器比 Haskell 实现要快得多，同时支持类似的功能。

请关注这个空间以获取更多更新，因为 mm0-rs 正在积极开发。有关 MM1 规范的描述，请参阅 mm1.md，该规范由 mm0-hs 和 mm0-rs 实现。

编译

要编译 mm0-rs，首先 安装 Rust。然后需要下载此仓库（例如，git clone https://github.com/digama0/mm0.git）。然后进入此 mm0-rs 目录（使用 cd mm0/mm0-rs）并运行

cargo build --release

然后应该使执行变得容易。一种方法是复制或创建符号链接到生成的可执行文件 target/release/mm0-rs 到您的系统路径中。如果如以下建议那样与 Visual Studio Code 集成，另一种选择是将 vscode-mm0 指向可执行文件，使用（如以下所述）设置 "metamath-zero.executablePath": "mm0-rs" 在您的 settings.json 文件中。

与 Visual Studio Code 集成

我们通常使用 Visual Studio Code，这是一个支持 LSP 服务器功能的开源软件编辑器/IDE。如果您选择这样做，请下载并安装 Visual Studio Code。

接下来，安装 "Metamath Zero" 语言支持扩展。您可以通过以下两种方式之一完成此操作

1. 使用快速打开（在 Windows/Linux 上按 Ctrl-P，在 MacOS 上按 Cmd-P），在框中粘贴 ext install digama0.metamath-zero 并按 Enter（Return）。这将安装 "Metamath Zero" 语言支持 扩展。
2. 选择“查看/扩展”，搜索“Metamath”。查找“Metamath Zero”；确保它是正确的（digama0.metamath-zero）。如果是，按其“安装”按钮。

如果 mm0-rs 不在您的路径中，那么您需要更改 Visual Studio Code 的设置，以便它可以执行 mm0-rs。为此，在您安装了 "Metamath Zero" 之后，查看其名称，点击其小的“齿轮符号”以更改其设置。注意：如果您点击其“齿轮符号”而看不到任何内容，这是 Visual Studio Code 程序中的错误；重新启动它，然后选择“查看/扩展”，以便您可以看到设置以更改它们。现在修改“Metamath-zero Executable Path”设置（对应于 metamath-zero.executablePath 在 settings.json 中）为正确的可执行文件路径（默认为 mm0-rs）。您可能需要使用绝对路径（例如，以 "/" 开头的 Linux/Unix/MacOS 路径）。

使用方法

如果直接调用 mm0-rs 程序，它提供了一些模式和选项。例如

• mm0-rs server 会使它通过 stdin 和 stdout 发送和接收 LSP 服务器命令。这不是直接从 CLI 使用，而是由 vscode-mm0 调用，当它设置为使用 mm0-rs 作为语言服务器时。
• mm0-rs server --debug 由 vscode-mm0 在扩展本身以调试模式运行时执行，这将启用回溯和日志记录。
• mm0-rs compile foo.mm1 将编译一个 MM1 文件，将错误报告到控制台。这基本上是 server 模式的控制台版本。

您可以从 Visual Studio Code 内部轻松使用 mm0-rs。启动 Visual Studio Code，然后使用“文件/打开”，导航到 mm0/examples 目录。选择要查看的文件；《code>do-block.mm1 和 demo.mm1 是好的起点（demo.mm1 显示 MM1 中证明的样子）。选择“查看/问题”以查看摘要。

有关如何使用MM1创建证明的更多信息，请参阅文件 ../mm0-hs/mm1.md（mm0-hs工具已弃用，但MM1文档目前仍在那里）。