From ff01be04a9c52804c73adf2e47c0c069ccb3c577 Mon Sep 17 00:00:00 2001 From: Hiroki Date: Mon, 10 Aug 2026 00:49:21 -0400 Subject: [PATCH 1/2] Support IRC11 Verus build arguments --- README.md | 21 +++++++++++- src/main.rs | 33 +++++++++++++++++++ src/verus.rs | 91 +++++++++++++++++++++++++++++++++++++--------------- 3 files changed, 118 insertions(+), 27 deletions(-) diff --git a/README.md b/README.md index 4830f54..6d88953 100644 --- a/README.md +++ b/README.md @@ -22,6 +22,26 @@ pre-commit = "run --manifest-path dv/Cargo.toml --bin pre_commit --" cargo dv verify --targets ... ``` +## Bootstrapping Verus + +By default, `cargo dv bootstrap` builds the `main` branch of +`asterinas/verus`. Use `--branch` to select another branch and repeat +`--build-arg` to pass additional arguments to that branch's `vargo build`. + +For example, the `irc11` branch requires its weak-memory vstd modules to be +enabled explicitly: + +```bash +cargo dv bootstrap --branch irc11 --build-arg=--vstd-weak-memory +``` + +The same arguments are honored by upgrades: + +```bash +cargo dv bootstrap --upgrade --branch irc11 \ + --build-arg=--vstd-weak-memory +``` + Optionally, if you want to use the pre-commit hook, you can add the rusty-hook to your project: ```bash @@ -37,4 +57,3 @@ pre-commit = "cargo pre-commit" [logging] verbose = true ``` - diff --git a/src/main.rs b/src/main.rs index 703e6b3..66eb57e 100644 --- a/src/main.rs +++ b/src/main.rs @@ -124,6 +124,15 @@ struct BootstrapArgs { value_name = "BRANCH_NAME" )] branch: Option, + + #[arg( + long = "build-arg", + help = "An extra argument passed to `vargo build` when building Verus", + value_name = "ARG", + action = ArgAction::Append, + allow_hyphen_values = true + )] + build_args: Vec, } #[derive(Parser, Debug)] @@ -470,6 +479,7 @@ fn bootstrap(args: &BootstrapArgs) -> Result<(), DynError> { release: !args.debug, restart: args.restart, branch: args.branch.clone(), + build_args: args.build_args.clone(), force_reset: args.upgrade, upstream_verus: args.upstream_verus, }; @@ -593,3 +603,26 @@ fn main() { error!("Error when executing command `{:?}`: {}", cli.command, e); } } + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn bootstrap_accepts_irc11_vargo_build_argument() { + let cli = Cli::try_parse_from([ + "dv", + "bootstrap", + "--branch", + "irc11", + "--build-arg=--vstd-weak-memory", + ]) + .unwrap(); + + let Commands::Bootstrap(args) = cli.command else { + panic!("expected bootstrap command"); + }; + assert_eq!(args.branch.as_deref(), Some("irc11")); + assert_eq!(args.build_args, ["--vstd-weak-memory"]); + } +} diff --git a/src/verus.rs b/src/verus.rs index c911cc5..20c7be5 100644 --- a/src/verus.rs +++ b/src/verus.rs @@ -1446,6 +1446,7 @@ pub mod install { pub restart: bool, pub release: bool, pub branch: Option, + pub build_args: Vec, pub force_reset: bool, pub upstream_verus: bool, } @@ -1720,50 +1721,72 @@ pub mod install { Ok(()) } + fn verus_build_args(release: bool, extra_args: &[String]) -> Vec { + let mut args = Vec::new(); + if release { + args.push("--release".to_string()); + } + args.extend(extra_args.iter().cloned()); + args.push("--features".to_string()); + args.push("singular".to_string()); + args + } + + fn run_build_command(cmd: &mut Command, description: &str) -> Result<(), DynError> { + debug!("{:?}", cmd); + let status = cmd.status()?; + if !status.success() { + return Err(format!("{} failed with status {}", description, status).into()); + } + Ok(()) + } + + #[cfg(target_os = "windows")] + fn powershell_quote(arg: &str) -> String { + format!("'{}'", arg.replace('\'', "''")) + } + #[cfg(target_os = "windows")] - pub fn build_verus(release: bool) -> Result<(), DynError> { + pub fn build_verus(release: bool, extra_args: &[String]) -> Result<(), DynError> { + let build_args = verus_build_args(release, extra_args); + let quoted_args = build_args + .iter() + .map(|arg| powershell_quote(arg)) + .collect::>() + .join(" "); let mut cmd = executable::get_powershell_command()?; cmd.current_dir(verus_source_dir()).arg("/c").arg(format!( - "& '..\\tools\\activate.ps1'; vargo build {} --features singular", - if release { "--release" } else { "" } + "& '..\\tools\\activate.ps1'; vargo build {}", + quoted_args )); - debug!("{:?}", cmd); - cmd.status().unwrap_or_else(|e| { - error!("Failed to build verus: {}", e); - }); + run_build_command(&mut cmd, "Verus build")?; let mut verusdoc_cmd = executable::get_powershell_command()?; verusdoc_cmd .current_dir(verus_source_dir()) .arg("/c") .arg("& '..\\tools\\activate.ps1'; vargo build -p verusdoc"); - debug!("{:?}", verusdoc_cmd); - verusdoc_cmd.status().unwrap_or_else(|e| { - error!("Failed to build verusdoc: {}", e); - }); + run_build_command(&mut verusdoc_cmd, "Verusdoc build")?; status!("Verus build complete"); Ok(()) } #[cfg(not(target_os = "windows"))] - pub fn build_verus(release: bool) -> Result<(), DynError> { + pub fn build_verus(release: bool, extra_args: &[String]) -> Result<(), DynError> { let toolchain = verus_dir().join("rust-toolchain.toml"); let toolchain_name = toolchain::load_toolchain(&toolchain); + let build_args = verus_build_args(release, extra_args); let cmd = &mut Command::new("bash"); cmd.current_dir(verus_source_dir()) .env_remove("RUSTUP_TOOLCHAIN") .env("RUSTUP_TOOLCHAIN", toolchain_name.clone()) .arg("-c") - .arg(format!( - "source ../tools/activate; vargo build {} --features singular", - if release { "--release" } else { "" } - )); - debug!("{:?}", cmd); - cmd.status().unwrap_or_else(|e| { - error!("Failed to build verus: {}", e); - }); + .arg("source ../tools/activate; vargo build \"$@\"") + .arg("vargo-build") + .args(&build_args); + run_build_command(cmd, "Verus build")?; let verusdoc_cmd = &mut Command::new("bash"); verusdoc_cmd @@ -1772,10 +1795,7 @@ pub mod install { .env("RUSTUP_TOOLCHAIN", toolchain_name) .arg("-c") .arg("source ../tools/activate; vargo build -p verusdoc"); - debug!("{:?}", verusdoc_cmd); - verusdoc_cmd.status().unwrap_or_else(|e| { - error!("Failed to build verusdoc: {}", e); - }); + run_build_command(verusdoc_cmd, "Verusdoc build")?; status!("Verus build complete"); Ok(()) @@ -1802,7 +1822,7 @@ pub mod install { install_z3()?; // Build Verus - build_verus(options.release)?; + build_verus(options.release, &options.build_args)?; // Update the workspace toolchain toolchain::sync_toolchain( @@ -2008,7 +2028,7 @@ pub mod install { status!("Verus repo updated to the latest version"); // Build Verus - build_verus(options.release)?; + build_verus(options.release, &options.build_args)?; // Update the workspace toolchain toolchain::sync_toolchain( @@ -2022,4 +2042,23 @@ pub mod install { status!("Verus upgrade complete"); Ok(()) } + + #[cfg(test)] + mod tests { + use super::*; + + #[test] + fn irc11_build_argument_is_forwarded_to_vargo() { + let extra_args = vec!["--vstd-weak-memory".to_string()]; + assert_eq!( + verus_build_args(true, &extra_args), + ["--release", "--vstd-weak-memory", "--features", "singular",] + ); + } + + #[test] + fn debug_build_keeps_existing_singular_feature() { + assert_eq!(verus_build_args(false, &[]), ["--features", "singular"]); + } + } } From 4f9accdfab93dd450151fc0c0e1c1574407212fd Mon Sep 17 00:00:00 2001 From: Hiroki Date: Mon, 10 Aug 2026 03:04:09 -0400 Subject: [PATCH 2/2] Document upstream IRC11 Verus remote --- README.md | 8 +++++--- src/main.rs | 4 +++- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 6f69b44..1105234 100644 --- a/README.md +++ b/README.md @@ -36,11 +36,13 @@ By default, `cargo dv bootstrap` builds the `main` branch of `--build-arg` to pass additional arguments to `cargo-verus` when it builds vstd. -For example, the `irc11` branch requires its weak-memory vstd modules to be +The `irc11` branch is hosted by `verus-lang/verus`, rather than the default +`asterinas/verus` remote, and requires its weak-memory vstd modules to be enabled explicitly: ```bash -cargo dv bootstrap --branch irc11 --build-arg=--vstd-weak-memory +cargo dv bootstrap --upstream-verus --branch irc11 \ + --build-arg=--vstd-weak-memory ``` For compatibility with the `irc11` branch's vargo spelling, DV translates @@ -50,7 +52,7 @@ For compatibility with the `irc11` branch's vargo spelling, DV translates The same arguments are honored by upgrades: ```bash -cargo dv bootstrap --upgrade --branch irc11 \ +cargo dv bootstrap --upgrade --upstream-verus --branch irc11 \ --build-arg=--vstd-weak-memory ``` diff --git a/src/main.rs b/src/main.rs index 2adb4f0..26a3565 100644 --- a/src/main.rs +++ b/src/main.rs @@ -556,10 +556,11 @@ mod tests { use super::*; #[test] - fn bootstrap_accepts_irc11_build_argument() { + fn bootstrap_accepts_upstream_irc11_build_argument() { let cli = Cli::try_parse_from([ "dv", "bootstrap", + "--upstream-verus", "--branch", "irc11", "--build-arg=--vstd-weak-memory", @@ -569,6 +570,7 @@ mod tests { let Commands::Bootstrap(args) = cli.command else { panic!("expected bootstrap command"); }; + assert!(args.upstream_verus); assert_eq!(args.branch.as_deref(), Some("irc11")); assert_eq!(args.build_args, ["--vstd-weak-memory"]); }