diff --git a/anneal/src/aeneas.rs b/anneal/src/aeneas.rs index 5a33937f97..1682b836df 100644 --- a/anneal/src/aeneas.rs +++ b/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()?; diff --git a/anneal/src/setup.rs b/anneal/src/setup.rs index 05cb3b73ad..3bd9268c57 100644 --- a/anneal/src/setup.rs +++ b/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. diff --git a/anneal/tests/integration.rs b/anneal/tests/integration.rs index 75f332643f..2aed52703e 100644 --- a/anneal/tests/integration.rs +++ b/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::(&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