Skip to content

refactor(doc): align build and doc targets for verus compatibility #37

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 1 commit into from
Aug 4, 2026
Merged

refactor(doc): align build and doc targets for verus compatibility #37

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
5 changes: 5 additions & 0 deletions src/commands.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -369,6 +369,11 @@ pub fn cargo_build_resolve_deps(
if release {
cmd.arg("--release");
}
// Resolve dependencies for the same verification target triple that
// `cargo dv build`/`cargo dv verify` use, so the recorded extern paths are
// compatible with rustdoc when generating docs for that target.
cmd.arg("--target")
.arg(crate::verus::VERIFICATION_RUST_TARGET);

let res = run_build_log_capture(&mut cmd);
CargoBuildExterns::parse_from_build_log(package, res.stdout.as_str(), res.stderr.as_str())
Expand Down
31 changes: 28 additions & 3 deletions src/doc.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -95,12 +95,21 @@ fn generate_single_target_doc(
cmd.env("VERUSDOC", verus_doc_value);
cmd.env("RUSTC_BOOTSTRAP", "1");

// Add extern dependencies for verus_builtin
let builtin_path = verus_target_dir.join("libverus_builtin.rlib");
// `cargo dv build` always builds with `--target <VERIFICATION_RUST_TARGET>`
// (x86_64-unknown-none), so the documentation must be generated for the same
// target triple to use those artifacts as externs. Regular libraries are
// resolved from the triple-prefixed target directory (falling back to the
// verus target directory), while proc-macro crates must remain at the host
// triple since they run during compilation.
cmd.arg("--target").arg(verus::VERIFICATION_RUST_TARGET);

// Add extern dependencies for verus_builtin (regular library -> target triple)
let builtin_path = find_dependency_artifact(&target_dir, "verus_builtin")
.unwrap_or_else(|| verus_target_dir.join("libverus_builtin.rlib"));
cmd.arg("--extern")
.arg(format!("verus_builtin={}", builtin_path.display()));

// Add extern dependencies for verus_builtin_macros
// Add extern dependencies for verus_builtin_macros (proc-macro -> host triple)
let builtin_macros_path =
verus_target_dir.join(format!("verus_builtin_macros{}", verus::DYN_LIB));
cmd.arg("--extern").arg(format!(
Expand Down Expand Up @@ -167,7 +176,15 @@ fn generate_single_target_doc(
}
}

// `cargo dv build` always passes `--target <VERIFICATION_RUST_TARGET>`, so
// the built artifacts live under the triple-prefixed directories. Search
// those first and keep the bare `target/release` and `target/debug`
// directories as a fallback for artifacts built without an explicit target
// (e.g. the `dv` crate's own dependencies).
let triple = verus::VERIFICATION_RUST_TARGET;
for deps_dir in [
target_dir.join(triple).join("release").join("deps"),
target_dir.join(triple).join("debug").join("deps"),
target_dir.join("release").join("deps"),
target_dir.join("debug").join("deps"),
] {
Expand Down Expand Up @@ -268,7 +285,10 @@ fn find_local_dependency_rlib(target_dir: &Path, dep_name: &str) -> Option<PathB
let unversioned = format!("lib{extern_name}.rlib");
let hashed_prefix = format!("lib{extern_name}-");

let triple = verus::VERIFICATION_RUST_TARGET;
let exact_candidates = [
target_dir.join(triple).join("release").join(&unversioned),
target_dir.join(triple).join("debug").join(&unversioned),
target_dir.join(&unversioned),
target_dir.join("release").join(&unversioned),
target_dir.join("debug").join(&unversioned),
Expand All @@ -280,6 +300,8 @@ fn find_local_dependency_rlib(target_dir: &Path, dep_name: &str) -> Option<PathB
}

let deps_dirs = [
target_dir.join(triple).join("release").join("deps"),
target_dir.join(triple).join("debug").join("deps"),
target_dir.join("release").join("deps"),
target_dir.join("debug").join("deps"),
];
Expand All @@ -300,7 +322,10 @@ fn find_dependency_artifact(target_dir: &Path, crate_name: &str) -> Option<PathB
fn find_hashed_artifact(target_dir: &Path, crate_name: &str, extension: &str) -> Option<PathBuf> {
let prefix = format!("lib{}-", crate_name.replace('-', "_"));
let suffix = format!(".{extension}");
let triple = verus::VERIFICATION_RUST_TARGET;
for deps_dir in [
target_dir.join(triple).join("release").join("deps"),
target_dir.join(triple).join("debug").join("deps"),
target_dir.join("release").join("deps"),
target_dir.join("debug").join("deps"),
] {
Expand Down
Loading