SQUASH ME: More clarifying tweaks, plus new (unreviewed) locking tests

anneal/v2/src/charon.rs

@@ -50,14 +50,29 @@ pub fn run_charon(
     // Global print mutex to prevent interleaved printing of consolidated artifact buffers.
     let print_mutex = std::sync::Arc::new(std::sync::Mutex::new(()));
 
-    // Determine if we should show progress bar.
-    let show_progress = show_progress && packages.len() == 1;
+    // Initialize MultiProgress if progress is enabled.
+    let mp = if show_progress {
+        Some(std::sync::Arc::new(indicatif::MultiProgress::new()))
+    } else {
+        None
+    };
 
     packages.par_iter().try_for_each(|artifact| {
         if artifact.start_from.is_empty() {
             return Ok(());
         }
 
+        let pb = mp.as_ref().map(|m| {
+            let pb = m.add(indicatif::ProgressBar::new_spinner());
+            pb.set_style(
+                indicatif::ProgressStyle::default_spinner()
+                    .template("{spinner:.green} {msg}")
+                    .unwrap(),
+            );
+            pb.set_message("Compiling...");
+            pb
+        });
+
         log::info!("Invoking Charon on package '{}'...", artifact.name.package_name);
 
         let mut cmd = toolchain.command(crate::setup::Tool::Charon);
@@ -185,9 +200,8 @@ pub fn run_charon(
 
         let mut mapper = crate::diagnostics::DiagnosticMapper::new(roots.workspace().clone());
 
-        let progress_msg = if show_progress { Some("Compiling...") } else { None };
-
-        let res = crate::util::run_command_with_progress(cmd, progress_msg, move |line, pb| {
+        let pb_clone = pb.clone();
+        let res = crate::util::run_command_with_progress(cmd, pb_clone, move |line, pb| {
             if let Ok(msg) = serde_json::from_str::<cargo_metadata::Message>(line) {
                 match msg {
                     cargo_metadata::Message::CompilerArtifact(a) => {
@@ -203,7 +217,8 @@ pub fn run_charon(
                         }
                         if matches!(
                             msg.message.level,
-                            cargo_metadata::diagnostic::DiagnosticLevel::Error | cargo_metadata::diagnostic::DiagnosticLevel::Ice
+                            cargo_metadata::diagnostic::DiagnosticLevel::Error
+                                | cargo_metadata::diagnostic::DiagnosticLevel::Ice
                         ) {
                             output_error_clone.store(true, std::sync::atomic::Ordering::Relaxed);
                         }
@@ -257,15 +272,14 @@ pub fn run_charon(
 #[cfg(test)]
 mod tests {
     use super::*;
-    use std::fs;
     use crate::resolve::{Args, resolve_roots};
     use crate::scanner::scan_workspace;
     use clap::Parser as _;
+    use std::fs;
 
+    #[cfg(feature = "exocrate_tests")]
     #[test]
     fn test_run_charon_simple() {
-        // The test environment disables progress bar via configuration injection.
-
         // 1. Create a temporary directory.
         let temp_dir = tempfile::tempdir().unwrap();
         let proj_dir = temp_dir.path().join("test_proj");
@@ -297,7 +311,8 @@ mod tests {
             "cargo-anneal",
             "--manifest-path",
             proj_dir.join("Cargo.toml").to_str().unwrap(),
-        ]).unwrap();
+        ])
+        .unwrap();
 
         // 5. Resolve roots.
         let roots = resolve_roots(&args).unwrap();
@@ -310,20 +325,20 @@ mod tests {
         // 7. Lock run root.
         let locked_roots = roots.lock_run_root().unwrap();
 
-        // 8. Resolve test-only stripped toolchain and run charon.
-        let toolchain_root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
-            .join("tests")
-            .join("toolchains")
-            .join("charon-only");
-        let toolchain = crate::setup::Toolchain::new_test(toolchain_root);
+        // 8. Resolve standard developer toolchain and run charon.
+        let toolchain = crate::setup::Toolchain::resolve().expect("Failed to resolve toolchain");
 
-        let res = run_charon(&args, &toolchain, &locked_roots, &packages, false);
+        let res = run_charon(
+            &args,
+            &toolchain,
+            &locked_roots,
+            &packages,
+            false, // show_progress
+        );
         assert!(res.is_ok(), "charon failed: {:?}", res.err());
 
         // 9. Verify .llbc file exists.
         let llbc_path = packages[0].llbc_path(&locked_roots);
         assert!(llbc_path.exists(), "llbc file not found at {:?}", llbc_path);
-
-
     }
 }

anneal/v2/src/diagnostics.rs

@@ -48,7 +48,9 @@ impl miette::Diagnostic for MappedError {
         self.help.as_ref().map(|h| Box::new(h.clone()) as Box<dyn std::fmt::Display>)
     }
 
-    fn related<'a>(&'a self) -> Option<Box<dyn std::iter::Iterator<Item = &'a dyn miette::Diagnostic> + 'a>> {
+    fn related<'a>(
+        &'a self,
+    ) -> Option<Box<dyn std::iter::Iterator<Item = &'a dyn miette::Diagnostic> + 'a>> {
         if self.related.is_empty() {
             None
         } else {
@@ -120,7 +122,10 @@ impl DiagnosticMapper {
     where
         F: FnMut(String),
     {
-        let mut mapped_paths_and_spans: std::collections::HashMap<std::path::PathBuf, Vec<&DiagnosticSpan>> = std::collections::HashMap::new();
+        let mut mapped_paths_and_spans: std::collections::HashMap<
+            std::path::PathBuf,
+            Vec<&DiagnosticSpan>,
+        > = std::collections::HashMap::new();
 
         // 1) Group spans by mapped path.
         for s in &diag.spans {
@@ -151,7 +156,8 @@ impl DiagnosticMapper {
                 let mut all_errors = Vec::new();
 
                 // Sort the paths to have the primary path first.
-                let mut paths: Vec<std::path::PathBuf> = mapped_paths_and_spans.keys().cloned().collect();
+                let mut paths: Vec<std::path::PathBuf> =
+                    mapped_paths_and_spans.keys().cloned().collect();
                 paths.sort_by_key(|p| p != &main_path);
 
                 for p in paths {

anneal/v2/src/main.rs

@@ -9,13 +9,13 @@
 
 use clap::Parser as _;
 
-mod util;
+mod charon;
 mod diagnostics;
-mod resolve;
 mod parse;
+mod resolve;
 mod scanner;
-mod charon;
 mod setup;
+mod util;
 
 /// Anneal: A Literate Verification Toolchain
 #[derive(clap::Parser, Debug)]
@@ -31,12 +31,19 @@ enum Commands {
     Setup(SetupArgs),
     /// Expand a crate (runs Charon)
     Expand(ExpandArgs),
-    /// Setup test-only stripped toolchain (dev only)
-    ///
-    /// FIXME: Add GitHub actions that will block changes that would update
-    /// tests/toolchains/ files if TestSetup were invoked without committing them.
+
+    /// Helper to acquire shared or exclusive locks for multi-process integration testing (dev only)
     #[cfg(feature = "exocrate_tests")]
-    TestSetup,
+    TestLockHelper {
+        #[arg(long)]
+        role: String,
+        #[arg(long)]
+        lock_dir: std::path::PathBuf,
+        #[arg(long)]
+        log_file: std::path::PathBuf,
+        #[arg(long)]
+        sig_file: std::path::PathBuf,
+    },
 }
 
 #[derive(clap::Parser, Debug)]
@@ -54,13 +61,15 @@ pub struct ExpandArgs {
     /// Controls where LLBC output is placed on the filesystem
     #[arg(long, value_name = "output-dir")]
     pub output_dir: Option<std::path::PathBuf>,
+
+    /// Do not show compilation progress bars
+    #[arg(long)]
+    pub no_progress: bool,
 }
 
 fn setup(args: SetupArgs) {
-    crate::setup::run_setup(crate::setup::SetupArgs {
-        local_archive: args.local_archive,
-    })
-    .expect("failed to setup toolchain");
+    crate::setup::run_setup(crate::setup::SetupArgs { local_archive: args.local_archive })
+        .expect("failed to setup toolchain");
 }
 
 fn expand(args: ExpandArgs) -> anyhow::Result<()> {
@@ -75,8 +84,14 @@ fn expand(args: ExpandArgs) -> anyhow::Result<()> {
         locked_roots.llbc_override = Some(output_dir);
     }
     let toolchain = crate::setup::Toolchain::resolve()?;
-    let show_progress = std::env::var("ANNEAL_NO_PROGRESS").is_err();
-    crate::charon::run_charon(&args.resolve_args, &toolchain, &locked_roots, &packages, show_progress)?;
+    let show_progress = !args.no_progress;
+    crate::charon::run_charon(
+        &args.resolve_args,
+        &toolchain,
+        &locked_roots,
+        &packages,
+        show_progress,
+    )?;
     Ok(())
 }
 
@@ -101,10 +116,13 @@ fn main() {
                 std::process::exit(1);
             }
         }
+
         #[cfg(feature = "exocrate_tests")]
-        Commands::TestSetup => {
-            if let Err(e) = crate::setup::run_test_setup() {
-                eprintln!("TestSetup failed: {:?}", e);
+        Commands::TestLockHelper { role, lock_dir, log_file, sig_file } => {
+            if let Err(e) =
+                crate::util::run_test_lock_helper(&role, &lock_dir, &log_file, &sig_file)
+            {
+                eprintln!("TestLockHelper failed: {:?}", e);
                 std::process::exit(1);
             }
         }
@@ -116,8 +134,7 @@ mod tests {
     #[cfg(feature = "exocrate_tests")]
     #[test]
     fn test_setup_and_toolchain_paths() {
-        // 1. Run setup (this compiles dependencies and installs them locally to target/.anneal
-        // because __ANNEAL_LOCAL_DEV=1 is defined in our .cargo/config.toml!).
+        // 1. Run setup.
         super::setup(super::SetupArgs {
             // ASSUMPTION: Dependency builder installs archive at
             // `target/anneal-exocrate.tar.zst`.
@@ -128,10 +145,29 @@ mod tests {
         let toolchain = crate::setup::Toolchain::resolve().expect("Failed to resolve toolchain");
 
         // 3. Verify that all returned paths exist as directories.
+        // Note: these assertions would be more appropriate in the setup.rs module,
+        // but including them here avoids introducing multiple tests that attempt to
+        // extract the (large) anneal exocrate archive.
         assert!(toolchain.root().is_dir(), "root is not a directory: {:?}", toolchain.root());
-        assert!(toolchain.aeneas_bin_dir().is_dir(), "aeneas_bin_dir is not a directory: {:?}", toolchain.aeneas_bin_dir());
-        assert!(toolchain.rust_sysroot().is_dir(), "rust_sysroot is not a directory: {:?}", toolchain.rust_sysroot());
-        assert!(toolchain.rust_bin().is_dir(), "rust_bin is not a directory: {:?}", toolchain.rust_bin());
-        assert!(toolchain.rust_lib().is_dir(), "rust_lib is not a directory: {:?}", toolchain.rust_lib());
+        assert!(
+            toolchain.aeneas_bin_dir().is_dir(),
+            "aeneas_bin_dir is not a directory: {:?}",
+            toolchain.aeneas_bin_dir()
+        );
+        assert!(
+            toolchain.rust_sysroot().is_dir(),
+            "rust_sysroot is not a directory: {:?}",
+            toolchain.rust_sysroot()
+        );
+        assert!(
+            toolchain.rust_bin().is_dir(),
+            "rust_bin is not a directory: {:?}",
+            toolchain.rust_bin()
+        );
+        assert!(
+            toolchain.rust_lib().is_dir(),
+            "rust_lib is not a directory: {:?}",
+            toolchain.rust_lib()
+        );
     }
 }

anneal/v2/src/resolve.rs

@@ -267,7 +267,9 @@ pub fn resolve_roots(args: &Args) -> anyhow::Result<Roots> {
     Ok(roots)
 }
 
-fn resolve_run_roots(metadata: &cargo_metadata::Metadata) -> (std::path::PathBuf, std::path::PathBuf) {
+fn resolve_run_roots(
+    metadata: &cargo_metadata::Metadata,
+) -> (std::path::PathBuf, std::path::PathBuf) {
     log::trace!("resolve_run_root");
     log::debug!("workspace_root: {:?}", metadata.workspace_root.as_std_path());
     // NOTE: Automatically handles `CARGO_TARGET_DIR` env var.

anneal/v2/src/setup.rs

@@ -84,11 +84,6 @@ impl Toolchain {
     pub fn command(&self, tool: Tool) -> std::process::Command {
         std::process::Command::new(tool.path(self))
     }
-
-    #[cfg(test)]
-    pub fn new_test(root: std::path::PathBuf) -> Self {
-        Self { root }
-    }
 }
 
 pub fn run_setup(args: SetupArgs) -> anyhow::Result<()> {
@@ -108,69 +103,3 @@ pub fn run_setup(args: SetupArgs) -> anyhow::Result<()> {
     log::info!("anneal toolchain is installed at {:?}", installation_dir);
     Ok(())
 }
-
-#[cfg(feature = "exocrate_tests")]
-pub fn run_test_setup() -> anyhow::Result<()> {
-    log::debug!("Running standard setup...");
-    run_setup(SetupArgs {
-        local_archive: Some("target/anneal-exocrate.tar.zst".into()),
-    })?;
-
-    let toolchain = Toolchain::resolve()?;
-    let dest_dir = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
-        .join("tests")
-        .join("toolchains")
-        .join("charon-only");
-
-    if dest_dir.exists() {
-        log::debug!("Cleaning existing test toolchain at {:?}", dest_dir);
-        std::fs::remove_dir_all(&dest_dir).context("Failed to clean test toolchain dir")?;
-    }
-    std::fs::create_dir_all(&dest_dir)?;
-
-    let copy_file = |src: &std::path::Path, dest: &std::path::Path| -> anyhow::Result<()> {
-        if let Some(parent) = dest.parent() {
-            std::fs::create_dir_all(parent)?;
-        }
-        std::fs::copy(src, dest)?;
-        let meta = std::fs::metadata(src)?;
-        std::fs::set_permissions(dest, meta.permissions())?;
-        Ok(())
-    };
-
-    log::debug!("Copying Charon binaries...");
-    copy_file(
-        &toolchain.aeneas_bin_dir().join("charon"),
-        &dest_dir.join("aeneas").join("bin").join("charon"),
-    )?;
-    copy_file(
-        &toolchain.aeneas_bin_dir().join("charon-driver"),
-        &dest_dir.join("aeneas").join("bin").join("charon-driver"),
-    )?;
-
-    log::debug!("Copying rustc binary...");
-    copy_file(
-        &toolchain.rust_bin().join("rustc"),
-        &dest_dir.join("rust").join("bin").join("rustc"),
-    )?;
-
-    log::debug!("Copying rust libraries (this may take a while)...");
-    let src_lib = toolchain.rust_lib();
-    let dest_lib = dest_dir.join("rust").join("lib");
-
-    for entry in walkdir::WalkDir::new(&src_lib) {
-        let entry = entry?;
-        let rel_path = entry.path().strip_prefix(&src_lib)?;
-        let dest_path = dest_lib.join(rel_path);
-        if entry.file_type().is_dir() {
-            std::fs::create_dir_all(&dest_path)?;
-        } else {
-            copy_file(entry.path(), &dest_path)?;
-        }
-    }
-
-    log::debug!("Test toolchain successfully set up at {:?}", dest_dir);
-    Ok(())
-}
-
-