[anneal] Remove redundant integration test harness code

anneal/src/aeneas.rs

@@ -398,31 +398,7 @@ fn run_lake(roots: &LockedRoots, artifacts: &[AnnealArtifact]) -> Result<()> {
     let lean_root = generated.parent().unwrap();
     log::info!("Running 'lake build' in {}", lean_root.display());
 
-    if !lean_root.join(".lake/packages/mathlib").exists() {
-        let toolchain = crate::setup::Toolchain::resolve()?;
-        // 1. Run 'lake exe cache get' to fetch pre-built Mathlib artifacts
-        // This prevents compiling Mathlib from source, which is slow and disk-heavy.
-        let mut cache_cmd = toolchain.command(Tool::Lake);
-        cache_cmd.args(["exe", "cache", "get"]);
-        cache_cmd.current_dir(lean_root);
-        cache_cmd.stdout(Stdio::piped());
-        cache_cmd.stderr(Stdio::piped());
-
-        log::debug!("Running 'lake exe cache get'...");
-        let start = std::time::Instant::now();
-        if let Ok(output) = cache_cmd.output() {
-            if !output.status.success() {
-                log::warn!(
-                    " 'lake exe cache get' failed (status={}). Falling back to full build.\nstderr: {}",
-                    output.status,
-                    String::from_utf8_lossy(&output.stderr)
-                );
-            }
-        } else {
-            log::warn!("Failed to spawn 'lake exe cache get'");
-        }
-        log::trace!("'lake exe cache get' took {:.2?}", start.elapsed());
-    }
+
 
     // 2. Build the project (dependencies only)
     let toolchain = crate::setup::Toolchain::resolve()?;

anneal/src/setup.rs

@@ -885,6 +885,8 @@ pub fn run_setup() -> Result<()> {
         }
     }
 
+
+
     // We now perform the core rewriting of dependency configurations to point
     // to the filesystem-local paths we just created using relative path dependencies.
     let manifest_path = lean_dir.join("lake-manifest.json");
@@ -949,6 +951,25 @@ pub fn run_setup() -> Result<()> {
 
     prebuild_lean_library(&lean_dir, &toolchain.cache_dir())?;
 
+    // Delete manifest files from dependencies AFTER pre-building.
+    // This is critical because mathlib's cache fetching tool (run during prebuild)
+    // requires its own manifest to function. However, once the toolchain is installed,
+    // we must not have any manifest files in the dependencies, otherwise Lake will
+    // read them during user project verification and attempt to resolve nested
+    // dependencies via Git, bypassing our path overrides.
+    if packages_dir.exists() {
+        for entry in fs::read_dir(&packages_dir).context("Failed to read packages directory")? {
+            let entry = entry.context("Failed to read directory entry")?;
+            let path = entry.path();
+            if path.is_dir() {
+                let dep_manifest = path.join("lake-manifest.json");
+                if dep_manifest.exists() {
+                    fs::remove_file(&dep_manifest).context("Failed to delete dependency manifest")?;
+                }
+            }
+        }
+    }
+
     // Lake records absolute paths in its `.trace` files (e.g., in the
     // compiler command lines). Since we built the project in a temporary
     // directory, these traces contain paths to that directory.

anneal/tests/integration.rs

@@ -274,62 +274,7 @@ 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 {
@@ -454,8 +399,7 @@ 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
 
@@ -521,11 +465,7 @@ 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,17 +484,7 @@ 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