diff --git a/anneal/Cargo.lock b/anneal/Cargo.lock index 2a89297700..04bcfa1bdb 100644 --- a/anneal/Cargo.lock +++ b/anneal/Cargo.lock @@ -223,6 +223,7 @@ dependencies = [ "indicatif", "log", "miette", + "pathdiff", "predicates", "proc-macro2", "quote", @@ -398,7 +399,7 @@ version = "3.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "faf9468729b8cbcea668e36183cb69d317348c2e08e994829fb56ebfdfbaac34" dependencies = [ - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] @@ -600,7 +601,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb" dependencies = [ "libc", - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] @@ -1074,6 +1075,12 @@ dependencies = [ "windows-link", ] +[[package]] +name = "pathdiff" +version = "0.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "df94ce210e5bc13cb6651479fa48d14f601d9858cfe0467f43ae157023b938d3" + [[package]] name = "percent-encoding" version = "2.3.2" @@ -1321,7 +1328,7 @@ dependencies = [ "errno", "libc", "linux-raw-sys", - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] @@ -1584,7 +1591,7 @@ dependencies = [ "getrandom 0.4.2", "once_cell", "rustix", - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] @@ -2079,7 +2086,7 @@ version = "0.1.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c2a7b1c03c876122aa43f3020e6c3c3ee5c05081c9a00739faf7503aeba10d22" dependencies = [ - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] diff --git a/anneal/Cargo.toml b/anneal/Cargo.toml index 627a17b728..8abf3e3391 100644 --- a/anneal/Cargo.toml +++ b/anneal/Cargo.toml @@ -68,6 +68,7 @@ console = "0.16.3" exocrate = { path = "../exocrate" } sha2 = "0.10" fs2 = "0.4" +pathdiff = "0.2.3" toml = "0.8" tempfile = "3.27.0" diff --git a/anneal/src/aeneas.rs b/anneal/src/aeneas.rs index 6fab4b23e6..9b4618a209 100644 --- a/anneal/src/aeneas.rs +++ b/anneal/src/aeneas.rs @@ -18,12 +18,11 @@ use std::{ path::{Path, PathBuf}, process::Stdio, sync::{Arc, Mutex}, - time::SystemTime, }; -use anyhow::{Context, Result, bail}; +use anyhow::{Context, Result, bail, ensure}; use indicatif::{ProgressBar, ProgressStyle}; -use walkdir::WalkDir; +use serde_json::{Value, json}; use crate::{generate, resolve::LockedRoots, scanner::AnnealArtifact, setup::Tool}; @@ -48,8 +47,8 @@ pub fn run_aeneas( // We generate into a temporary directory first to ensure atomic updates. // If the process crashes during generation, the existing `lean` directory // will remain untouched (or if it didn't exist, we won't leave a half-baked one). - let lean_root = roots.lean_generated_root().parent().unwrap().to_path_buf(); - let tmp_lean_root = lean_root.with_extension("tmp"); + let final_lean_root = roots.lean_generated_root().parent().unwrap().to_path_buf(); + let tmp_lean_root = final_lean_root.with_extension("tmp"); let lean_generated_root = tmp_lean_root.join("generated"); // Start with a clean slate in tmp @@ -271,8 +270,10 @@ pub fn run_aeneas( // 4. Write Lakefile // - // Aeneas and its Lean dependencies are unpacked from the managed archive. - let path = materialize_aeneas_dependency(&tmp_lean_root, &lean_root, &toolchain)?; + // Aeneas and its Lean dependencies are used directly from the managed + // archive. The generated manifest below keeps Lake on the locked dependency + // loading path, so package config/build caches can stay read-only. + let path = toolchain.aeneas_lean_dir(); let aeneas_dep = format!( r#"-- Aeneas rev: {} require aeneas from "{}""#, @@ -307,21 +308,21 @@ lean_lib «User» where ); write_if_changed(&tmp_lean_root.join("lakefile.lean"), &lakefile) .context("Failed to write Lakefile")?; + write_lake_manifest(&tmp_lean_root, &final_lean_root, &toolchain) + .context("Failed to write Lake manifest")?; // ATOMIC SWAP: If we successfully generated everything, we now swap the // temporary directory with the real one. let lean_root = roots.lean_root(); if lean_root.exists() { - // Preserve the `.lake` directory and manifest to prevent re-downloading - // dependencies (like Mathlib) on subsequent runs. + // Preserve the `.lake` directory for generated-workspace build/config + // caches. The Lake manifest is regenerated in the temporary directory + // above because it records paths to the installed toolchain relative + // to this generated workspace. let old_lake = lean_root.join(".lake"); - let old_manifest = lean_root.join("lake-manifest.json"); if old_lake.exists() { fs::rename(&old_lake, tmp_lean_root.join(".lake"))?; } - if old_manifest.exists() { - fs::rename(&old_manifest, tmp_lean_root.join("lake-manifest.json"))?; - } // Remove the existing directory before renaming the temporary directory. // Note: `fs::rename` on Unix typically requires the target directory to be @@ -338,169 +339,124 @@ lean_lib «User» where Ok(()) } -fn materialize_aeneas_dependency( - tmp_lean_root: &Path, - lean_root: &Path, +fn write_lake_manifest( + manifest_root: &Path, + final_workspace_root: &Path, toolchain: &crate::setup::Toolchain, -) -> Result { - let vendor_root = tmp_lean_root.join("vendor").join("aeneas"); - let lean_dst = vendor_root.join("backends").join("lean"); - let packages_dst = vendor_root.join("packages"); - - println!("Materializing packages by copying from toolchain..."); - copy_toolchain_tree_writable(&toolchain.aeneas_lean_dir(), &lean_dst) - .context("Failed to copy Aeneas Lean package from toolchain")?; - copy_toolchain_tree_writable(&toolchain.aeneas_root().join("packages"), &packages_dst) - .context("Failed to copy Aeneas Lean dependencies from toolchain")?; - - Ok(lean_root.join("vendor").join("aeneas").join("backends").join("lean")) +) -> Result<()> { + // We stage `lake-manifest.json` in the temporary workspace, but Lake reads + // it after that directory has been renamed to `final_workspace_root`. + // + // The final `lean` directory is not the stable object here: it is absent on + // first runs, and on reruns it is the old workspace that will be replaced. + // Canonicalize the parent and append the final leaf so manifest paths are + // relative to the post-rename workspace location. + let final_workspace_root = canonical_path_after_create_or_replace(final_workspace_root) + .with_context(|| { + format!("Failed to resolve final Lean workspace {}", final_workspace_root.display()) + })?; + let manifest = generated_lake_manifest(&final_workspace_root, toolchain)?; + let mut contents = + serde_json::to_string_pretty(&manifest).context("Failed to serialize Lake manifest")?; + contents.push('\n'); + write_if_changed(&manifest_root.join("lake-manifest.json"), &contents) } -fn copy_toolchain_tree_writable(src: &Path, dst: &Path) -> Result<()> { - if dst.exists() { - fs::remove_dir_all(dst) - .with_context(|| format!("Failed to remove stale directory {}", dst.display()))?; - } - - let mut entries = WalkDir::new(src).into_iter(); - while let Some(entry) = entries.next() { - let entry = entry.with_context(|| format!("Failed to walk {}", src.display()))?; - let path = entry.path(); - let rel = path.strip_prefix(src).with_context(|| { - format!("Failed to relativize {} against {}", path.display(), src.display()) +fn generated_lake_manifest( + workspace_root: &Path, + toolchain: &crate::setup::Toolchain, +) -> Result { + let aeneas_lean_dir = fs::canonicalize(toolchain.aeneas_lean_dir()).with_context(|| { + format!( + "Failed to resolve Aeneas Lake package directory {}", + toolchain.aeneas_lean_dir().display() + ) + })?; + let aeneas_manifest_path = aeneas_lean_dir.join("lake-manifest.json"); + let aeneas_manifest_file = fs::File::open(&aeneas_manifest_path) + .with_context(|| format!("Failed to open {}", aeneas_manifest_path.display()))?; + let aeneas_manifest: Value = serde_json::from_reader(aeneas_manifest_file) + .with_context(|| format!("Failed to parse {}", aeneas_manifest_path.display()))?; + let aeneas_packages = + aeneas_manifest.get("packages").and_then(Value::as_array).with_context(|| { + format!( + "Aeneas Lake manifest {} is missing a packages array", + aeneas_manifest_path.display() + ) })?; - let target = dst.join(rel); - - if is_lake_build_dir(rel) { - // The Nix-built archive already contains Lake build caches for the - // immutable Aeneas dependency tree. Link those caches back to the - // read-only toolchain instead of copying several GiB of `.olean` - // files into every generated Lean workspace. The surrounding - // package/config/source files are still copied below so Lake can - // update small mutable metadata such as `.lake/config`. - if let Some(parent) = target.parent() { - fs::create_dir_all(parent).with_context(|| { - format!("Failed to create parent directory {}", parent.display()) - })?; - } - create_symlink(path, &target).with_context(|| { - format!( - "Failed to link prebuilt Lake cache {} to {}", - path.display(), - target.display() - ) - })?; - entries.skip_current_dir(); - } else if entry.file_type().is_dir() { - fs::create_dir_all(&target) - .with_context(|| format!("Failed to create directory {}", target.display()))?; - } else if entry.file_type().is_symlink() { - let link = fs::read_link(path) - .with_context(|| format!("Failed to read symlink {}", path.display()))?; - if let Some(parent) = target.parent() { - fs::create_dir_all(parent).with_context(|| { - format!("Failed to create parent directory {}", parent.display()) - })?; - } - create_symlink(&link, &target) - .with_context(|| format!("Failed to copy symlink {}", target.display()))?; - } else if entry.file_type().is_file() { - if let Some(parent) = target.parent() { - fs::create_dir_all(parent).with_context(|| { - format!("Failed to create parent directory {}", parent.display()) - })?; - } - fs::copy(path, &target).with_context(|| { - format!("Failed to copy {} to {}", path.display(), target.display()) - })?; - make_writable(&target)?; - } - } - for entry in WalkDir::new(dst).contents_first(true) { - let entry = entry.with_context(|| format!("Failed to walk {}", dst.display()))?; - if !entry.file_type().is_symlink() { - make_writable(entry.path())?; - } + let mut packages = Vec::with_capacity(aeneas_packages.len() + 1); + let aeneas_lean_dir_manifest_path = + path_to_manifest_string(&relative_manifest_path(&aeneas_lean_dir, workspace_root)?); + packages.push(json!({ + "type": "path", + "name": "aeneas", + "dir": aeneas_lean_dir_manifest_path, + "inherited": false, + })); + + for entry in aeneas_packages { + let mut entry = entry + .as_object() + .cloned() + .context("Aeneas Lake manifest package entry is not an object")?; + let package_name = entry.get("name").and_then(Value::as_str).unwrap_or(""); + let package_type = entry.get("type").and_then(Value::as_str).with_context(|| { + format!("Aeneas Lake manifest package entry {package_name} is missing type") + })?; + ensure!( + package_type == "path", + "Aeneas Lake manifest package entry {package_name} is {package_type:?}, not a path dependency" + ); + let package_dir = entry.get("dir").and_then(Value::as_str).with_context(|| { + format!("Aeneas Lake manifest package entry {package_name} is missing dir") + })?; + let package_dir = Path::new(package_dir); + let package_dir = if package_dir.is_absolute() { + package_dir.to_path_buf() + } else { + aeneas_lean_dir.join(package_dir) + }; + let package_dir = fs::canonicalize(&package_dir) + .with_context(|| format!("Failed to resolve Lake package {}", package_dir.display()))?; + let package_dir_manifest_path = + path_to_manifest_string(&relative_manifest_path(&package_dir, workspace_root)?); + entry.insert("dir".to_string(), json!(package_dir_manifest_path)); + entry.insert("inherited".to_string(), json!(true)); + packages.push(Value::Object(entry)); } - normalize_lake_input_mtimes(dst)?; - - Ok(()) -} - -fn is_lake_build_dir(rel: &Path) -> bool { - rel.file_name().is_some_and(|name| name == "build") - && rel.parent().and_then(Path::file_name).is_some_and(|name| name == ".lake") + Ok(json!({ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": packages, + "name": "anneal_verification", + "lakeDir": ".lake", + "fixedToolchain": false, + })) } -#[cfg(unix)] -fn create_symlink(src: &Path, dst: &Path) -> std::io::Result<()> { - std::os::unix::fs::symlink(src, dst) -} - -#[cfg(windows)] -fn create_symlink(src: &Path, dst: &Path) -> std::io::Result<()> { - if src.is_dir() { - std::os::windows::fs::symlink_dir(src, dst) - } else { - std::os::windows::fs::symlink_file(src, dst) - } -} - -fn make_writable(path: &Path) -> Result<()> { - let metadata = - fs::symlink_metadata(path).with_context(|| format!("Failed to stat {}", path.display()))?; - if metadata.file_type().is_symlink() { - return Ok(()); - } - let mut perms = metadata.permissions(); - if perms.readonly() { - #[allow(clippy::permissions_set_readonly_false)] - perms.set_readonly(false); - fs::set_permissions(path, perms) - .with_context(|| format!("Failed to make {} writable", path.display()))?; - } - Ok(()) +/// Resolves the path a child will have once it is created under its current parent. +/// +/// This canonicalizes ancestors without resolving the final component, which +/// may be missing or may name an old object that is about to be replaced. +fn canonical_path_after_create_or_replace(path: &Path) -> Result { + let parent = path.parent().with_context(|| format!("Path {} has no parent", path.display()))?; + let parent = fs::canonicalize(parent) + .with_context(|| format!("Failed to resolve parent {}", parent.display()))?; + let file_name = + path.file_name().with_context(|| format!("Path {} has no file name", path.display()))?; + Ok(parent.join(file_name)) } -fn normalize_lake_input_mtimes(root: &Path) -> Result<()> { - // The installed toolchain archive is intentionally read-only, and - // `copy_toolchain_tree_writable` symlinks `.lake/build` directories back to - // that archive so each verification workspace does not copy several GiB of - // prebuilt `.olean` files. That optimization only works if Lake accepts the - // linked cache artifacts as newer than the copied source/config files. A - // normal file copy gives the copied inputs fresh mtimes, so Lake `--old` - // can decide that archive outputs are stale and then fail while trying to - // remove read-only files through the `.lake/build` symlinks. Mirror the - // archive builder's convention: copied Lake inputs are older than the - // archive cache artifacts, while generated project files keep their normal - // mtimes and remain mutable. - for entry in WalkDir::new(root) { - let entry = entry.with_context(|| format!("Failed to walk {}", root.display()))?; - if !entry.file_type().is_file() || !is_lake_input_file(entry.path()) { - continue; - } - - let file = fs::File::options().write(true).open(entry.path()).with_context(|| { - format!("Failed to open {} to normalize mtime", entry.path().display()) - })?; - file.set_times(fs::FileTimes::new().set_modified(SystemTime::UNIX_EPOCH)) - .with_context(|| format!("Failed to normalize mtime for {}", entry.path().display()))?; - } - - Ok(()) +fn relative_manifest_path(path: &Path, base: &Path) -> Result { + pathdiff::diff_paths(path, base).with_context(|| { + format!("Failed to compute relative path from {} to {}", base.display(), path.display()) + }) } -fn is_lake_input_file(path: &Path) -> bool { - if path.extension().and_then(|ext| ext.to_str()) == Some("lean") { - return true; - } - - matches!( - path.file_name().and_then(|name| name.to_str()), - Some("lakefile.toml" | "lake-manifest.json" | "lean-toolchain") - ) +fn path_to_manifest_string(path: &Path) -> String { + path.to_string_lossy().into_owned() } /// Generates Anneal `Specs.lean` and writes `Generated.lean`, but does not run the `lake build`. @@ -760,11 +716,10 @@ fn configure_lake_command( // FIXME: Replace this with a cleaner toolchain/archive contract. // // The Nix-built archive contains prebuilt Lake outputs for the vendored - // Aeneas package, and `materialize_aeneas_dependency` links each generated - // verification workspace's `vendor/aeneas/backends/lean/.lake/build` back - // to that read-only archive cache. That is only sound if Lake evaluates the - // vendored Aeneas package with the same build configuration that was used - // when the archive was produced. + // Aeneas package, and generated verification workspaces require that + // package directly from the installed archive. That is only sound if Lake + // evaluates Aeneas with the same build configuration that was used when the + // archive was produced. // // Aeneas' Lakefile currently makes one of those build settings depend on // the ambient `CI` environment variable: @@ -775,9 +730,8 @@ fn configure_lake_command( // sets `CI=true` for normal workflow steps. If we let that variable reach // this child process, Lake observes a different Aeneas package config than // the one recorded in the archive traces. It then invalidates the prebuilt - // cache and attempts to rebuild/remove files below the symlinked - // `.lake/build`, which fails because those archive files are intentionally - // read-only. + // cache and attempts to rebuild/remove files below the installed archive's + // read-only `.lake/build`. // // Scrubbing `CI` here keeps local runs, example CI jobs, and the integration // test harness aligned with the archive build environment. A cleaner future @@ -1013,7 +967,7 @@ fn write_if_changed(path: &std::path::Path, content: &str) -> Result<()> { #[cfg(test)] mod tests { - use std::path::PathBuf; + use std::path::{Path, PathBuf}; use super::*; use crate::generate::{MappingKind, SourceMapping}; @@ -1031,6 +985,79 @@ mod tests { } } + #[test] + fn generated_lake_manifest_locks_archive_path_dependencies_relative_to_future_workspace() { + let temp = tempfile::tempdir().unwrap(); + let workspace_root = temp.path().join("workspace/target/anneal/hash/lean"); + let toolchain_root = temp.path().join("toolchain"); + let aeneas_lean = toolchain_root.join("aeneas/backends/lean"); + let mathlib = toolchain_root.join("aeneas/packages/mathlib"); + let qq = toolchain_root.join("aeneas/packages/Qq"); + std::fs::create_dir_all(workspace_root.parent().unwrap()).unwrap(); + std::fs::create_dir_all(&aeneas_lean).unwrap(); + std::fs::create_dir_all(&mathlib).unwrap(); + std::fs::create_dir_all(&qq).unwrap(); + std::fs::write( + aeneas_lean.join("lake-manifest.json"), + serde_json::to_string(&json!({ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "type": "path", + "name": "mathlib", + "dir": "../../packages/mathlib", + "inherited": false, + }, + { + "type": "path", + "name": "Qq", + "dir": "../../packages/Qq", + "inherited": true, + "scope": "", + }, + ], + "name": "aeneas", + "lakeDir": ".lake", + "fixedToolchain": false, + })) + .unwrap(), + ) + .unwrap(); + + let toolchain = crate::setup::Toolchain { root: toolchain_root }; + let workspace_root = canonical_path_after_create_or_replace(&workspace_root).unwrap(); + let manifest = generated_lake_manifest(&workspace_root, &toolchain).unwrap(); + let packages = manifest.get("packages").unwrap().as_array().unwrap(); + + // The manifest is written before the workspace leaf exists. Create it + // now to verify that the relative paths resolve after the tmp directory + // is renamed into place. + std::fs::create_dir_all(&workspace_root).unwrap(); + + assert_eq!(packages.len(), 3); + assert_eq!(packages[0]["name"], "aeneas"); + assert_manifest_dir_resolves(&workspace_root, &packages[0], &aeneas_lean); + assert_eq!(packages[0]["inherited"], false); + + assert_eq!(packages[1]["name"], "mathlib"); + assert_manifest_dir_resolves(&workspace_root, &packages[1], &mathlib); + assert_eq!(packages[1]["inherited"], true); + + assert_eq!(packages[2]["name"], "Qq"); + assert_manifest_dir_resolves(&workspace_root, &packages[2], &qq); + assert_eq!(packages[2]["inherited"], true); + } + + fn assert_manifest_dir_resolves(workspace_root: &Path, entry: &Value, expected: &Path) { + let dir = entry.get("dir").unwrap().as_str().unwrap(); + assert!(Path::new(dir).is_relative(), "manifest dir should be relative: {dir}"); + assert_eq!( + std::fs::canonicalize(workspace_root.join(dir)).unwrap(), + std::fs::canonicalize(expected).unwrap() + ); + } + fn mk_mapping( lean_start: usize, lean_end: usize, diff --git a/anneal/tests/fixtures/expand_output/expected-aeneas.stdout b/anneal/tests/fixtures/expand_output/expected-aeneas.stdout index 35f4c97f22..db30a24a2e 100644 --- a/anneal/tests/fixtures/expand_output/expected-aeneas.stdout +++ b/anneal/tests/fixtures/expand_output/expected-aeneas.stdout @@ -1,4 +1,3 @@ -Materializing packages by copying from toolchain... === Lean expansion for: expand_output === --- Aeneas --- -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS diff --git a/anneal/tests/fixtures/expand_output/expected-all.stdout b/anneal/tests/fixtures/expand_output/expected-all.stdout index 6610b1a7cb..b4934dc041 100644 --- a/anneal/tests/fixtures/expand_output/expected-all.stdout +++ b/anneal/tests/fixtures/expand_output/expected-all.stdout @@ -1,4 +1,3 @@ -Materializing packages by copying from toolchain... === Lean expansion for: expand_output === --- Aeneas --- -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS diff --git a/anneal/tests/fixtures/expand_output/expected-anneal.stdout b/anneal/tests/fixtures/expand_output/expected-anneal.stdout index 25391c9fa2..459890bdeb 100644 --- a/anneal/tests/fixtures/expand_output/expected-anneal.stdout +++ b/anneal/tests/fixtures/expand_output/expected-anneal.stdout @@ -1,4 +1,3 @@ -Materializing packages by copying from toolchain... === Lean expansion for: expand_output === --- Anneal --- -- This file is automatically generated by Anneal. diff --git a/anneal/tests/fixtures/extern_never_verified/out.txt b/anneal/tests/fixtures/extern_never_verified/out.txt index af40cb8a87..9cf7a9e663 100644 --- a/anneal/tests/fixtures/extern_never_verified/out.txt +++ b/anneal/tests/fixtures/extern_never_verified/out.txt @@ -1,4 +1,3 @@ -Materializing packages by copying from toolchain... === Lean expansion for: extern_never_verified === --- Aeneas --- -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS diff --git a/anneal/tests/fixtures/generate_output/expected-generate.stdout b/anneal/tests/fixtures/generate_output/expected-generate.stdout index 3cba225c7f..bfeac5b89f 100644 --- a/anneal/tests/fixtures/generate_output/expected-generate.stdout +++ b/anneal/tests/fixtures/generate_output/expected-generate.stdout @@ -1,4 +1,3 @@ -Materializing packages by copying from toolchain... Lean workspace generated at: [PROJECT_ROOT]/target/anneal/anneal_test_target/lean To manually build and experiment: diff --git a/anneal/v2/flake.nix b/anneal/v2/flake.nix index 7d260ce371..3c0057ab66 100644 --- a/anneal/v2/flake.nix +++ b/anneal/v2/flake.nix @@ -445,6 +445,32 @@ "test -f ../../packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Merge.olean" (runLeanCommand "lake --old build") "test -f ../../packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Merge.olean" + # FIXME: Remove this v1-only package config primer once generated + # workspaces migrate to v2. + # Anneal v1 generated workspaces require this package directly + # from the installed archive. Prime the package config that Lake + # needs in that dependency context before the archive is frozen. + "mkdir -p $TMPDIR/aeneas-config-primer/generated" + "cp lean-toolchain $TMPDIR/aeneas-config-primer/lean-toolchain" + "cat > $TMPDIR/aeneas-config-primer/generated/Generated.lean <<'EOF'" + "import Aeneas" + "EOF" + "cat > $TMPDIR/aeneas-config-primer/lakefile.lean <<'EOF'" + "import Lake" + "open Lake DSL" + "" + "require aeneas from \"@AENEAS_ROOT@\"" + "" + "package anneal_verification" + "" + "@[default_target]" + "lean_lib «Generated» where" + " srcDir := \"generated\"" + " roots := #[`Generated]" + "EOF" + "substituteInPlace $TMPDIR/aeneas-config-primer/lakefile.lean --replace-fail @AENEAS_ROOT@ \"$PWD\"" + "(cd $TMPDIR/aeneas-config-primer && ${runLeanCommand "lake --old build Generated"})" + "test -f .lake/config/aeneas/lakefile.olean" "python3 ${./rewrite-lake-vendor.py} --root . --packages-dir ../../packages --rewrite-traces --trace-prefix \"$leanToolchain=lean\"" "TRACE_ABS_RE='(^|[\"[:space:]=:])/(nix/store|build|private/tmp/nix-build|ANNEAL_PLACEHOLDER_ROOT)'" "if find . ../../packages -type f -name \"*.trace\" -exec grep -EIl \"\$TRACE_ABS_RE\" {} + | tee /tmp/non-relocatable-traces | grep -q .; then" @@ -513,6 +539,13 @@ " cat /tmp/non-relocatable-staged-traces >&2" " exit 1" "fi" + # FIXME: Figure out whether v2 can avoid this mtime workaround. + # Nix store finalization and the staging copy can collapse file + # mtimes in the final archive. Keep Lake source/config inputs + # older than the prebuilt `.lake/build` artifacts so generated v1 + # workspaces can use `lake --old` against the installed archive + # without setup-time mtime repair. + "find $TMPDIR/dist_staging/aeneas -type f \\( -name \"*.lean\" -o -name \"lakefile.lean\" -o -name \"lakefile.toml\" -o -name \"lake-manifest.json\" -o -name \"lean-toolchain\" \\) -exec touch -h -d \"1970-01-01 00:00:00\" {} +" "chmod -R a-w $TMPDIR/dist_staging" "cd $TMPDIR/dist_staging" "tar -cf $out *" @@ -578,6 +611,7 @@ aeneas/bin/aeneas \ aeneas/bin/charon \ aeneas/bin/charon-driver \ + aeneas/backends/lean/.lake/config/aeneas/lakefile.olean \ aeneas/backends/lean/lakefile.lean \ aeneas/packages/mathlib/lake-manifest.json \ aeneas/packages/mathlib/.lake/config/mathlib/lakefile.olean \ diff --git a/anneal/v2/rewrite-lake-vendor.py b/anneal/v2/rewrite-lake-vendor.py index 053d407440..e61fc99283 100755 --- a/anneal/v2/rewrite-lake-vendor.py +++ b/anneal/v2/rewrite-lake-vendor.py @@ -155,6 +155,14 @@ def rewrite_trace_prefixes( ) for name in packages ] + root_package_patterns = [ + # Aeneas release archives can already contain traces produced in an + # upstream staging directory such as + # `/var/lib/.../dist_staging/backends/lean/...`. Those paths are not + # known to Nix, so strip any absolute package-root prefix ending in the + # Aeneas Lean backend layout. + re.compile(r"(?, Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +"""Unit tests for rewrite-lake-vendor.py.""" + +from __future__ import annotations + +import importlib.util +import tempfile +import unittest +from pathlib import Path + + +SCRIPT = Path(__file__).resolve().parents[1] / "rewrite-lake-vendor.py" +SPEC = importlib.util.spec_from_file_location("rewrite_lake_vendor", SCRIPT) +assert SPEC is not None and SPEC.loader is not None +rewrite_lake_vendor = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(rewrite_lake_vendor) + + +def write(path: Path, contents: str = "") -> None: + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(contents, encoding="utf-8") + + +class RewriteLakeVendorTests(unittest.TestCase): + def test_rewrites_upstream_aeneas_backend_trace_prefix(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) / "aeneas" / "backends" / "lean" + packages_dir = Path(tmp) / "aeneas" / "packages" + packages_dir.mkdir(parents=True) + + trace = root / ".lake" / "build" / "lib" / "lean" / "AeneasMeta" / "Utils.trace" + upstream_root = "/var/lib/github-runner-work/aeneas/aeneas/dist_staging/backends/lean" + write( + trace, + f"""{{ + "log": [{{"message": "lean {upstream_root}/AeneasMeta/Utils.lean"}}], + "inputs": [["{upstream_root}/AeneasMeta/Utils.lean", "cfad31626f87a3ad"]] +}} +""", + ) + + count = rewrite_lake_vendor.rewrite_trace_prefixes( + root=root, + packages_dir=packages_dir, + packages={}, + extra_prefixes=[], + ) + + self.assertEqual(count, 1) + rewritten = trace.read_text(encoding="utf-8") + self.assertNotIn("/var/lib", rewritten) + self.assertNotIn("backends/lean", rewritten) + self.assertIn("AeneasMeta/Utils.lean", rewritten) + + +if __name__ == "__main__": + unittest.main()