Skip to content

feat: delegate fmt to cargo verus fmt #47

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Marsman1996 merged 1 commit into from
Oct 3, 2026
Merged

feat: delegate fmt to cargo verus fmt #47

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
52 changes: 0 additions & 52 deletions Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 0 additions & 1 deletion Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,6 @@ dotenv = { version = "*" }
log = { version = "*" }
log4rs = { version = "*", features = ["gzip"] }
walkdir = { version = "*" }
rayon = { version = "*" }
toml_edit = { version = "*" }

syn = { version = "2", features = ["full", "extra-traits"] }
Expand Down
190 changes: 39 additions & 151 deletions src/format.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,82 +1,22 @@
use cargo_metadata::MetadataCommand;
use memoize::memoize;
use rayon::prelude::*;
use std::{
collections::HashSet,
path::{self, PathBuf},
process::Command,
};
use walkdir::WalkDir;

use crate::{executable, helper::DynError, verus};

const VERUSFMT_MIN_EDITION_VERSION: &str = "0.7.2";
const VERUSFMT_MIN_EDITION_VERSION: &str = "0.7.4";
const VERUSFMT_EDITION: &str = "2024";

fn get_verusfmt_path() -> Result<PathBuf, DynError> {
executable::locate(verus::VERUSFMT_BIN, None, &Vec::<PathBuf>::new()).ok_or(
"Cannot find the Verusfmt binary, please install it by running `cargo dv bootstrap`".into(),
)
}

fn collect_rust_files_from_dir(dir: &std::path::Path) -> Vec<PathBuf> {
WalkDir::new(dir)
.into_iter()
.filter_map(|entry| {
let path = entry.ok()?.path().to_path_buf();
if path.is_file() && path.extension().map_or(false, |ext| ext == "rs") {
Some(path)
} else {
None
}
})
.collect()
}

fn run_formatter_on_files(files: &[PathBuf], formatter: &str, formatter_path: Option<&PathBuf>) {
println!("Running {} on {} files...", formatter, files.len());
files.par_iter().for_each(|file| {
println!("Formatting file: {}", file.display());

let mut cmd = if let Some(path) = formatter_path {
Command::new(path)
} else {
Command::new(formatter)
};

if formatter == "verusfmt" {
cmd.args(["--edition", "2024"]);
}

let output = cmd.arg(file).output();

match output {
Ok(output) if output.status.success() => {}
Ok(output) => {
if formatter == "rustfmt" {
eprintln!("Warning: {} failed for file: {}", formatter, file.display());
print_command_output(&output.stdout, &output.stderr);
} else if verusfmt_refused_edition_arg(&output.stdout, &output.stderr) {
eprintln!(
"verusfmt failed because it does not support `--edition`. Please update verusfmt to >= {}.",
VERUSFMT_MIN_EDITION_VERSION
);
} else {
eprintln!("Failed to format file: {}, skipping", file.display());
print_command_output(&output.stdout, &output.stderr);
}
}
Err(e) => {
eprintln!(
"Warning: Could not run {} on {}: {}",
formatter,
file.display(),
e
);
}
}
});
}

fn print_command_output(stdout: &[u8], stderr: &[u8]) {
if !stdout.is_empty() {
eprint!("{}", String::from_utf8_lossy(stdout));
Expand All @@ -102,70 +42,50 @@ fn verusfmt_refused_edition_arg(stdout: &[u8], stderr: &[u8]) -> bool {
|| output.contains("invalid argument"))
}

fn run_rustfmt_on_files(files: &[PathBuf]) {
run_formatter_on_files(files, "rustfmt", None);
}

fn run_verusfmt_on_files(files: &[PathBuf], verusfmt: &PathBuf) {
run_formatter_on_files(files, "verusfmt", Some(verusfmt));
}

pub fn format_vostd(targets: &Vec<String>) {
let verusfmt = match get_verusfmt_path() {
Ok(path) => path,
Err(e) => {
eprintln!("{}", e);
std::process::exit(1);
}
};

// Read the cargo metadata for all files
let metadata = MetadataCommand::new()
.no_deps()
.exec()
.expect("Failed to get cargo metadata");
/// Format workspace packages by delegating to `cargo verus fmt`, one
/// invocation per package so a failing one does not stop the rest.
pub fn format_packages(targets: &Vec<String>) -> Result<(), DynError> {
let verusfmt = get_verusfmt_path()?;

// Filter packages based on the provided targets
let fmt_packages = if targets.is_empty() {
metadata.packages
// The given targets, or all workspace members.
let mut packages: Vec<String> = if targets.is_empty() {
get_all_targets().into_iter().collect()
} else {
metadata
.packages
.into_iter()
.filter(|p| targets.contains(&p.name))
.collect::<Vec<_>>()
targets.clone()
};

for package in fmt_packages {
for target in &package.targets {
let path = &target.src_path;
let src_dir = path.parent().unwrap().as_std_path();
let rust_files = collect_rust_files_from_dir(src_dir);
run_verusfmt_on_files(&rust_files, &verusfmt);
}

if package.name == "ostd" {
let specs_dir = package.manifest_path.parent().unwrap().join("specs");
if specs_dir.exists() {
let rust_files = collect_rust_files_from_dir(specs_dir.as_std_path());
run_rustfmt_on_files(&rust_files);
run_verusfmt_on_files(&rust_files, &verusfmt);
packages.sort();

let cargo_verus = verus::get_cargo_verus(true);
for package in &packages {
println!("Running `cargo verus fmt -p {}`...", package);

// verusfmt defaults to edition 2021; this repo is formatted with 2024.
let output = Command::new(&cargo_verus)
.arg("fmt")
.arg("-p")
.arg(package)
.env("VERUSFMT", &verusfmt)
.args(["--", "--edition", VERUSFMT_EDITION])
.output()?;

if !output.status.success() {
if verusfmt_refused_edition_arg(&output.stdout, &output.stderr) {
eprintln!(
"verusfmt failed because it does not support `--edition`. Please update verusfmt to >= {}.",
VERUSFMT_MIN_EDITION_VERSION
);
} else {
eprintln!(
"Warning: `cargo verus fmt -p {}` failed on some files, skipping them.",
package
);
}
}
}
}

pub fn run_cargo_fmt(targets: &Vec<String>) {
let mut cmd = Command::new("cargo");
cmd.arg("fmt");

if !targets.is_empty() {
for target in targets {
cmd.arg("--package").arg(target);
print_command_output(&output.stdout, &output.stderr);
}
}

cmd.status().expect("Failed to run cargo fmt");
println!("Formatting complete!");
Ok(())
}

#[memoize]
Expand Down Expand Up @@ -201,35 +121,3 @@ pub fn target_parser(s: &str) -> Result<String, String> {
Err(format!("Unknown target: {}", s))
}
}

pub fn format_paths(paths: &[PathBuf]) -> Result<(), DynError> {
let mut rust_files = Vec::new();

for path in paths {
if !path.exists() {
eprintln!("Warning: Path does not exist: {}", path.display());
continue;
}

if path.is_file() {
if path.extension().map_or(false, |ext| ext == "rs") {
rust_files.push(path.clone());
}
} else if path.is_dir() {
rust_files.extend(collect_rust_files_from_dir(path));
}
}

if rust_files.is_empty() {
println!("No Rust files found in the specified paths.");
return Ok(());
}

run_rustfmt_on_files(&rust_files);

let verusfmt = get_verusfmt_path()?;
run_verusfmt_on_files(&rust_files, &verusfmt);

println!("Formatting complete!");
Ok(())
}
19 changes: 1 addition & 18 deletions src/main.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
use clap::{ArgAction, Parser, Subcommand};
use colored::Colorize;
use rust_dv::helper::*;
use std::path::PathBuf;

#[derive(Parser, Debug)]
#[command(
Expand Down Expand Up @@ -440,11 +439,6 @@ struct FmtArgs {
help = "The targets to format", num_args = 0..,
action = ArgAction::Append)]
targets: Vec<String>,

#[arg(short = 'p', long = "paths",
help = "Specific file or directory paths to format", num_args = 0..,
action = ArgAction::Append)]
paths: Vec<PathBuf>,
}

fn cargo_feature_args(features: &clap_cargo::Features) -> Vec<String> {
Expand Down Expand Up @@ -574,18 +568,7 @@ fn show_item(args: &ShowItemArgs) -> Result<(), DynError> {
}

fn format(args: &FmtArgs) -> Result<(), DynError> {
if !args.paths.is_empty() {
// Format specific paths
format::format_paths(&args.paths)?;
} else {
// Format by targets (existing behavior)
// do `cargo fmt` before verusfmt
format::run_cargo_fmt(&args.targets);

// format the source code of vostd
format::format_vostd(&args.targets);
}
Ok(())
format::format_packages(&args.targets)
}

fn main() {
Expand Down
Loading