From a195684db6f6d2b377ba6cfdc83ab5dc3d707ce0 Mon Sep 17 00:00:00 2001 From: rikosellic <64517311+rikosellic@users.noreply.github.com> Date: Wed, 5 Aug 2026 14:42:32 +0800 Subject: [PATCH 1/2] use cargo instead of vargo in `exec_bootstrap` --- src/executable.rs | 5 +- src/format.rs | 2 +- src/verus.rs | 120 +++++++++++++++++++++++++--------------------- 3 files changed, 69 insertions(+), 58 deletions(-) diff --git a/src/executable.rs b/src/executable.rs index 85819f6..60d9e4f 100644 --- a/src/executable.rs +++ b/src/executable.rs @@ -74,9 +74,8 @@ where P: AsRef + ?Sized, D: AsRef, { - let path = env_var - .and_then(|e| locate_from_env(binary, e)) - .or_else(|| locate_from_hints(binary, hints)) + let path = locate_from_hints(binary, hints) + .or_else(|| env_var.and_then(|e| locate_from_env(binary, e))) .or_else(|| locate_from_path(binary)); path.map(|path| files::absolutize(&path)) diff --git a/src/format.rs b/src/format.rs index e15f406..b683ffa 100644 --- a/src/format.rs +++ b/src/format.rs @@ -10,7 +10,7 @@ use walkdir::WalkDir; use crate::{executable, helper::DynError, verus}; -const VERUSFMT_MIN_EDITION_VERSION: &str = "0.7.1"; +const VERUSFMT_MIN_EDITION_VERSION: &str = "0.7.2"; fn get_verusfmt_path() -> Result { executable::locate(verus::VERUSFMT_BIN, None, &Vec::::new()).ok_or( diff --git a/src/verus.rs b/src/verus.rs index cad33f4..0bc6911 100644 --- a/src/verus.rs +++ b/src/verus.rs @@ -31,6 +31,9 @@ pub const VERIFICATION_RUST_TARGET: &str = "x86_64-unknown-none"; pub const VERUS_HINT_RELEASE: &str = "tools/verus/source/target-verus/release"; pub const VERUS_HINT: &str = "tools/verus/source/target-verus/debug"; +pub const Z3_BIN: &str = "z3"; +pub const Z3_HINT: &str = "tools/verus/source"; + pub const VERUSFMT_BIN: &str = "verusfmt"; #[cfg(target_os = "windows")] @@ -43,8 +46,8 @@ pub const DYN_LIB: &str = ".dylib"; pub const RUSTDOC_BIN: &str = "rustdoc"; pub const VERUSDOC_BIN: &str = "verusdoc"; -pub const VERUSDOC_HINT_RELEASE: &str = "tools/verus/source/target/release"; -pub const VERUSDOC_HINT: &str = "tools/verus/source/target/debug"; +pub const VERUSDOC_HINT_RELEASE: &str = "tools/verus/source/target-verus/release"; +pub const VERUSDOC_HINT: &str = "tools/verus/source/target-verus/debug"; #[memoize] pub fn get_cargo_verus(release: bool) -> PathBuf { @@ -64,6 +67,15 @@ pub fn get_cargo_verus(release: bool) -> PathBuf { }) } +#[memoize] +pub fn get_z3() -> PathBuf { + executable::locate(Z3_BIN, Some(CARGO_VERUS_ENV), &[Z3_HINT]).unwrap_or_else(|| { + error!( + "Cannot find the Z3 binary, please run `cargo dv bootstrap`, set CARGO_VERUS_PATH to the Verus toolchain directory, or add z3 to your PATH" + ); + }) +} + #[memoize] pub fn get_rustdoc() -> PathBuf { executable::locate( @@ -611,10 +623,12 @@ pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<() return Err("--count-line is currently unsupported with cargo-verus".into()); } + let z3 = get_z3(); let run = |target: Option<&VerusTarget>| -> Result<(), DynError> { let ts_start = Instant::now(); let cmd = &mut Command::new(get_cargo_verus(options.release)); cmd.env("RUSTC_BOOTSTRAP", "1") + .env("VERUS_Z3_PATH", &z3) .arg(if options.focus { "focus" } else { "verify" }); if !options.focus && verus_args_should_apply_to_roots_only(&options.pass_through) { cmd.arg("--fwd-verus-args-to").arg("roots"); @@ -865,9 +879,12 @@ pub fn disassemble(target: &VerusTarget) -> Result<(), DynError> { } pub fn exec_build(targets: &[VerusTarget], options: &ExtraOptions) -> Result<(), DynError> { + let z3 = get_z3(); let run = |target: Option<&VerusTarget>| -> Result<(), DynError> { let cmd = &mut Command::new(get_cargo_verus(options.release)); - cmd.env("RUSTC_BOOTSTRAP", "1").arg("build"); + cmd.env("RUSTC_BOOTSTRAP", "1") + .env("VERUS_Z3_PATH", &z3) + .arg("build"); if verus_args_should_apply_to_roots_only(&options.pass_through) { cmd.arg("--fwd-verus-args-to").arg("roots"); } @@ -1227,62 +1244,57 @@ pub mod install { Ok(()) } - #[cfg(target_os = "windows")] - pub fn build_verus(release: bool) -> Result<(), DynError> { - 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 { "" } - )); - debug!("{:?}", cmd); - cmd.status().unwrap_or_else(|e| { - error!("Failed to build verus: {}", e); - }); - - 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); - }); - - status!("Verus build complete"); - Ok(()) - } - - #[cfg(not(target_os = "windows"))] pub fn build_verus(release: bool) -> Result<(), DynError> { let toolchain = verus_dir().join("rust-toolchain.toml"); let toolchain_name = toolchain::load_toolchain(&toolchain); + let source_dir = verus_source_dir(); + + let cargo = |subcommand: &str| { + let mut cmd = Command::new("cargo"); + cmd.current_dir(&source_dir) + .env_remove("RUSTUP_TOOLCHAIN") + .env("RUSTUP_TOOLCHAIN", &toolchain_name) + .arg(subcommand); + cmd + }; - 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); - }); + let clean_cmd = cargo("clean"); - let verusdoc_cmd = &mut Command::new("bash"); - verusdoc_cmd - .current_dir(verus_source_dir()) - .env_remove("RUSTUP_TOOLCHAIN") - .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); - }); + let mut build_cmd = cargo("build"); + if release { + build_cmd.arg("--release"); + } + build_cmd.args(["--features", "singular"]); + + let mut vstd_cmd = cargo("run"); + if release { + vstd_cmd.arg("--release"); + } + vstd_cmd.args(["-p", "cargo-verus", "--", "build"]); + if release { + vstd_cmd.arg("--release"); + } + vstd_cmd.args(["--manifest-path", "vstd/Cargo.toml"]); + + for (mut cmd, description) in [ + (clean_cmd, "Cleaning the Verus workspace"), + (build_cmd, "Building Verus"), + (vstd_cmd, "Building vstd"), + ] { + debug!("{:?}", cmd); + let status = cmd.status()?; + if !status.success() { + return Err(format!("{} failed with {}", description, status).into()); + } + } + + let profile = if release { "release" } else { "debug" }; + File::create( + source_dir + .join("target-verus") + .join(profile) + .join("verus-root"), + )?; status!("Verus build complete"); Ok(()) From 9664c9fae240db5523c9c1d920e37e7bc9a3da5c Mon Sep 17 00:00:00 2001 From: rikosellic <64517311+rikosellic@users.noreply.github.com> Date: Wed, 5 Aug 2026 14:50:52 +0800 Subject: [PATCH 2/2] set HTTPS as the default clone method --- src/verus.rs | 52 ++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 36 insertions(+), 16 deletions(-) diff --git a/src/verus.rs b/src/verus.rs index 0bc6911..6eab3b7 100644 --- a/src/verus.rs +++ b/src/verus.rs @@ -1127,10 +1127,23 @@ pub mod install { }; let branch_name = branch.unwrap_or("main"); + let clone_dir_existed = verus_dir.exists(); + let cleanup_failed_clone = || -> Result<(), DynError> { + if !clone_dir_existed && verus_dir.exists() { + std::fs::remove_dir_all(verus_dir).map_err(|e| { + format!( + "Failed to clean up incomplete clone at {}: {}", + verus_dir.display(), + e + ) + })?; + } + Ok(()) + }; info!( "Cloning Verus repo from {} (branch: {}) to {} ...", - repo_ssh, + repo_https, branch_name, verus_dir.display() ); @@ -1138,6 +1151,17 @@ pub mod install { let mut builder = git2::build::RepoBuilder::new(); builder.branch(branch_name); + let https_error = match builder.clone(repo_https, verus_dir) { + Ok(_) => return Ok(()), + Err(e) => e, + }; + cleanup_failed_clone()?; + + info!("HTTPS failed, trying SSH: {}", repo_ssh); + + let mut builder_ssh = git2::build::RepoBuilder::new(); + builder_ssh.branch(branch_name); + let mut callbacks = git2::RemoteCallbacks::new(); callbacks.credentials(|_url, username_from_url, _allowed_types| { @@ -1146,22 +1170,18 @@ pub mod install { let mut fetch_opts = git2::FetchOptions::new(); fetch_opts.remote_callbacks(callbacks); - builder.fetch_options(fetch_opts); - - let ssh_result = builder.clone(repo_ssh, verus_dir); - if ssh_result.is_ok() { - return Ok(()); - } - - info!("SSH failed, trying HTTPS: {}", repo_https); - - let mut builder_https = git2::build::RepoBuilder::new(); - builder_https.branch(branch_name); - builder_https - .clone(repo_https, verus_dir) - .map_err(|e| format!("Failed to clone verus repo: {}", e))?; + builder_ssh.fetch_options(fetch_opts); + let ssh_error = match builder_ssh.clone(repo_ssh, verus_dir) { + Ok(_) => return Ok(()), + Err(e) => e, + }; + cleanup_failed_clone()?; - Ok(()) + Err(format!( + "Failed to clone Verus repo via HTTPS ({}) or SSH ({})", + https_error, ssh_error + ) + .into()) } #[cfg(target_os = "windows")]