Skip to content

[hermes] Use prebuilt Aeneas Lean artifacts #3229

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
joshlf wants to merge 1 commit into from
Closed

[hermes] Use prebuilt Aeneas Lean artifacts #3229

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion hermes/Dockerfile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
60 changes: 5 additions & 55 deletions hermes/src/aeneas.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
//
Expand All @@ -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::<Vec<_>>().join(", ");
Expand Down Expand Up @@ -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::<serde_json::Value>(&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
Expand Down
61 changes: 57 additions & 4 deletions hermes/tests/integration.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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() {
Expand All @@ -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::<serde_json::Value>(&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");
Expand Down
Loading