[anneal] Don't copy Lean build artifacts from ~/.anneal (#3344)

Prior to this change, Lake verification relied on recursively copying
the entire global precompiled toolchain package directory (~5,000
`.olean` files, ~5GB) into a build directory. This was obviously slow
and caused massive disk bloat.

In this commit, we instead:
- Copy only those files which Lake will attempt to write, and symlink
  all other files. In practice, this means that only the smallest files
  are actually copied. (Note: Copying is necessary *at all* because Lake
  will write to some files in the directories of a package's
  *dependencies* if those dependencies are filesystem-local. Without
  copying, this would result in concurrent writes to the user-global
  `~/.anneal/toolchain` directory.)
- Mark the `~/.anneal/toolchain/<toolchain>` directory as recursively
  read-only to ensure that any attempted writes fail loudly.

Release 0.1.0-alpha.22.

gherrit-pr-id: Gks63dnqyjzxt6s6sgowdaz63rogw5kz3

Author: joshlf

anneal/Cargo.lock

@@ -4,7 +4,7 @@ members = [".", "tools/doc_gen"]
 [package]
 name = "cargo-anneal"
 edition = "2024"
-version = "0.1.0-alpha.21"
+version = "0.1.0-alpha.22"
 description = "Formally verify that your safety comments are correct."
 categories = [
   "development-tools::cargo-plugins",

anneal/Cargo.toml

@@ -85,10 +85,12 @@ RUN cargo build && \
 # command fetches and builds the dependencies.
 ENV ANNEAL_TOOLCHAIN_DIR=/opt/anneal_toolchain
 RUN cargo run && \
+    chmod -R u+w /opt/anneal_toolchain && \
     LEAN_DIR=$(find /opt/anneal_toolchain/.anneal/toolchain/ -type d -path "*/backends/lean" | head -n 1) && \
     cd $LEAN_DIR && \
-    lake exe graph imports.dot --to Aeneas,Aeneas.Std.Core,Aeneas.Std.WP,Aeneas.Tactic.Solver.ScalarTac,Aeneas.Std.Scalar.Core --include-deps && \
-    python3 /workspace/tools/prune_mathlib.py imports.dot .lake/packages/mathlib
+    lake exe graph /workspace/imports.dot --to Aeneas,Aeneas.Std.Core,Aeneas.Std.WP,Aeneas.Tactic.Solver.ScalarTac,Aeneas.Std.Scalar.Core --include-deps && \
+    python3 /workspace/tools/prune_mathlib.py /workspace/imports.dot ../../packages/mathlib && \
+    chmod -R a-w /opt/anneal_toolchain
 
 # Ensure the integration target directory exists.
 RUN mkdir -p /cache/anneal_target

anneal/Dockerfile

@@ -109,7 +109,7 @@ impl std::ops::Div<PositiveUsize> for usize {
 Install Anneal and its required toolchains (Charon and Aeneas):
 
 ```bash
-cargo install cargo-anneal@0.1.0-alpha.21
+cargo install cargo-anneal@0.1.0-alpha.22
 cargo anneal setup
 ```
 

anneal/README.md

@@ -1,7 +1,8 @@
-use std::path::PathBuf;
+use std::path::{Path, PathBuf};
 
 use anyhow::{Context, Result};
 use fs2::FileExt;
+use walkdir::WalkDir;
 
 /// Represents an active, exclusive lock on a directory.
 ///
@@ -68,3 +69,28 @@ impl DirLock {
         }
     }
 }
+
+/// Walks a directory recursively and replaces string patterns inside `.trace`
+/// files. This is used to patch non-portable paths generated by Lake.
+pub fn patch_trace_files(dir: &Path, replacements: &[(&str, &str)]) -> Result<()> {
+    if dir.exists() {
+        let walker = WalkDir::new(dir).into_iter();
+        for entry in walker {
+            let entry = entry.context("Failed to walk directory for trace patching")?;
+            let path = entry.path();
+            if path.is_file() && path.extension().map_or(false, |ext| ext == "trace") {
+                let content = std::fs::read_to_string(path)
+                    .with_context(|| format!("Failed to read trace file {:?}", path))?;
+                let mut new_content = content.clone();
+                for (from, to) in replacements {
+                    new_content = new_content.replace(from, to);
+                }
+                if new_content != content {
+                    std::fs::write(path, new_content)
+                        .with_context(|| format!("Failed to write trace file {:?}", path))?;
+                }
+            }
+        }
+    }
+    Ok(())
+}

anneal/src/aeneas.rs

@@ -274,63 +274,6 @@ impl TestContext {
             Some(temp)
         };
 
-        let lean_root = sandbox_root.join("target/anneal/anneal_test_target/lean");
-        fs::create_dir_all(&lean_root)?;
-
-        // We skip seeding the Lean workspace cache for mock setup tests because
-        // they do not run the full verification pipeline and do not need Lean.
-        // 1. Seed the Lean workspace cache so Lake skips Mathlib downloads.
-
-        // The Lean manifest dictates which dependencies Lake needs to
-        // resolve. We copy this directly from the global cache to ensure
-        // the test sandbox observes exactly the same dependency tree as
-        // the precompiled artifacts. If we did not copy this lockfile,
-        // Lake would attempt to resolve dependencies from scratch. Since
-        // our dependencies specify floating branches rather than explicit
-        // git hashes in their configuration files, a fresh resolution
-        // could map to newer commits. A mismatch in a single commit hash
-        // invalidates the shared compilation cache, causing Lean to
-        // redundantly recompile the entire dependency tree (e.g.,
-        // Mathlib) from source. Copying the manifest guarantees a
-        // cache hit.
-        let source_manifest = toolchain_path.join("backends/lean").join("lake-manifest.json");
-        let target_manifest = lean_root.join("lake-manifest.json");
-        if source_manifest.exists() {
-            fs::copy(&source_manifest, &target_manifest)?;
-            let mut perms = fs::metadata(&target_manifest)?.permissions();
-            #[allow(clippy::permissions_set_readonly_false)]
-            perms.set_readonly(false);
-            fs::set_permissions(&target_manifest, perms)?;
-
-            // Inject aeneas dependency into manifest
-            if let Ok(content) = fs::read_to_string(&target_manifest) {
-                if let Ok(mut json) = serde_json::from_str::<serde_json::Value>(&content) {
-                    if let Some(packages) = json.get_mut("packages").and_then(|v| v.as_array_mut())
-                    {
-                        let aeneas_url =
-                            format!("file://{}/backends/lean", toolchain_path.display());
-                        let entry = serde_json::json!({
-                            "url": aeneas_url,
-                            "type": "git",
-                            "name": "aeneas",
-                            "subDir": null,
-                            "scope": "",
-                            "rev": "main",
-                            "inputRev": "main",
-                            "inherited": false,
-                            "configFile": "lakefile.lean",
-                            "manifestFile": "lake-manifest.json"
-                        });
-                        packages.push(entry);
-
-                        if let Ok(new_content) = serde_json::to_string_pretty(&json) {
-                            let _ = fs::write(&target_manifest, new_content);
-                        }
-                    }
-                }
-            }
-        }
-
         // Copy extra inputs based on config.
         for extra in &config.extra_inputs {
             let extra_path = test_case_root.join(extra);
@@ -454,9 +397,6 @@ echo "---END-INVOCATION---" >> "{}"
             cmd.env("ELAN_HOME", elan_home);
         }
 
-        let toolchain_path = get_toolchain_path();
-        let lean_backend_dir = toolchain_path.join("backends/lean");
-
         // Resolve Mocks
 
         // Re-organizing execution flow:
@@ -521,11 +461,6 @@ echo "---END-INVOCATION---" >> "{}"
         cmd.env("ANNEAL_FORCE_TTY", "1");
         cmd.env("FORCE_COLOR", "1");
 
-        cmd.env("ANNEAL_INTEGRATION_TEST_LEAN_CACHE_DIR", &lean_backend_dir);
-        // Set `LAKE_CACHE_DIR` to point to the global cache in the toolchain
-        // directory to share build artifacts across tests and avoid redundant
-        // recompilation.
-        cmd.env("LAKE_CACHE_DIR", toolchain_path.join("lake-cache"));
         cmd.env("ANNEAL_USE_PATH_FOR_TOOLS", "1");
         cmd.env("RAYON_NUM_THREADS", "1");
 
@@ -544,18 +479,6 @@ echo "---END-INVOCATION---" >> "{}"
         cmd.env("PATH", new_path);
         cmd.env("RUSTFLAGS", rustflags);
 
-        // Configure git to trust all directories in this test sandbox
-        // Configure Git to trust all directories within this test sandbox.
-        // This is required because tests run as the host user but may access
-        // files created by the `anneal` user in the Docker image, triggering
-        // Git's 'dubious ownership' security check.
-        let status = std::process::Command::new("git")
-            .args(["config", "--global", "--add", "safe.directory", "*"])
-            .env("HOME", &self.home_dir)
-            .status()
-            .expect("Failed to run git config");
-        assert!(status.success(), "git config failed");
-
         // Redirect HOME to the persistent home directory within the sandbox.
         // This ensures that the toolchain is looked up and potentially
         // repaired/reinstalled in a location that is isolated from the