From e641e55cd30d9fe4090ed7d01b1be2f3b5be6b69 Mon Sep 17 00:00:00 2001 From: rikosellic <64517311+rikosellic@users.noreply.github.com> Date: Mon, 6 Jul 2026 11:12:30 +0800 Subject: [PATCH 1/2] Remove unused environment variables --- src/verus.rs | 70 ---------------------------------------------------- 1 file changed, 70 deletions(-) diff --git a/src/verus.rs b/src/verus.rs index e2f5712..d76b72e 100644 --- a/src/verus.rs +++ b/src/verus.rs @@ -24,11 +24,6 @@ pub type DynError = Box; /// It also provides a method to get the root directory of the project. /// -#[cfg(target_os = "windows")] -pub const VERUS_BIN: &str = "verus.exe"; -#[cfg(not(target_os = "windows"))] -pub const VERUS_BIN: &str = "verus"; - #[cfg(target_os = "windows")] pub const CARGO_VERUS_BIN: &str = "cargo-verus.exe"; #[cfg(not(target_os = "windows"))] @@ -36,7 +31,6 @@ pub const CARGO_VERUS_BIN: &str = "cargo-verus"; 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 VERUS_EVN: &str = "VERUS_PATH"; pub const CARGO_VERUS_ENV: &str = "CARGO_VERUS_PATH"; #[cfg(target_os = "windows")] @@ -44,16 +38,6 @@ pub const VERUSFMT_BIN: &str = "verusfmt.exe"; #[cfg(not(target_os = "windows"))] pub const VERUSFMT_BIN: &str = "verusfmt"; -#[cfg(target_os = "windows")] -pub const RUST_VERIFY: &str = "rust_verify.exe"; -#[cfg(not(target_os = "windows"))] -pub const RUST_VERIFY: &str = "rust_verify"; - -#[cfg(target_os = "windows")] -pub const Z3_BIN: &str = "z3.exe"; -#[cfg(not(target_os = "windows"))] -pub const Z3_BIN: &str = "z3"; - #[cfg(target_os = "windows")] pub const DYN_LIB: &str = ".dll"; #[cfg(target_os = "linux")] @@ -61,11 +45,6 @@ pub const DYN_LIB: &str = ".so"; #[cfg(target_os = "macos")] pub const DYN_LIB: &str = ".dylib"; -pub const Z3_HINT: &str = "tools/verus/source"; -pub const Z3_EVN: &str = "VERUS_Z3_PATH"; - -pub const RUSTDOC_BIN: &str = "rustdoc"; - #[cfg(target_os = "windows")] pub const VERUSDOC_BIN: &str = "verusdoc.exe"; #[cfg(not(target_os = "windows"))] @@ -73,17 +52,6 @@ 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"; -#[memoize] -pub fn get_verus(release: bool) -> PathBuf { - executable::locate( - VERUS_BIN, - Some(VERUS_EVN), - if release { &[VERUS_HINT_RELEASE] } else {&[VERUS_HINT]}, - ).unwrap_or_else(|| { - error!("Cannot find the Verus binary, please set the VERUS_PATH environment variable or add it to your PATH"); - }) -} - #[memoize] pub fn get_cargo_verus(release: bool) -> PathBuf { executable::locate( @@ -102,44 +70,6 @@ pub fn get_cargo_verus(release: bool) -> PathBuf { }) } -#[memoize] -pub fn get_rust_verify(release: bool) -> PathBuf { - executable::locate( - RUST_VERIFY, - None, - if release { - &[VERUS_HINT_RELEASE] - } else { - &[VERUS_HINT] - }, - ) - .unwrap_or_else(|| { - error!("Cannot find the Verus `rust_verify` binary."); - }) -} - -#[memoize] -pub fn get_z3() -> PathBuf { - executable::locate( - Z3_BIN, - Some(Z3_EVN), - &[Z3_HINT], - ).unwrap_or_else(|| { - error!("Cannot find the Z3 binary, please set the VERUS_Z3_PATH environment variable or add it to your PATH"); - }) -} - -#[memoize] -pub fn get_rustdoc() -> PathBuf { - executable::locate( - RUSTDOC_BIN, - None, - &[] as &[&str] - ).unwrap_or_else(|| { - error!("Cannot find the rustdoc binary, please install it using `rustup component add rust-docs`"); - }) -} - #[memoize] pub fn get_verusdoc() -> PathBuf { executable::locate(VERUSDOC_BIN, None, &[VERUSDOC_HINT_RELEASE, VERUSDOC_HINT]).unwrap_or_else( From c667f6a627a8991047889db0cea2baed400e2cc3 Mon Sep 17 00:00:00 2001 From: rikosellic <64517311+rikosellic@users.noreply.github.com> Date: Mon, 6 Jul 2026 15:35:15 +0800 Subject: [PATCH 2/2] restore `get_rustdoc` and process windoes suffix --- src/doc.rs | 4 +++- src/executable.rs | 18 +++++++++++++++--- src/verus.rs | 24 ++++++++++++++---------- 3 files changed, 32 insertions(+), 14 deletions(-) diff --git a/src/doc.rs b/src/doc.rs index c7c3b13..adc4652 100644 --- a/src/doc.rs +++ b/src/doc.rs @@ -82,7 +82,9 @@ fn generate_single_target_doc( let verus_target_dir = verus::get_verus_target_dir(); let target_dir = verus::get_target_dir(); - let mut cmd = Command::new("rustdoc"); + let rustdoc = verus::get_rustdoc(); + + let mut cmd = Command::new(&rustdoc); // Set VERUSDOC environment variable based on verus_conds flags let verus_doc_value = if verus_conds || verus_conds_debug { diff --git a/src/executable.rs b/src/executable.rs index 8fd575b..85819f6 100644 --- a/src/executable.rs +++ b/src/executable.rs @@ -3,15 +3,25 @@ use crate::files; use std::env; use std::path::{Path, PathBuf}; +#[cfg(target_os = "windows")] +const EXE_SUFFIX: &str = ".exe"; +#[cfg(not(target_os = "windows"))] +const EXE_SUFFIX: &str = ""; + +fn bin_name(binary: &Path) -> PathBuf { + PathBuf::from(format!("{}{}", binary.display(), EXE_SUFFIX)) +} + pub fn locate_from_path

(binary: &P) -> Option where P: AsRef + ?Sized, { + let binary = bin_name(binary.as_ref()); let path = env::var("PATH").ok()?; let paths = env::split_paths(&path); paths .filter_map(|dir| { - let full = dir.join(binary); + let full = dir.join(&binary); if full.is_file() { Some(full) } else { @@ -26,10 +36,11 @@ where P: AsRef + ?Sized, D: AsRef, { + let binary = bin_name(binary.as_ref()); hints .iter() .filter_map(|hint| { - let full = hint.as_ref().join(binary); + let full = hint.as_ref().join(&binary); if full.is_file() { Some(full) } else { @@ -43,11 +54,12 @@ pub fn locate_from_env

(binary: &P, env_var: &str) -> Option where P: AsRef + ?Sized, { + let binary = bin_name(binary.as_ref()); let env_path = env::var(env_var).ok()?; let paths = env::split_paths(&env_path); paths .filter_map(|dir| { - let full = dir.join(binary); + let full = dir.join(&binary); if full.is_file() { Some(full) } else { diff --git a/src/verus.rs b/src/verus.rs index d76b72e..e3ef08e 100644 --- a/src/verus.rs +++ b/src/verus.rs @@ -24,18 +24,12 @@ pub type DynError = Box; /// It also provides a method to get the root directory of the project. /// -#[cfg(target_os = "windows")] -pub const CARGO_VERUS_BIN: &str = "cargo-verus.exe"; -#[cfg(not(target_os = "windows"))] pub const CARGO_VERUS_BIN: &str = "cargo-verus"; +pub const CARGO_VERUS_ENV: &str = "CARGO_VERUS_PATH"; 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 CARGO_VERUS_ENV: &str = "CARGO_VERUS_PATH"; -#[cfg(target_os = "windows")] -pub const VERUSFMT_BIN: &str = "verusfmt.exe"; -#[cfg(not(target_os = "windows"))] pub const VERUSFMT_BIN: &str = "verusfmt"; #[cfg(target_os = "windows")] @@ -45,9 +39,8 @@ pub const DYN_LIB: &str = ".so"; #[cfg(target_os = "macos")] pub const DYN_LIB: &str = ".dylib"; -#[cfg(target_os = "windows")] -pub const VERUSDOC_BIN: &str = "verusdoc.exe"; -#[cfg(not(target_os = "windows"))] +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"; @@ -70,6 +63,17 @@ pub fn get_cargo_verus(release: bool) -> PathBuf { }) } +#[memoize] +pub fn get_rustdoc() -> PathBuf { + executable::locate( + RUSTDOC_BIN, + None, + &[] as &[&str] + ).unwrap_or_else(|| { + error!("Cannot find the rustdoc binary, please install it using `rustup component add rust-docs`"); + }) +} + #[memoize] pub fn get_verusdoc() -> PathBuf { executable::locate(VERUSDOC_BIN, None, &[VERUSDOC_HINT_RELEASE, VERUSDOC_HINT]).unwrap_or_else(