Add dv clean

Author: rikosellic

src/main.rs

@@ -43,6 +43,13 @@ enum Commands {
     )]
     Compile(CompileArgs),
 
+    #[command(
+        name = "clean",
+        about = "Clean build artefacts produced by `cargo dv compile`",
+        alias = "cl"
+    )]
+    Clean(CleanArgs),
+
     #[command(
         name = "fingerprint",
         about = "Print the fingerprint of the verification targets",
@@ -268,6 +275,24 @@ struct CompileArgs {
     count_line: bool,
 }
 
+#[derive(Parser, Debug)]
+struct CleanArgs {
+    #[arg(
+        short = 't',
+        long = "targets",
+        value_parser = verus::find_target,
+        help = "The targets to clean",
+        num_args = 0..,
+        action = ArgAction::Append)]
+    targets: Vec<VerusTarget>,
+    #[arg(
+        long = "all",
+        help = "Clean verification artifacts for all workspace targets",
+        default_value = "false",
+        action = ArgAction::SetTrue)]
+    all: bool,
+}
+
 #[derive(Parser, Debug)]
 struct FingerprintArgs {
     #[arg(
@@ -440,6 +465,16 @@ fn fingerprint(args: &FingerprintArgs) -> Result<(), DynError> {
     Ok(())
 }
 
+fn clean(args: &CleanArgs) -> Result<(), DynError> {
+    let targets = args.targets.clone();
+    // if --all provided, pass empty targets with all=true to verus
+    if args.all {
+        verus::exec_clean(&[], true)
+    } else {
+        verus::exec_clean(&targets, false)
+    }
+}
+
 fn list_targets(_args: &ListTargetsArgs) -> Result<(), DynError> {
     let targets = verus::verus_targets();
     let width = targets.keys().map(|s| s.len()).max().unwrap_or(0).min(70) + 1;
@@ -506,6 +541,7 @@ fn main() {
         Commands::NewTarget(args) => new_target(args),
         Commands::ShowItem(args) => show_item(args),
         Commands::Format(args) => format(args),
+        Commands::Clean(args) => clean(args),
     } {
         error!("Error when executing command `{:?}`: {}", cli.command, e);
     }

src/verus.rs

@@ -271,6 +271,35 @@ impl VerusTarget {
         if !ts.exists() {
             return false;
         }
+
+        // Check if our own verification file exists
+        if !self.library_proof().exists() {
+            return false;
+        }
+
+        // Get our own timestamp
+        let self_timestamp = match std::fs::metadata(&self.library_proof()) {
+            Ok(metadata) => metadata.modified().unwrap_or(std::time::UNIX_EPOCH),
+            Err(_) => return false,
+        };
+
+        // Check if all recursive dependencies have their verification files and are not newer than us
+        let deps = get_local_dependency_recursive(self);
+        for dep in deps.values() {
+            if !dep.library_proof().exists() {
+                return false;
+            }
+
+            // Check if dependency is newer than us
+            if let Ok(dep_metadata) = std::fs::metadata(&dep.library_proof()) {
+                if let Ok(dep_timestamp) = dep_metadata.modified() {
+                    if dep_timestamp > self_timestamp {
+                        return false; // Dependency is newer, we need to rebuild
+                    }
+                }
+            }
+        }
+
         let ts_hash = self.load_library_proof_timestamp();
         let cur_hash = self.fingerprint_recursive(all_targets);
         if cur_hash == ts_hash {
@@ -537,8 +566,44 @@ pub fn get_local_dependency(target: &VerusTarget) -> IndexMap<String, VerusTarge
     deps
 }
 
+pub fn get_local_dependency_recursive(target: &VerusTarget) -> IndexMap<String, VerusTarget> {
+    let mut result = IndexMap::new();
+    let mut visited = std::collections::HashSet::new();
+
+    fn collect_deps_recursive(
+        target: &VerusTarget,
+        result: &mut IndexMap<String, VerusTarget>,
+        visited: &mut std::collections::HashSet<String>,
+        _is_root: bool,
+    ) {
+        let target_name = target.name.replace('-', "_");
+
+        // Prevent infinite recursion
+        if visited.contains(&target_name) {
+            return;
+        }
+        visited.insert(target_name.clone());
+
+        // Get direct dependencies
+        let direct_deps = get_local_dependency(target);
+
+        // Add direct dependencies to result (unless it's the root target)
+        for (dep_name, dep_target) in direct_deps.iter() {
+            let dep_key = dep_name.replace('-', "_");
+            if !result.contains_key(&dep_key) {
+                result.insert(dep_key, dep_target.clone());
+            }
+            // Recursively collect dependencies of this dependency
+            collect_deps_recursive(dep_target, result, visited, false);
+        }
+    }
+
+    collect_deps_recursive(target, &mut result, &mut visited, true);
+    result
+}
+
 pub fn get_dependent_targets(target: &VerusTarget, release: bool) -> IndexMap<String, VerusTarget> {
-    let mut deps = get_local_dependency(target);
+    let mut deps = get_local_dependency_recursive(target);
     let order = resolve_deps_cached(target, release).full_externs;
     deps.sort_by(|a, _, b, _| {
         let x = order.get_index_of(a).unwrap_or(usize::MAX);
@@ -554,7 +619,7 @@ pub fn get_dependent_targets_batch(
 ) -> IndexMap<String, VerusTarget> {
     let mut deps = IndexMap::new();
     for target in targets.iter() {
-        deps.extend(get_local_dependency(target));
+        deps.extend(get_local_dependency_recursive(target));
     }
     let order = resolve_deps_cached(targets.first().unwrap(), release).full_externs;
     deps.sort_by(|a, _, b, _| {
@@ -622,6 +687,49 @@ pub fn check_import(imports: &[&VerusTarget]) -> Result<(), DynError> {
     Ok(())
 }
 
+pub fn check_import_with_auto_compile(
+    imports: &[&VerusTarget],
+    options: &ExtraOptions,
+) -> Result<(), DynError> {
+    let mut missing_targets = Vec::new();
+
+    for imp in imports.iter() {
+        if !imp.library_proof().exists() || !imp.library_path().exists() {
+            missing_targets.push((*imp).clone());
+        }
+    }
+
+    if !missing_targets.is_empty() {
+        info!(
+            "Missing verification files for dependencies: {:?}",
+            missing_targets.iter().map(|t| &t.name).collect::<Vec<_>>()
+        );
+        info!("Automatically compiling missing dependencies...");
+
+        // Get all dependencies of missing targets to ensure proper compilation order
+        let extended_targets = get_dependent_targets_batch(&missing_targets, options.release);
+        for target in extended_targets.values() {
+            if !target.library_proof().exists() {
+                compile_target(target, &vec![], options).map_err(|e| {
+                    format!("Failed to auto-compile dependency `{}`: {}", target.name, e)
+                })?;
+            }
+        }
+
+        // Compile the missing targets themselves
+        for target in &missing_targets {
+            if !target.library_proof().exists() {
+                compile_target(target, &vec![], options).map_err(|e| {
+                    format!("Failed to auto-compile dependency `{}`: {}", target.name, e)
+                })?;
+            }
+        }
+    }
+
+    // Final check
+    check_import(imports)
+}
+
 pub fn check_externs(externs: &IndexMap<String, String>) -> Result<(), DynError> {
     for (name, path) in externs.iter() {
         if !Path::new(path).exists() {
@@ -757,7 +865,7 @@ pub fn compile_target(
 
     prepare(target, options.release);
 
-    let mut deps = get_local_dependency(target);
+    let mut deps = get_local_dependency_recursive(target);
     let dep_rebuilt = deps.values().into_iter().any(|t| t.rebuilt == true);
 
     if !dep_rebuilt && target.is_fresh(&verus_targets()) {
@@ -791,7 +899,7 @@ pub fn compile_target(
     // imported dependencies
     deps.extend(extra_imports.clone());
     let all_imports = deps.values().collect::<Vec<_>>();
-    check_import(all_imports.as_slice()).unwrap_or_else(|e| {
+    check_import_with_auto_compile(all_imports.as_slice(), options).unwrap_or_else(|e| {
         error!("Error during verification: {}", e);
     });
     cmd_push_import(cmd, all_imports.as_slice());
@@ -935,11 +1043,11 @@ pub fn exec_verify(
         }
 
         // imported dependencies
-        let deps = &mut get_local_dependency(target);
+        let deps = &mut get_local_dependency_recursive(target);
         deps.extend(extra_imports.clone());
         let all_imports = deps.values().collect::<Vec<_>>();
 
-        check_import(all_imports.as_slice()).unwrap_or_else(|e| {
+        check_import_with_auto_compile(all_imports.as_slice(), options).unwrap_or_else(|e| {
             error!("Error during verification: {}", e);
         });
         cmd_push_import(cmd, all_imports.as_slice());
@@ -1088,6 +1196,67 @@ pub fn exec_compile(
     Ok(())
 }
 
+/// Clean build artefacts produced by `exec_compile`.
+pub fn exec_clean(targets: &[VerusTarget], all: bool) -> Result<(), DynError> {
+    let out_dir = get_target_dir();
+
+    let to_clean: Vec<VerusTarget> = if all || targets.is_empty() {
+        // clean all known targets
+        verus_targets().values().cloned().collect()
+    } else {
+        targets.iter().cloned().collect()
+    };
+
+    for target in to_clean.iter() {
+        // remove .verusdata
+        let proof = target.library_proof();
+        if proof.exists() {
+            info!("Removing {}", proof.display());
+            std::fs::remove_file(&proof).unwrap_or_else(|e| {
+                warn!("Failed to remove {}: {}", proof.display(), e);
+            });
+        }
+
+        // remove .verusdata.timestamp
+        let proof_ts = target.library_proof_timestamp();
+        if proof_ts.exists() {
+            info!("Removing {}", proof_ts.display());
+            std::fs::remove_file(&proof_ts).unwrap_or_else(|e| {
+                warn!("Failed to remove {}: {}", proof_ts.display(), e);
+            });
+        }
+
+        // remove lib{name}.rlib
+        let lib = target.library_path();
+        if lib.exists() {
+            info!("Removing {}", lib.display());
+            std::fs::remove_file(&lib).unwrap_or_else(|e| {
+                warn!("Failed to remove {}: {}", lib.display(), e);
+            });
+        }
+
+        // remove generated extern_crates
+        let extern_crates_path = out_dir.join(format!("{}.extern_crates.rs", target.name));
+        if extern_crates_path.exists() {
+            info!("Removing {}", extern_crates_path.display());
+            std::fs::remove_file(&extern_crates_path).unwrap_or_else(|e| {
+                warn!("Failed to remove {}: {}", extern_crates_path.display(), e);
+            });
+        }
+
+        // remove deps.toml
+        let deps_toml_path = out_dir.join(format!("{}.deps.toml", target.name));
+        if deps_toml_path.exists() {
+            info!("Removing {}", deps_toml_path.display());
+            std::fs::remove_file(&deps_toml_path).unwrap_or_else(|e| {
+                warn!("Failed to remove {}: {}", deps_toml_path.display(), e);
+            });
+        }
+    }
+
+    Ok(())
+}
+
 pub mod install {
     use super::*;
     use crate::toolchain;