From a918be80b6ff7c9def27f8da339a990064f6182c Mon Sep 17 00:00:00 2001 From: Joshua Liebow-Feeser Date: Wed, 8 Apr 2026 17:46:57 +0000 Subject: [PATCH] [hermes] Use prebuilt Aeneas Lean artifacts Previously, we generated Lean which took a dependency on the Aeneas Lean library from GitHub. Now that we ship prebuilts which include this library, and now that we install it via `cargo hermes setup`, we can take a local dependency instead. This reduces the risk of network flakiness and makes certain workflows more cacheable, especially in development *on* Hermes and in CI. gherrit-pr-id: Gzi3vyc4cu7ln7covbdhksi66puulql2i --- hermes/Dockerfile | 3 +- hermes/src/aeneas.rs | 60 +++--------------------------------- hermes/tests/integration.rs | 61 ++++++++++++++++++++++++++++++++++--- 3 files changed, 64 insertions(+), 60 deletions(-) diff --git a/hermes/Dockerfile b/hermes/Dockerfile index c7547bdd50..a0cc0596ef 100644 --- a/hermes/Dockerfile +++ b/hermes/Dockerfile @@ -27,7 +27,8 @@ RUN mkdir -p /cache && chmod 777 /cache && \ # Direct Hermes tests to write ephemeral integration targets here to leverage # overlayfs. -ENV HERMES_INTEGRATION_TARGET_DIR=/cache/hermes_target +ENV HERMES_INTEGRATION_TARGET_DIR=/cache/hermes_target \ + HERMES_AENEAS_DIR=/cache/hermes_target/hermes_integration_cache WORKDIR /workspace COPY testdata testdata diff --git a/hermes/src/aeneas.rs b/hermes/src/aeneas.rs index cb54ecb823..64aed0a5aa 100644 --- a/hermes/src/aeneas.rs +++ b/hermes/src/aeneas.rs @@ -268,9 +268,8 @@ pub fn run_aeneas( // 4. Write Lakefile // - // If `HERMES_AENEAS_DIR` is set (e.g., in CI or local development), we use - // a local path dependency. Otherwise, we use a git dependency pinned to the - // revision specified in `Cargo.toml`. + // If `HERMES_AENEAS_DIR` is set (e.g., in CI or local development via Docker), + // we use it. Otherwise, we default to the managed toolchain directory. let aeneas_dep = if let Ok(path) = std::env::var("HERMES_AENEAS_DIR") { // Use a path dependency to avoid git cloning. // @@ -279,12 +278,9 @@ pub fn run_aeneas( // correct revision, even when using a local override. format!(r#"require aeneas from "{path}/backends/lean" -- {}"#, env!("HERMES_AENEAS_REV")) } else { - format!( - r#"require aeneas from git - "https://github.com/AeneasVerif/aeneas" @ "{}" / "backends/lean""#, - env!("HERMES_AENEAS_REV") - ) - .to_string() + let toolchain = crate::setup::Toolchain::resolve()?; + let path = toolchain.root.display(); + format!(r#"require aeneas from "{path}/backends/lean" -- {}"#, env!("HERMES_AENEAS_REV")) }; let roots_str = lake_roots.iter().map(|r| format!("`{}", r)).collect::>().join(", "); @@ -410,52 +406,6 @@ fn run_lake(roots: &LockedRoots, artifacts: &[HermesArtifact]) -> Result<()> { let lean_root = generated.parent().unwrap(); log::info!("Running 'lake build' in {}", lean_root.display()); - // If `lake-manifest.json` exists (copied from the cache), manually inject - // the `aeneas` dependency. This avoids running `lake update`, which - // would trigger the `mathlib` post-update hook (cache download). - if lean_root.join("lake-manifest.json").exists() - && let Ok(aeneas_dir) = std::env::var("HERMES_AENEAS_DIR") - { - let aeneas_url = format!("{}/backends/lean", aeneas_dir); - let manifest_path = lean_root.join("lake-manifest.json"); - - match std::fs::read_to_string(&manifest_path) { - Ok(content) => match serde_json::from_str::(&content) { - Ok(mut json) => { - if let Some(packages) = json.get_mut("packages").and_then(|v| v.as_array_mut()) - { - // Remove existing aeneas entry if present - packages - .retain(|p| p.get("name").and_then(|n| n.as_str()) != Some("aeneas")); - - log::debug!("Patching lake-manifest.json to use aeneas at {}", aeneas_url); - let entry = serde_json::json!({ - "dir": aeneas_url, - "type": "path", - "name": "aeneas", - "subDir": null, - "scope": "", - "rev": null, - "inputRev": null, // We can't easily know the inputRev, but null usually works for path deps - "inherited": false, - "configFile": "lakefile.lean", - "manifestFile": "lake-manifest.json" - }); - packages.push(entry); - - if let Ok(new_content) = serde_json::to_string_pretty(&json) - && let Err(e) = std::fs::write(&manifest_path, new_content) - { - log::warn!("Failed to write patched manifest: {}", e); - } - } - } - Err(e) => log::warn!("Failed to parse lake-manifest.json: {}", e), - }, - Err(e) => log::warn!("Failed to read lake-manifest.json: {}", e), - } - } - 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 diff --git a/hermes/tests/integration.rs b/hermes/tests/integration.rs index addcb57a60..b29ab453d2 100644 --- a/hermes/tests/integration.rs +++ b/hermes/tests/integration.rs @@ -533,10 +533,18 @@ impl TestContext { let lean_root = sandbox_root.join("target/hermes/hermes_test_target/lean"); fs::create_dir_all(&lean_root)?; - // 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. + // 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 = aeneas_cache_backend.join("lake-manifest.json"); let target_manifest = lean_root.join("lake-manifest.json"); if source_manifest.exists() { @@ -545,6 +553,51 @@ impl TestContext { #[allow(clippy::permissions_set_readonly_false)] perms.set_readonly(false); fs::set_permissions(&target_manifest, perms)?; + + // We must manually inject the `aeneas` package into the + // copied manifest. The source manifest comes from the Aeneas + // project itself, where Aeneas is the root project rather + // than a dependency. As a result, the source manifest does + // not contain an entry for the `aeneas` package. + // + // However, the generated project treats Aeneas as a path + // dependency. Lake evaluates the generated project and + // expects `aeneas` to exist in the manifest. When Lake finds + // it missing, it triggers an automatic dependency update, + // which in turn runs global post-update hooks. These hooks + // trigger operations such as large cloud cache downloads for + // Mathlib, resulting in severe performance regressions (e.g., + // tens of minutes per test run). + // + // By manually constructing the `aeneas` path dependency entry + // and injecting it into the manifest, we trick Lake into + // accepting the workspace configuration as fully resolved, + // preventing the execution of these expensive hooks. + 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!("{}/backends/lean", worker_cache.aeneas.display()); + 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 _ = fs::write(&target_manifest, new_content); + } + } + } + } } let target_lake = lean_root.join(".lake");