fix: bring dependency resolution back

src/doc.rs

@@ -1,7 +1,9 @@
 use crate::verus::{self, DynError, VerusTarget};
+use cargo_metadata::MetadataCommand;
 use colored::Colorize;
 use indexmap::IndexMap;
-use std::path::Path;
+use std::collections::HashSet;
+use std::path::{Path, PathBuf};
 use std::process::Command;
 
 /// Generate documentation for verification targets
@@ -112,26 +114,25 @@ fn generate_single_target_doc(
         state_machine_macros_path.display()
     ));
 
-    // Add extern dependencies for vstd
-    let vstd_path = verus_target_dir.join("libvstd.rlib");
+    // Prefer the Cargo-built vstd when available so rustdoc uses the same crate
+    // instance as built local dependencies.
+    let vstd_path = find_dependency_artifact(&target_dir, "vstd")
+        .unwrap_or_else(|| verus_target_dir.join("libvstd.rlib"));
     cmd.arg("--extern")
         .arg(format!("vstd={}", vstd_path.display()));
 
     // Add dependencies that this target actually needs
     let deps = verus::get_local_dependency(target);
     for (_name, dep_target) in deps.iter() {
         if dep_target.name != target.name {
-            // Check if .rlib file exists for this dependency
-            let rlib_path =
-                target_dir.join(format!("lib{}.rlib", dep_target.name.replace('-', "_")));
-            if rlib_path.exists() {
+            if let Some(rlib_path) = find_local_dependency_rlib(&target_dir, &dep_target.name) {
                 let extern_name = dep_target.name.replace('-', "_");
                 cmd.arg("--extern")
                     .arg(format!("{}={}", extern_name, rlib_path.display()));
             } else {
                 return Err(format!(
-                    "Missing compiled dependency '{}' for target '{}'.\n\nPlease run:\n  cargo dv verify --targets {}",
-                    dep_target.name, target.name, target.name
+                    "Missing built dependency '{}' for target '{}'.\n\nPlease run:\n  cargo dv build",
+                    dep_target.name, target.name
                 ).into());
             }
         }
@@ -151,10 +152,26 @@ fn generate_single_target_doc(
         .collect::<IndexMap<_, _>>();
     verus::check_externs(&remote_deps)?;
     verus::cmd_push_externs(&mut cmd, &remote_deps);
+    let mut pushed_externs = remote_deps.keys().cloned().collect::<HashSet<_>>();
 
-    let deps_dir = target_dir.join("release").join("deps");
-    cmd.arg("-L")
-        .arg(format!("dependency={}", deps_dir.display()));
+    for (extern_name, artifact_name) in direct_cargo_dependencies(&target.name)? {
+        if pushed_externs.contains(&extern_name) {
+            continue;
+        }
+        if let Some(path) = find_dependency_artifact(&target_dir, &artifact_name) {
+            cmd.arg("--extern")
+                .arg(format!("{}={}", extern_name, path.display()));
+            pushed_externs.insert(extern_name);
+        }
+    }
+
+    for deps_dir in [
+        target_dir.join("release").join("deps"),
+        target_dir.join("debug").join("deps"),
+    ] {
+        cmd.arg("-L")
+            .arg(format!("dependency={}", deps_dir.display()));
+    }
     cmd.arg("-L").arg(format!("{}", verus_target_dir.display()));
     cmd.arg("-L").arg(format!("{}", target_dir.display()));
     cmd.arg("--edition=2021")
@@ -209,6 +226,108 @@ fn generate_single_target_doc(
     Ok(())
 }
 
+fn direct_cargo_dependencies(package_name: &str) -> Result<Vec<(String, String)>, DynError> {
+    let metadata = MetadataCommand::new().exec()?;
+    let workspace_packages = metadata
+        .workspace_members
+        .iter()
+        .filter_map(|id| metadata.packages.iter().find(|package| package.id == *id))
+        .map(|package| package.name.replace('-', "_"))
+        .collect::<HashSet<_>>();
+
+    let Some(package) = metadata
+        .packages
+        .iter()
+        .find(|package| package.name == package_name)
+    else {
+        return Ok(Vec::new());
+    };
+
+    Ok(package
+        .dependencies
+        .iter()
+        .filter(|dep| matches!(dep.kind, cargo_metadata::DependencyKind::Normal))
+        .filter_map(|dep| {
+            let extern_name = dep.rename.as_ref().unwrap_or(&dep.name).replace('-', "_");
+            let artifact_name = dep.name.replace('-', "_");
+            if workspace_packages.contains(&artifact_name)
+                || verus::system_crates().contains(extern_name.as_str())
+            {
+                None
+            } else {
+                Some((extern_name, artifact_name))
+            }
+        })
+        .collect())
+}
+
+fn find_local_dependency_rlib(target_dir: &Path, dep_name: &str) -> Option<PathBuf> {
+    let extern_name = dep_name.replace('-', "_");
+    let unversioned = format!("lib{extern_name}.rlib");
+    let hashed_prefix = format!("lib{extern_name}-");
+
+    let exact_candidates = [
+        target_dir.join(&unversioned),
+        target_dir.join("release").join(&unversioned),
+        target_dir.join("debug").join(&unversioned),
+    ];
+    for candidate in exact_candidates {
+        if candidate.exists() {
+            return Some(candidate);
+        }
+    }
+
+    let deps_dirs = [
+        target_dir.join("release").join("deps"),
+        target_dir.join("debug").join("deps"),
+    ];
+    for deps_dir in deps_dirs {
+        if let Some(path) = newest_matching_artifact(&deps_dir, &hashed_prefix, ".rlib") {
+            return Some(path);
+        }
+    }
+
+    None
+}
+
+fn find_dependency_artifact(target_dir: &Path, crate_name: &str) -> Option<PathBuf> {
+    find_hashed_artifact(target_dir, crate_name, "rlib")
+        .or_else(|| find_hashed_artifact(target_dir, crate_name, "rmeta"))
+}
+
+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}");
+    for deps_dir in [
+        target_dir.join("release").join("deps"),
+        target_dir.join("debug").join("deps"),
+    ] {
+        if let Some(path) = newest_matching_artifact(&deps_dir, &prefix, &suffix) {
+            return Some(path);
+        }
+    }
+
+    None
+}
+
+fn newest_matching_artifact(dir: &Path, prefix: &str, suffix: &str) -> Option<PathBuf> {
+    std::fs::read_dir(dir)
+        .ok()?
+        .filter_map(|entry| entry.ok())
+        .map(|entry| entry.path())
+        .filter(|path| {
+            path.file_name()
+                .and_then(|name| name.to_str())
+                .map(|name| name.starts_with(prefix) && name.ends_with(suffix))
+                .unwrap_or(false)
+        })
+        .max_by_key(|path| {
+            path.metadata()
+                .and_then(|metadata| metadata.modified())
+                .ok()
+        })
+}
+
 fn run_verusdoc_postprocessor() -> Result<(), DynError> {
     let verusdoc = verus::get_verusdoc();
 

src/main.rs

@@ -37,12 +37,8 @@ enum Commands {
     )]
     Bootstrap(BootstrapArgs),
 
-    #[command(
-        name = "compile",
-        about = "Compile the verification targets",
-        alias = "c"
-    )]
-    Compile(CompileArgs),
+    #[command(name = "build", about = "Build the verification targets", alias = "c")]
+    Build(BuildArgs),
 
     #[command(
         name = "clean",
@@ -149,7 +145,7 @@ struct VerifyArgs {
         short = 'i',
         long = "import", 
         value_parser = verus::find_target,
-        help = "Import verified local crates (they need to be compiled first)",
+        help = "Import verified local crates (they need to be built first)",
         num_args = 0..,
         action = ArgAction::Append)]
     imports: Vec<VerusTarget>,
@@ -240,12 +236,12 @@ struct DocArgs {
 }
 
 #[derive(Parser, Debug)]
-struct CompileArgs {
+struct BuildArgs {
     #[arg(
         short = 't',
         long = "targets",
         value_parser = verus::find_target,
-        help = "The targets to compile",
+        help = "The targets to build",
         num_args = 0..,
         action = ArgAction::Append)]
     targets: Vec<VerusTarget>,
@@ -254,7 +250,7 @@ struct CompileArgs {
         short = 'i',
         long = "import", 
         value_parser = verus::find_target,
-        help = "Import verified local crates (they need to be compiled first)",
+        help = "Import verified local crates (they need to be built first)",
         num_args = 0..,
         action = ArgAction::Append)]
     imports: Vec<VerusTarget>,
@@ -296,7 +292,7 @@ struct CompileArgs {
         short = 'a',
         long = "disasm",
         default_value = "false",
-        help = "Do not disassemble the compiled binary",
+        help = "Do not disassemble the built binary",
         action = ArgAction::SetTrue)]
     disasm: bool,
 
@@ -475,7 +471,7 @@ fn bootstrap(args: &BootstrapArgs) -> Result<(), DynError> {
     }
 }
 
-fn compile(args: &CompileArgs) -> Result<(), DynError> {
+fn build(args: &BuildArgs) -> Result<(), DynError> {
     let targets = args.targets.clone();
     let options = verus::ExtraOptions {
         max_errors: args.max_errors,
@@ -489,7 +485,7 @@ fn compile(args: &CompileArgs) -> Result<(), DynError> {
         verify_only_module_main_only: false,
     };
 
-    verus::exec_compile(&targets, &options)
+    verus::exec_build(&targets, &options)
 }
 
 fn fingerprint(args: &FingerprintArgs) -> Result<(), DynError> {
@@ -570,7 +566,7 @@ fn main() {
         Commands::Verify(args) => verify(args),
         Commands::Doc(args) => doc(args),
         Commands::Bootstrap(args) => bootstrap(args),
-        Commands::Compile(args) => compile(args),
+        Commands::Build(args) => build(args),
         Commands::Fingerprint(args) => fingerprint(args),
         Commands::ListTargets(args) => list_targets(args),
         Commands::NewTarget(args) => new_target(args),

src/verus.rs

@@ -262,7 +262,7 @@ pub struct ExtraOptions {
 }
 
 impl ExtraOptions {
-    /// Create a modified version of options for dependency compilation
+    /// Create a modified version of options for dependency builds
     /// If verify_only_module_main_only is true, removes the verify-only-module parameter
     /// since it should only apply to the main target
     pub fn for_dependency(&self) -> Self {
@@ -955,10 +955,13 @@ pub fn disassemble(target: &VerusTarget) -> Result<(), DynError> {
     Ok(())
 }
 
-pub fn exec_compile(targets: &[VerusTarget], options: &ExtraOptions) -> Result<(), DynError> {
-    for target in targets.iter() {
+pub fn exec_build(targets: &[VerusTarget], options: &ExtraOptions) -> Result<(), DynError> {
+    let run = |target: Option<&VerusTarget>| -> Result<(), DynError> {
         let cmd = &mut Command::new(get_cargo_verus(options.release));
-        cmd.arg("build").arg("-p").arg(&target.name);
+        cmd.arg("build");
+        if let Some(target) = target {
+            cmd.arg("-p").arg(&target.name);
+        }
         if options.release {
             cmd.arg("--release");
         }
@@ -977,27 +980,42 @@ pub fn exec_compile(targets: &[VerusTarget], options: &ExtraOptions) -> Result<(
             cmd.arg("--").args(verus_args);
         }
 
+        let target_name = target
+            .map(|target| target.name.as_str())
+            .unwrap_or("workspace");
+        let target_version = target.map(|target| target.version.as_str()).unwrap_or("");
+
         info!(
             "  {} {} {}",
-            "Compiling".bold().green(),
-            target.name.white(),
-            target.version.white()
+            "Building".bold().green(),
+            target_name.white(),
+            target_version.white()
         );
         debug!(">> {:?}", cmd);
 
         let status = cmd.status().unwrap_or_else(|e| {
-            error!("Error during compilation: {}", e);
+            error!("Error during build: {}", e);
         });
 
         if status.success() {
             info!(
                 "  {} {} {}",
-                "Compiled".bold().green(),
-                target.name.white(),
-                target.version.white()
+                "Built".bold().green(),
+                target_name.white(),
+                target_version.white()
             );
         } else {
-            error!("Compilation failed for target {}", target.name);
+            error!("Build failed for target {}", target_name);
+        }
+
+        Ok(())
+    };
+
+    if targets.is_empty() {
+        run(None)?;
+    } else {
+        for target in targets.iter() {
+            run(Some(target))?;
         }
     }