Verusfmt

Verus代码的意见性格式化工具。

更新verusfmt

如果你已经安装了预构建的二进制文件，你可以使用以下方式更新到最新版本：

verusfmt --update

安装和使用Verusfmt

我们支持多种安装方法。使用以下方式获取最新版本：

• 预构建的二进制文件（推荐）

  • Linux/MacOS（点击展开）

    curl --proto '=https' --tlsv1.2 -LsSf https://github.com/verus-lang/verusfmt/releases/latest/download/verusfmt-installer.sh | sh
    

  • Windows（点击展开）

    powershell.exe -ExecutionPolicy RemoteSigned -c "irm https://github.com/verus-lang/verusfmt/releases/latest/download/verusfmt-installer.ps1 | iex"
    

• cargo install（点击展开）

  cargo install verusfmt --locked
  

这些将安装verusfmt二进制文件。然后你可以使用以下方式在文件上运行它：

verusfmt foo.rs

查看verusfmt --help以获取更多选项和详细信息。

目标

1. 通过自动以一致的风格格式化代码，使阅读和贡献Verus代码更容易（额外的好处：消除关于风格的令人沮丧的争论）。
2. 生成可接受的“美观”输出。
3. 运行速度快！verusfmt可以用于预提交脚本、CI等，因此不能慢。
4. 保持代码相对简单。漂亮的打印机是最难编写的程序之一，所以我们试图采取措施减少这种难度，以便verusfmt可以以合理的努力进行更新和修改。

常见问题解答

1. 为什么不针对rustfmt进行Verus习惯的修改？

   尽管Verus拥有类似Rust的语法，但它必然也会偏离它以自然地支持其惯用语，因此不仅需要更新rustfmt的解析器，还需要对生成器进行仔细的更改，以便代码看起来自然。此外，由于几乎所有Verus代码都位于verus!{}宏（而rustfmt并不容易支持宏内即使是常规Rust的格式化），需要付出相当大的努力才能进行管道和维护工作，以同时支持在verus!{}宏（作为Rust代码）之外进行格式化，同时也在宏内部格式化Verus代码。

2. verusfmt与rustfmt在verus!{}宏之外对代码的处理是否一致？

   是的，默认情况下，verusfmt处理宏内部的代码，并运行rustfmt来处理宏之外的代码。两者不应互相冲突或覆盖彼此的格式化更改。这使得对较大未验证的Rustcrate内的少量代码进行增量验证变得更容易。您可以使用--verus-only禁用对rustfmt的调用。

3. 为什么不将此作为Verus的一个功能来构建呢？

   当Verus从rustc接收到AST时，我们已丢失关于空白和注释的信息，这意味着我们无法在重新格式化的代码中保留注释。此外，仅仅为了格式化一些代码就启动整个rustc似乎很重。

未来工作

• 为常用宏（如println!，state_machine!）进行特殊处理
• 强制执行Rust命名策略？

非未来工作

• 我们目前没有计划像rustfmt那样对use声明进行排序
• 我们不打算解析Verus本身无法解析的代码。有时verusfmt会意外地解析此类代码，但这并非故意为之，也不能依赖。
• 与rustfmt生成的格式完全匹配
• 完美处理注释——它们出奇地难以处理！

设计概述

我们的设计深受上述目标的影响。我们不是从头开始编写一切（这是一项臭名昭著的艰巨任务），而是使用解析器生成器来读取Verus源代码，并在输出时使用一个漂亮的打印库来格式化它。我们试图使每个阶段尽可能高效，并且我们主要尝试使格式化器无状态，出于性能原因，但更重要的是，试图使代码合理简单且易于推理。因此，为了简单起见，我们有时会偏离Rust的样式指南。

解析

我们使用这个语法定义Verus源代码的语法，它由Pest解析器生成器处理，该生成器依赖于解析表达式语法（PEG）。这使得我们可以方便地定义空白和注释的概念，其余规则可以忽略它们；Pest将隐式处理它们。我们明确忽略verus!宏之外的代码，将其留给rustfmt处理。我们更喜欢使用显式规则来定义字符串常量，因为它允许在格式化代码时具有更统一的风格。在某些地方，我们对同一个Verus构造有多个定义，以便根据上下文以不同的方式对其进行格式化（例如，参见attr_core）。许多规则都是为了遵循Rust参考中的相应描述而设计的。

格式化

我们不是尝试自己格式化内容，而是依赖于基于Philip Wadler设计的美观打印器pretty软件包。核心思想是创建一组可能的代码布局，然后美观打印器使用其内部启发式算法来选择最漂亮的版本。通常这意味着我们指定在代码需要放置在多行时，换行符可以出现在何处，但你也可以使用group运算符来说明，对于特定的代码片段，美观打印器还应该考虑将组中的每一行都放在一行上。

在尽可能的情况下，我们通过安排节点格式化是通过简单地格式化其每个子节点来计算的，来尽量保持格式化器简单。有时这需要将解析器中的节点拆分，以便可以根据上下文以两种不同的方式格式化相同的项。跟踪Rust上下文可能很棘手（因为Rust允许在语句中使用表达式，在表达式中使用语句），所以我们尽量使格式化器无状态，以减少错误的可能性。

贡献

我们欢迎贡献！请继续阅读以获取详细信息。

如果您向verusfmt提供Verus接受的代码，但verusfmt要么不接受/解析它，要么生成Verus不接受（或与原始代码有不同的语义）的代码，我们认为这是verusfmt的一个错误。当这种情况发生时，请打开一个GitHub问题，其中包含格式化前后违规代码的最小示例。

如果verusfmt生成了有效的代码，但您不喜欢格式，请打开一个GitHub pull request，其中包含您的提议更改和这些更改的理由。请确保现有的测试用例仍然通过（以下有更多详细信息），除非您的目标是更改处理某些测试用例的方式。请还包括新的/更新的测试用例，以测试您的提议更改。

开发修复或改进的技巧

1. 编写一个小的.rs文件，专注于您想要改进的特定内容。在格式化之前和之后，在简化的示例上测试verusfmt，以确保问题仍然存在；使用--check运行这个过程非常有帮助。示例文件越小，后续步骤就越容易。
2. 当使用--check运行时，您还可以添加-dd来查看第2级调试输出，这包括解析树。查看解析树并识别与您的特定示例相关的规则。
3. 一旦找到相关规则名称，如果问题似乎是错误解析，请转到src/verus.pest以找到相关规则并查看语法是否需要修复或改进。
4. 如果解析没有问题但打印有问题，那么请查找src/lib.rs中的to_doc函数中的相关规则。这可能有点难以立即理解，所以随时查阅pretty文档非常有帮助。此外，查看相关的调试打印（使用-d或-dd）也很有用，它提供了在优化之前递归展开的doc的序列化版本，因此确定哪个部分不符合您的期望非常有帮助。
5. 尝试修复，直到小示例成功。
6. 将示例添加到测试中——请参阅下面的测试部分。
7. 如果修复小示例中的规则成功但破坏了其他测试，您可能需要将解析语法中的相关规则拆分为两个独立的案例，以便每个案例可以独立格式化。例如，请参阅comma_delimited_exprs_for_verus_clauses和groupable_comma_delimited_exprs_for_verus_clauses。

测试

Rust-like格式化

通常，我们努力遵守Rust的风格指南。此类遵守的测试位于tests/rustfmt-matching.rs中。这些测试将比较rustfmt和verusfmt的输出。您可以通过cargo test运行它们。

Verus-like格式化

在多个地方，我们偏离了Rust的风格，要么是为了简化格式化器，要么是为了处理Verus特定的语法。此类格式化代码的测试位于tests/verus-consistency.rs中。您可以通过编写/更改输入代码添加新测试或修改现有测试。测试的正确答案通过Insta测试框架维护。

Insta建议安装cargo-insta工具以获得改进的审查体验。

cargo install cargo-insta

您可以使用cargo test正常运行测试，但通常更方便通过

cargo insta test
cargo insta review

或更简洁地

cargo insta test --review