mm0-rs

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

请关注这个空间以获取更多更新，因为 mm0-rs 正在积极开发中。请参阅 mm1.md 以了解 MM1 规范的描述，该规范由 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 指向可执行文件：在您的 settings.json 文件中设置 "metamath-zero.executablePath": "mm0-rs"。

与 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" 设置（在 settings.json 中对应于 metamath-zero.executablePath）以成为可执行文件的正确路径（默认为 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目录。选择一个文件进行查看；do-block.mm1和demo.mm1是良好的起点（demo.mm1显示了MM1中的证明看起来是什么样子）。选择“查看/问题”以查看摘要。

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