Improve rustfmt.toml support (#51)

This PR does a few things related to `rustfmt.toml`, categorized into
stuff that is user-facing, and library API changes.

### User-Facing Changes

* Improve handling of `rustfmt.toml` for non-`verus!` code
- Rather than picking up `rustfmt.toml` based on working directory, it
is now picked up based on the file being formatted. This now matches the
search that `rustfmt` itself does.

### Public verusfmt-as-library API

* Remove `parse_and_format` from the public library API
  - The intended usage is now the more extensible `verusfmt::run`
* Add support for passing in an explicit `rustfmt.toml` via the public
library API

CHANGELOG.md

@@ -1,5 +1,8 @@
 # Unreleased
 
+* Improve handling of `rustfmt.toml` for non-`verus!` code
+  - Rather than picking up `rustfmt.toml` based on working directory, it is now picked up based on the file being formatted. This now matches the search that `rustfmt` itself does.
+
 # v0.2.10
 
 * Add support for `broadcast proof`, `broadcast group`, and `broadcast use` (see [verus#1022](https://github.com/verus-lang/verus/pull/1022))

Cargo.toml

@@ -29,6 +29,7 @@ pest_derive = "2.0"
 pretty = "0.12.1"
 regex = "1.9.6"
 similar = "2.2.1"
+tempfile = "3.10.1"
 thiserror = "1.0.52"
 tracing = "0.1.37"
 tracing-subscriber = { version = "0.3.17" }

examples/verus-snapshot/get_latest.sh

@@ -12,7 +12,7 @@ wget --quiet -O verus.zip https://github.com/verus-lang/verus/archive/refs/heads
 echo "[INFO] Unzipping Verus"
 unzip -q verus.zip
 
-MOVE_PATHS="source/rust_verify/example/syntax.rs source/vstd"
+MOVE_PATHS="source/rustfmt.toml source/rust_verify/example/syntax.rs source/vstd"
 
 echo "[INFO] Moving files"
 for path in $MOVE_PATHS; do

examples/verus-snapshot/source/rustfmt.toml

@@ -0,0 +1,7 @@
+# Copied from Rust compiler's rustfmt.toml settings
+
+# Run rustfmt with this config (it should be picked up automatically).
+# unstable_features=true # provided by vargo
+# version=Two # provided by vargo
+use_small_heuristics = "Max"
+merge_derives = false

examples/verus-snapshot/source/vstd/source/vstd/atomic.rs

@@ -471,13 +471,7 @@ macro_rules! atomic_bool_methods {
     };
 }
 
-make_bool_atomic!(
-    PAtomicBool,
-    PermissionBool,
-    PermissionDataBool,
-    AtomicBool,
-    bool
-);
+make_bool_atomic!(PAtomicBool, PermissionBool, PermissionDataBool, AtomicBool, bool);
 
 make_unsigned_integer_atomic!(
     PAtomicU8,

examples/verus-snapshot/source/vstd/source/vstd/atomic_ghost.rs

@@ -114,33 +114,15 @@ declare_atomic_type!(AtomicU64, PAtomicU64, PermissionU64, u64, AtomicPredU64);
 declare_atomic_type!(AtomicU32, PAtomicU32, PermissionU32, u32, AtomicPredU32);
 declare_atomic_type!(AtomicU16, PAtomicU16, PermissionU16, u16, AtomicPredU16);
 declare_atomic_type!(AtomicU8, PAtomicU8, PermissionU8, u8, AtomicPredU8);
-declare_atomic_type!(
-    AtomicUsize,
-    PAtomicUsize,
-    PermissionUsize,
-    usize,
-    AtomicPredUsize
-);
+declare_atomic_type!(AtomicUsize, PAtomicUsize, PermissionUsize, usize, AtomicPredUsize);
 
 declare_atomic_type!(AtomicI64, PAtomicI64, PermissionI64, i64, AtomicPredI64);
 declare_atomic_type!(AtomicI32, PAtomicI32, PermissionI32, i32, AtomicPredI32);
 declare_atomic_type!(AtomicI16, PAtomicI16, PermissionI16, i16, AtomicPredI16);
 declare_atomic_type!(AtomicI8, PAtomicI8, PermissionI8, i8, AtomicPredI8);
-declare_atomic_type!(
-    AtomicIsize,
-    PAtomicIsize,
-    PermissionIsize,
-    isize,
-    AtomicPredIsize
-);
-
-declare_atomic_type!(
-    AtomicBool,
-    PAtomicBool,
-    PermissionBool,
-    bool,
-    AtomicPredBool
-);
+declare_atomic_type!(AtomicIsize, PAtomicIsize, PermissionIsize, isize, AtomicPredIsize);
+
+declare_atomic_type!(AtomicBool, PAtomicBool, PermissionBool, bool, AtomicPredBool);
 
 /// Performs a given atomic operation on a given atomic
 /// while providing access to its ghost state.

examples/verus-snapshot/source/vstd/source/vstd/std_specs/num.rs

@@ -165,20 +165,8 @@ num_specs!(u8, i8, u8_specs, i8_specs, 0x100);
 num_specs!(u16, i16, u16_specs, i16_specs, 0x1_0000);
 num_specs!(u32, i32, u32_specs, i32_specs, 0x1_0000_0000);
 num_specs!(u64, i64, u64_specs, i64_specs, 0x1_0000_0000_0000_0000);
-num_specs!(
-    u128,
-    i128,
-    u128_specs,
-    i128_specs,
-    0x1_0000_0000_0000_0000_0000_0000_0000_0000
-);
-num_specs!(
-    usize,
-    isize,
-    usize_specs,
-    isize_specs,
-    (usize::MAX - usize::MIN + 1)
-);
+num_specs!(u128, i128, u128_specs, i128_specs, 0x1_0000_0000_0000_0000_0000_0000_0000_0000);
+num_specs!(usize, isize, usize_specs, isize_specs, (usize::MAX - usize::MIN + 1));
 
 verus! {
 

src/lib.rs

@@ -3,7 +3,7 @@
 
 mod rustfmt;
 
-pub use crate::rustfmt::rustfmt;
+pub use crate::rustfmt::{rustfmt, RustFmtConfig};
 
 use itertools::Itertools;
 use pest::{iterators::Pair, iterators::Pairs, Parser};
@@ -1514,7 +1514,7 @@ impl miette::Diagnostic for ParseAndFormatError {
     }
 }
 
-pub fn parse_and_format(s: &str) -> miette::Result<String> {
+fn parse_and_format(s: &str) -> miette::Result<String> {
     let ctx = Context {
         inline_comment_lines: find_inline_comment_lines(s),
     };
@@ -1596,13 +1596,16 @@ pub struct RunOptions {
     pub file_name: Option<String>,
     /// Whether to run rustfmt on non-verus parts of code.
     pub run_rustfmt: bool,
+    /// Whether to perform extra configuration for the rustfmt run. Ignored if `run_rustfmt` is false.
+    pub rustfmt_config: RustFmtConfig,
 }
 
 impl Default for RunOptions {
     fn default() -> Self {
         Self {
             file_name: None,
             run_rustfmt: true,
+            rustfmt_config: Default::default(),
         }
     }
 }
@@ -1622,7 +1625,9 @@ pub fn run(s: &str, opts: RunOptions) -> miette::Result<String> {
     let formatted_output = if !opts.run_rustfmt {
         verus_fmted
     } else {
-        rustfmt(&verus_fmted).ok_or(miette::miette!("rustfmt failed"))?
+        opts.rustfmt_config
+            .run(&verus_fmted)
+            .ok_or(miette::miette!("rustfmt failed"))?
     };
 
     Ok(formatted_output)