Skip to content

refactor: bootstrap process #38

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
rikosellic merged 2 commits into from
Aug 5, 2026
Merged

refactor: bootstrap process #38

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a195684
use cargo instead of vargo in `exec_bootstrap`
rikosellic Aug 5, 2026
9664c9f
set HTTPS as the default clone method
rikosellic Aug 5, 2026
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
5 changes: 2 additions & 3 deletions src/executable.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -74,9 +74,8 @@ where
P: AsRef<Path> + ?Sized,
D: AsRef<Path>,
{
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))
Expand Down
2 changes: 1 addition & 1 deletion src/format.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<PathBuf, DynError> {
executable::locate(verus::VERUSFMT_BIN, None, &Vec::<PathBuf>::new()).ok_or(
Expand Down
172 changes: 102 additions & 70 deletions src/verus.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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")]
Expand All @@ -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 {
Expand All @@ -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(
Expand Down Expand Up @@ -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");
Expand Down Expand Up @@ -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");
}
Expand Down Expand Up @@ -1110,17 +1127,41 @@ 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()
);

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| {
Expand All @@ -1129,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")]
Expand Down Expand Up @@ -1227,62 +1264,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(())
Expand Down
Loading