[anneal] Adopt Lake artifact cache and share packages in workspace generation

anneal/src/aeneas.rs

@@ -54,6 +54,66 @@ pub fn run_aeneas(
     }
     std::fs::create_dir_all(tmp_lean_root.join("anneal"))?;
 
+    // Copy the manifest from the toolchain to seed the workspace. This
+    // prevents Lake from resolving dependencies from scratch.
+    let toolchain = crate::setup::Toolchain::resolve()?;
+    let source_manifest = toolchain.root.join("backends/lean/lake-manifest.json");
+    let target_manifest = tmp_lean_root.join("lake-manifest.json");
+    if source_manifest.exists() {
+        std::fs::copy(&source_manifest, &target_manifest)
+            .context("Failed to copy lake-manifest.json from toolchain")?;
+
+        // FIXME: This manual injection of the `aeneas` package into the
+        // manifest is a hack to work around Lake's behavior. Lake requires all
+        // dependencies listed in `lakefile.lean` to be present in the
+        // manifest, and running `lake update` triggers a full re-resolution
+        // and cloning of all dependencies (like Mathlib), defeating the
+        // purpose of the pre-populated cache.
+        //
+        // An alternative design would be to generate a manifest for a dummy
+        // project that depends on `aeneas` during toolchain setup or release,
+        // and copy that manifest here. That would avoid this manual JSON
+        // manipulation, but would require updating the path to `aeneas` in the
+        // manifest to match the user's environment.
+        if let Ok(content) = std::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 = toolchain.root.join("backends/lean").display().to_string();
+                    let entry = serde_json::json!({
+                        "dir": aeneas_url,
+                        "type": "path",
+                        "name": "aeneas",
+                        "subDir": null,
+                        "scope": "",
+                        "rev": null,
+                        "inputRev": null,
+                        "inherited": false,
+                        "configFile": "lakefile.lean",
+                        "manifestFile": "lake-manifest.json"
+                    });
+                    packages.push(entry);
+
+                    if let Ok(new_content) = serde_json::to_string_pretty(&json) {
+                        let _ = std::fs::write(&target_manifest, new_content);
+                    }
+                }
+            }
+        }
+    }
+
+    // Symlink the toolchain's `.lake/packages` directory into the workspace.
+    // This avoids redundant clones of large dependencies like Mathlib.
+    let source_packages = toolchain.root.join("backends/lean/.lake/packages");
+    let target_packages = tmp_lean_root.join(".lake/packages");
+    if source_packages.exists() {
+        // Ensure that the `.lake` directory exists in the target before
+        // symlinking packages into it.
+        std::fs::create_dir_all(tmp_lean_root.join(".lake"))
+            .context("Failed to create .lake directory in tmp workspace")?;
+        std::os::unix::fs::symlink(&source_packages, &target_packages)
+            .context("Failed to symlink .lake/packages from toolchain")?;
+    }
+
     // 2. Write Standard Library & Configuration
     let config_content = if args.allow_sorry { "axiom Anneal.allow_sorry : True\n" } else { "" };
     write_if_changed(&tmp_lean_root.join("anneal").join("Config.lean"), config_content)

anneal/src/setup.rs

@@ -643,12 +643,20 @@ fn install_lean_toolchain() -> Result<()> {
 
 /// Pre-builds the Aeneas Lean library in the extracted toolchain directory.
 /// This prevents compiling the library from source when users verify their
-/// projects, which is slow and disk-heavy. It first attempts to fetch
-/// pre-compiled Mathlib artifacts using `lake exe cache get` to avoid
-/// compiling Mathlib from source, and then runs `lake build`.
-fn prebuild_lean_library(lean_dir: &Path) -> Result<()> {
+/// projects, which is slow and disk-heavy. It first fetches pre-compiled
+/// Mathlib artifacts using `lake exe cache get`, then runs `lake build`
+/// with `LAKE_ARTIFACT_CACHE=1` so the resulting `.olean`s are also
+/// published into Lake's content-addressed artifact cache. The cache is
+/// pinned to `<toolchain_root>/lake_cache/` via `LAKE_CACHE_DIR` so that
+/// reader processes — notably the integration test suite, which runs with
+/// `HOME` redirected to a per-test sandbox — can locate it deterministically
+/// without relying on the developer's home directory.
+fn prebuild_lean_library(toolchain_root: &Path, lean_dir: &Path) -> Result<()> {
     println!("Pre-building Aeneas Lean library at {:?}...", lean_dir);
 
+    let lake_cache_dir = toolchain_root.join("lake_cache");
+    fs::create_dir_all(&lake_cache_dir).context("Failed to create Lake cache dir")?;
+
     // Fetch Mathlib cache
     println!("Fetching Mathlib cache...");
     let status = Command::new("lake")
@@ -661,10 +669,14 @@ fn prebuild_lean_library(lean_dir: &Path) -> Result<()> {
         bail!("Failed to fetch Mathlib cache; refusing to build from scratch");
     }
 
-    // Build the library
+    // Build the library, populating the artifact cache as a side effect.
+    // Targets are listed explicitly so that Mathlib's `.olean`s are also
+    // published into the artifact cache, not just Aeneas's own outputs.
     println!("Building Aeneas Lean library...");
     let status = Command::new("lake")
-        .arg("build")
+        .args(["build", "Mathlib", "Aeneas", "AeneasMeta"])
+        .env("LAKE_ARTIFACT_CACHE", "1")
+        .env("LAKE_CACHE_DIR", &lake_cache_dir)
         .current_dir(lean_dir)
         .status()
         .context("Failed to run `lake build`")?;
@@ -758,7 +770,7 @@ pub fn run_setup() -> Result<()> {
 
         let lean_dir = toolchain.root.join("backends").join("lean");
         if lean_dir.exists() {
-            prebuild_lean_library(&lean_dir)?;
+            prebuild_lean_library(&toolchain.root, &lean_dir)?;
         } else {
             log::warn!("Lean directory not found at {:?}", lean_dir);
         }