From c88afa3514514225544ee431683210e2db5c1a51 Mon Sep 17 00:00:00 2001 From: Mark Dittmer Date: Mon, 13 Jul 2026 19:53:20 +0000 Subject: [PATCH] [anneal] Audit cached Lean artifacts against clean builds Split the Nix pipeline at a shared, path-rewritten source tree. Keep the default fast path cache-seeded with one trace traversal, and add a seed-free Lean build whose packaged output passes through the same pruning and archive finalizers. Compare complete source, toolchain, and Lake build payloads, including raw ILean reference usages, hash sidecars, and stable trace dependency/output hashes. Regenerate the two stale candidate ILean files exposed by that audit, install both archives independently, and compare the complete normalized InfoView setup contract in isolated environments. Run the clean reference build and equivalence checks in a standalone nightly workflow on main so ordinary push and pull-request jobs retain the fast path. gherrit-pr-id: Gri3qjmi3mkxqhujr7xw3insogx5mpcm4 --- .../workflows/anneal-archive-equivalence.yml | 253 ++++++ .github/workflows/anneal.yml | 4 +- .../archive_lake_cache_reuse/anneal.toml | 2 +- anneal/tests/integration.rs | 240 ++++-- anneal/v2/check-flake-eval.sh | 12 + anneal/v2/compare-toolchain-archives.py | 804 ++++++++++++++++++ anneal/v2/flake.nix | 392 ++++++--- anneal/v2/prune-lake-cache.py | 3 +- anneal/v2/rewrite-lake-vendor.py | 24 +- .../tests/test_compare_toolchain_archives.py | 458 ++++++++++ anneal/v2/tests/test_prune_lake_cache.py | 14 + anneal/v2/tests/test_rewrite_lake_vendor.py | 94 ++ 12 files changed, 2131 insertions(+), 169 deletions(-) create mode 100644 .github/workflows/anneal-archive-equivalence.yml create mode 100755 anneal/v2/compare-toolchain-archives.py create mode 100644 anneal/v2/tests/test_compare_toolchain_archives.py diff --git a/.github/workflows/anneal-archive-equivalence.yml b/.github/workflows/anneal-archive-equivalence.yml new file mode 100644 index 0000000000..09b46bca7b --- /dev/null +++ b/.github/workflows/anneal-archive-equivalence.yml @@ -0,0 +1,253 @@ +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , 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. + +name: Anneal Archive Equivalence + +on: + # Keep this expensive reference build out of the ordinary push, pull-request, + # and merge-queue graph. Scheduled workflows run from the default branch; the + # checkout step below pins the exact main revision recorded by the event. + schedule: + - cron: '37 07 * * *' + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +env: + CARGO_TERM_COLOR: always + +jobs: + compare-fast-and-slow: + name: Compare fast and clean-build archives + if: github.repository == 'google/zerocopy' + runs-on: ubuntu-latest + timeout-minutes: 360 + permissions: + contents: read + steps: + - name: Free up disk space + run: | + df -h + sudo rm -rf /usr/local/lib/android + sudo rm -rf /usr/share/dotnet + sudo rm -rf /usr/local/share/boost + df -h + + - name: Checkout + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 + with: + # The scheduled event SHA is the exact main revision recorded for + # this run. For a manual run, retain the ref selected in the UI/API. + ref: ${{ github.event_name == 'schedule' && github.sha || github.ref }} + persist-credentials: false + + - name: Install stable Rust + uses: dtolnay/rust-toolchain@e97e2d8cc328f1b50210efc529dca0028893a2d9 # zizmor: ignore[superfluous-actions] + with: + toolchain: stable + + # Reuse the trusted default-branch cache populated by anneal.yml. This is + # deliberately restore-only: the nightly clean-build profile is a + # reference result, not a substituter that ordinary PR jobs should trust. + - name: Restore Anneal main Nix binary cache + uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 + with: + path: anneal/v2/target/nix-cache-main + key: anneal-v2-main-nix-cache-v2-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('anneal/v2/flake.nix', 'anneal/v2/flake.lock', 'anneal/v2/rewrite-lake-vendor.py', 'anneal/v2/prune-lake-cache.py', 'anneal/v2/prime-lakefile.lean') }} + restore-keys: | + anneal-v2-main-nix-cache-v2-${{ runner.os }}-${{ runner.arch }}- + + - name: Install Nix + uses: DeterminateSystems/determinate-nix-action@629b284231c2a82554b724e357e47fc6020833c8 # v3.21.2 + + # Ubuntu 24.04 restricts the user namespaces used by the FHS environment + # in the Mathlib cache/build derivations. + - name: Enable unprivileged user namespaces + run: sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0 + + - name: Build fast and clean-build archives + id: build_archives + working-directory: anneal/v2 + run: | + set -euo pipefail + mkdir -p target + nix_args=() + if [ -f target/nix-cache-main/nix-cache-info ]; then + nix_args+=(--extra-substituters "file://$PWD/target/nix-cache-main/?trusted=1") + fi + + nix build "${nix_args[@]}" .#omnibus-archive-ci-fast \ + --out-link target/anneal-exocrate-fast.tar.zst + # Force the Lean-artifact-free recipe itself to execute tonight. + # Rebuilding only its archive wrapper could still substitute a cached + # reference compilation while appearing to perform the slow audit. + nix build "${nix_args[@]}" --rebuild .#aeneas-compiled-slow \ + --out-link target/aeneas-compiled-slow + nix build "${nix_args[@]}" .#omnibus-archive-ci-slow \ + --out-link target/anneal-exocrate-slow.tar.zst + + fast_archive="$(readlink -f target/anneal-exocrate-fast.tar.zst)" + slow_archive="$(readlink -f target/anneal-exocrate-slow.tar.zst)" + if [ "$fast_archive" = "$slow_archive" ]; then + echo "Fast and clean-build archive attributes resolved to the same output" >&2 + exit 1 + fi + + fast_compiled_drv="$(nix eval --raw .#aeneas-compiled-fast.drvPath)" + slow_compiled_drv="$(nix eval --raw .#aeneas-compiled-slow.drvPath)" + prepared_cache_drv="$(nix eval --raw .#aeneas-prepared-cache.drvPath)" + fast_archive_drv="$(nix eval --raw .#omnibus-archive-ci-fast.drvPath)" + slow_archive_drv="$(nix eval --raw .#omnibus-archive-ci-slow.drvPath)" + nix-store --query --requisites "$fast_archive_drv" > target/fast-archive-requisites + nix-store --query --requisites "$slow_archive_drv" > target/slow-archive-requisites + nix-store --query --requisites "$slow_compiled_drv" > target/slow-compiled-requisites + + require_requisite() { + local inventory="$1" + local dependency="$2" + local description="$3" + if ! grep -Fxq "$dependency" "$inventory"; then + echo "$description is missing its required dependency" >&2 + exit 1 + fi + } + reject_requisite() { + local inventory="$1" + local dependency="$2" + local description="$3" + if grep -Fxq "$dependency" "$inventory"; then + echo "$description unexpectedly reaches a forbidden dependency" >&2 + exit 1 + fi + } + require_requisite target/fast-archive-requisites \ + "$fast_compiled_drv" "Fast archive" + require_requisite target/fast-archive-requisites \ + "$prepared_cache_drv" "Fast archive" + reject_requisite target/fast-archive-requisites \ + "$slow_compiled_drv" "Fast archive" + require_requisite target/slow-archive-requisites \ + "$slow_compiled_drv" "Clean-build archive" + reject_requisite target/slow-archive-requisites \ + "$fast_compiled_drv" "Clean-build archive" + reject_requisite target/slow-archive-requisites \ + "$prepared_cache_drv" "Clean-build archive" + reject_requisite target/slow-compiled-requisites \ + "$prepared_cache_drv" "Clean-build compilation" + + # Exercise the full layout contract against both packaged results. + nix build "${nix_args[@]}" --no-link \ + .#omnibus-archive-layout-check-fast \ + .#omnibus-archive-layout-check-slow + + echo "fast_archive=$fast_archive" >> "$GITHUB_OUTPUT" + echo "slow_archive=$slow_archive" >> "$GITHUB_OUTPUT" + printf 'Fast archive: %s bytes\n' "$(stat -c %s "$fast_archive")" + printf 'Slow archive: %s bytes\n' "$(stat -c %s "$slow_archive")" + + - name: Restore AppArmor restriction + if: always() + run: sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=1 + + - name: Install fast archive + id: install_fast + if: steps.build_archives.outcome == 'success' + continue-on-error: true + env: + FAST_ARCHIVE: ${{ steps.build_archives.outputs.fast_archive }} + working-directory: anneal + run: | + ANNEAL_TOOLCHAIN_DIR="$RUNNER_TEMP/anneal-toolchain-fast" cargo run setup \ + --local-archive "$FAST_ARCHIVE" + + - name: Install clean-build archive + id: install_slow + if: steps.build_archives.outcome == 'success' + continue-on-error: true + env: + SLOW_ARCHIVE: ${{ steps.build_archives.outputs.slow_archive }} + working-directory: anneal + run: | + ANNEAL_TOOLCHAIN_DIR="$RUNNER_TEMP/anneal-toolchain-slow" cargo run setup \ + --local-archive "$SLOW_ARCHIVE" + + - name: Check fast archive contract + id: check_fast + if: always() && steps.install_fast.outcome == 'success' + continue-on-error: true + env: + ANNEAL_TOOLCHAIN_DIR: ${{ runner.temp }}/anneal-toolchain-fast + RUSTFLAGS: '' + RUSTDOCFLAGS: '' + RUST_TEST_THREADS: '1' + __ZEROCOPY_LOCAL_DEV: '1' + working-directory: anneal + run: cargo test --test integration archive_lake_cache_reuse -- --nocapture + + - name: Check clean-build archive contract + id: check_slow + if: always() && steps.install_slow.outcome == 'success' + continue-on-error: true + env: + ANNEAL_TOOLCHAIN_DIR: ${{ runner.temp }}/anneal-toolchain-slow + RUSTFLAGS: '' + RUSTDOCFLAGS: '' + RUST_TEST_THREADS: '1' + __ZEROCOPY_LOCAL_DEV: '1' + working-directory: anneal + run: cargo test --test integration archive_lake_cache_reuse -- --nocapture + + - name: Compare InfoView setup contracts + id: compare_infoview + if: >- + always() && + steps.install_fast.outcome == 'success' && + steps.install_slow.outcome == 'success' + continue-on-error: true + env: + ANNEAL_TOOLCHAIN_DIR: ${{ runner.temp }}/anneal-toolchain-fast + ANNEAL_REFERENCE_TOOLCHAIN_DIR: ${{ runner.temp }}/anneal-toolchain-slow + RUSTFLAGS: '' + RUSTDOCFLAGS: '' + RUST_TEST_THREADS: '1' + __ZEROCOPY_LOCAL_DEV: '1' + working-directory: anneal + run: cargo test --test integration archive_lake_cache_reuse -- --nocapture + + - name: Compare archive build outputs + id: compare_archives + if: steps.build_archives.outcome == 'success' + continue-on-error: true + env: + FAST_ARCHIVE: ${{ steps.build_archives.outputs.fast_archive }} + SLOW_ARCHIVE: ${{ steps.build_archives.outputs.slow_archive }} + working-directory: anneal/v2 + run: ./compare-toolchain-archives.py "$FAST_ARCHIVE" "$SLOW_ARCHIVE" + + - name: Require every equivalence check to pass + if: always() + env: + INSTALL_FAST: ${{ steps.install_fast.outcome }} + INSTALL_SLOW: ${{ steps.install_slow.outcome }} + CHECK_FAST: ${{ steps.check_fast.outcome }} + CHECK_SLOW: ${{ steps.check_slow.outcome }} + COMPARE_INFOVIEW: ${{ steps.compare_infoview.outcome }} + COMPARE_ARCHIVES: ${{ steps.compare_archives.outcome }} + run: | + set -euo pipefail + test "$INSTALL_FAST" = success + test "$INSTALL_SLOW" = success + test "$CHECK_FAST" = success + test "$CHECK_SLOW" = success + test "$COMPARE_INFOVIEW" = success + test "$COMPARE_ARCHIVES" = success diff --git a/.github/workflows/anneal.yml b/.github/workflows/anneal.yml index 70ed992a3f..c1ffe040dc 100644 --- a/.github/workflows/anneal.yml +++ b/.github/workflows/anneal.yml @@ -284,7 +284,7 @@ jobs: uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 with: path: anneal/v2/target/nix-cache-main - key: anneal-v2-main-nix-cache-v2-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('anneal/v2/flake.nix', 'anneal/v2/flake.lock', 'anneal/v2/rewrite-lake-vendor.py', 'anneal/v2/prune-lake-cache.py') }} + key: anneal-v2-main-nix-cache-v2-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('anneal/v2/flake.nix', 'anneal/v2/flake.lock', 'anneal/v2/rewrite-lake-vendor.py', 'anneal/v2/prune-lake-cache.py', 'anneal/v2/prime-lakefile.lean') }} # Pull request caches are scoped by GitHub to the PR merge ref, so they # can speed up repeated pushes to the same PR without becoming visible to @@ -296,7 +296,7 @@ jobs: uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 with: path: anneal/v2/target/nix-cache-pr - key: anneal-v2-pr-nix-cache-v1-${{ runner.os }}-${{ runner.arch }}-pr-${{ github.event.pull_request.number }}-${{ hashFiles('anneal/v2/flake.nix', 'anneal/v2/flake.lock', 'anneal/v2/rewrite-lake-vendor.py', 'anneal/v2/prune-lake-cache.py') }} + key: anneal-v2-pr-nix-cache-v1-${{ runner.os }}-${{ runner.arch }}-pr-${{ github.event.pull_request.number }}-${{ hashFiles('anneal/v2/flake.nix', 'anneal/v2/flake.lock', 'anneal/v2/rewrite-lake-vendor.py', 'anneal/v2/prune-lake-cache.py', 'anneal/v2/prime-lakefile.lean') }} - name: Install Nix uses: DeterminateSystems/determinate-nix-action@629b284231c2a82554b724e357e47fc6020833c8 # v3.21.2 diff --git a/anneal/tests/fixtures/archive_lake_cache_reuse/anneal.toml b/anneal/tests/fixtures/archive_lake_cache_reuse/anneal.toml index 5714e4edec..cf5e6b1ed7 100644 --- a/anneal/tests/fixtures/archive_lake_cache_reuse/anneal.toml +++ b/anneal/tests/fixtures/archive_lake_cache_reuse/anneal.toml @@ -1,4 +1,4 @@ description = """ Purpose: Verifies that the installed Nix-built archive can be used read-only by a fresh generated Lake workspace and the Lean language server. -Behavior: Builds, diagnoses, and runs IDE setup-file on a tiny workspace with a complete relative Lake manifest pointing at the installed Aeneas archive. +Behavior: Builds, diagnoses, and runs IDE setup-file on a tiny workspace with a complete relative Lake manifest pointing at the installed Aeneas archive. When ANNEAL_REFERENCE_TOOLCHAIN_DIR is set, repeats the full contract against that installation and compares the complete setup-file output after normalizing installed-toolchain artifact paths. """ diff --git a/anneal/tests/integration.rs b/anneal/tests/integration.rs index ce5215b663..a42b447a46 100644 --- a/anneal/tests/integration.rs +++ b/anneal/tests/integration.rs @@ -259,37 +259,48 @@ fn get_toolchain_base_dir() -> PathBuf { fn get_toolchain_install_dir() -> PathBuf { TOOLCHAIN_INSTALL_DIR .get_or_init(|| { - let dir = get_toolchain_base_dir() - .join("anneal") - .join("toolchain") - .join(env!("ANNEAL_EXOCRATE_VERSION_SLUG")); - if !dir.exists() { - panic!( - "Anneal toolchain is not installed at {}. Run `cargo run setup \ - --local-archive ...` once before running integration tests.", - dir.display() - ); - } - - for path in [ - dir.join("aeneas/bin/charon"), - dir.join("aeneas/bin/aeneas"), - dir.join("lean/bin/lake"), - ] { - if !path.exists() { + validate_toolchain_install_dir(&get_toolchain_base_dir(), "ANNEAL_TOOLCHAIN_DIR") + .unwrap_or_else(|error| { panic!( - "Anneal toolchain installation is missing {}. Re-run `cargo run setup \ - --local-archive ...` before running integration tests.", - path.display() - ); - } - } - - dir + "{error}. Run `cargo run setup --local-archive ...` once before running \ + integration tests." + ) + }) }) .clone() } +fn validate_toolchain_install_dir( + toolchain_base_dir: &Path, + environment_variable: &str, +) -> Result> { + let dir = toolchain_base_dir + .join("anneal") + .join("toolchain") + .join(env!("ANNEAL_EXOCRATE_VERSION_SLUG")); + if !dir.exists() { + return Err(invalid_data(format!( + "{environment_variable} has no Anneal toolchain installed at {}", + dir.display() + )) + .into()); + } + + for path in + [dir.join("aeneas/bin/charon"), dir.join("aeneas/bin/aeneas"), dir.join("lean/bin/lake")] + { + if !path.exists() { + return Err(invalid_data(format!( + "{environment_variable} installation is missing {}", + path.display() + )) + .into()); + } + } + + Ok(dir) +} + fn get_toolchain_bin_dir() -> PathBuf { get_toolchain_install_dir().join("aeneas").join("bin") } @@ -300,14 +311,51 @@ fn run_archive_lake_cache_reuse_test(test_name: &str) -> datatest_stable::Result let temp = tempfile::Builder::new() .prefix("anneal-archive-cache-reuse-") .tempdir_in(get_target_dir())?; - assert_archive_lake_cache_reuse(test_name, &get_toolchain_install_dir(), temp.path()) + let primary_toolchain = get_toolchain_install_dir(); + let reference_toolchain = + if let Some(reference_base_dir) = std::env::var_os("ANNEAL_REFERENCE_TOOLCHAIN_DIR") { + let reference_toolchain = validate_toolchain_install_dir( + Path::new(&reference_base_dir), + "ANNEAL_REFERENCE_TOOLCHAIN_DIR", + )?; + let primary_canonical = fs::canonicalize(&primary_toolchain)?; + let reference_canonical = fs::canonicalize(&reference_toolchain)?; + if primary_canonical == reference_canonical { + return Err(invalid_data(format!( + "ANNEAL_TOOLCHAIN_DIR and ANNEAL_REFERENCE_TOOLCHAIN_DIR resolve to the same \ + installed toolchain: {}", + primary_canonical.display() + )) + .into()); + } + Some(reference_toolchain) + } else { + None + }; + + let setup = assert_archive_lake_cache_reuse(test_name, &primary_toolchain, temp.path())?; + let Some(reference_toolchain) = reference_toolchain else { return Ok(()) }; + let reference_setup = assert_archive_lake_cache_reuse( + test_name, + &reference_toolchain, + &temp.path().join("reference"), + )?; + if setup != reference_setup { + return Err(invalid_data(format!( + "Lake setup-file output differs between ANNEAL_TOOLCHAIN_DIR and \ + ANNEAL_REFERENCE_TOOLCHAIN_DIR:\nprimary: {setup:#?}\nreference: {reference_setup:#?}" + )) + .into()); + } + + Ok(()) } fn assert_archive_lake_cache_reuse( test_name: &str, toolchain_root: &Path, temp_root: &Path, -) -> Result<(), Box> { +) -> Result> { let aeneas_root = toolchain_root.join("aeneas"); let aeneas_lean = aeneas_root.join("backends/lean"); let lean_root = toolchain_root.join("lean"); @@ -341,7 +389,7 @@ lean_lib Generated where // This is the workspace-loading path used by the Lean language server and // IDE InfoView on first open. `setup-file` checks dependency traces in hash // mode and is not allowed to repair the read-only archive. - run_lake_archive_setup_file(test_name, &workspace, toolchain_root, &lean_root)?; + let setup = run_lake_archive_setup_file(test_name, &workspace, toolchain_root, &lean_root)?; // This mirrors v1's generated workspace contract with the Nix-built // archive: dependency paths are locked relative to the workspace, package // caches are read-only, and `--old` must reuse the prebuilt Lake outputs. @@ -365,7 +413,7 @@ lean_lib Generated where ], )?; - Ok(()) + Ok(setup) } fn assert_no_write_bits(root: &Path) -> Result<(), Box> { @@ -485,7 +533,7 @@ fn run_lake_archive_setup_file( workspace: &Path, toolchain_root: &Path, lean_root: &Path, -) -> Result<(), Box> { +) -> Result> { let cmd = lake_archive_command( workspace, lean_root, @@ -516,7 +564,7 @@ fn run_lake_archive_setup_file( Some(input.as_bytes()), )?; let assert = run.assert.success(); - let setup: Value = serde_json::from_slice(&assert.get_output().stdout)?; + let mut setup: Value = serde_json::from_slice(&assert.get_output().stdout)?; let import_arts = setup .get("importArts") .and_then(Value::as_object) @@ -524,37 +572,70 @@ fn run_lake_archive_setup_file( if !import_arts.contains_key("Aeneas") { return Err(invalid_data("Lake setup-file output has no Aeneas import artifact").into()); } - for (module, artifacts) in import_arts { - let artifacts = artifacts.as_array().ok_or_else(|| { - invalid_data(format!("Lake setup-file artifacts for {module} are not an array")) - })?; - for artifact in artifacts { - let artifact = artifact.as_str().ok_or_else(|| { - invalid_data(format!("Lake setup-file artifact for {module} is not a path")) - })?; - validate_setup_artifact(toolchain_root, artifact)?; - } - } for field in ["dynlibs", "plugins"] { - let artifacts = setup - .get(field) - .and_then(Value::as_array) - .ok_or_else(|| invalid_data(format!("Lake setup-file output has no {field} array")))?; - for artifact in artifacts { - let artifact = artifact.as_str().ok_or_else(|| { - invalid_data(format!("Lake setup-file {field} entry is not a path")) - })?; - validate_setup_artifact(toolchain_root, artifact)?; + if !setup.get(field).is_some_and(Value::is_array) { + return Err(invalid_data(format!("Lake setup-file output has no {field} array")).into()); } } + + let toolchain_root = fs::canonicalize(toolchain_root)?; + for field in ["importArts", "dynlibs", "plugins"] { + normalize_setup_path_field( + setup.get_mut(field).expect("validated Lake setup-file field is missing"), + field, + &toolchain_root, + )?; + } fs::write(workspace.join("lean-server-setup.json"), &assert.get_output().stdout)?; + Ok(setup) +} + +fn normalize_setup_path_field( + value: &mut Value, + field_path: &str, + toolchain_root: &Path, +) -> Result<(), Box> { + match value { + Value::String(artifact) => { + let normalized = normalize_setup_artifact(toolchain_root, artifact)?; + *artifact = normalized + .to_str() + .ok_or_else(|| { + invalid_data(format!( + "Lake setup-file artifact at {field_path} is not valid UTF-8: {}", + normalized.display() + )) + })? + .to_owned(); + } + Value::Array(values) => { + for (index, value) in values.iter_mut().enumerate() { + normalize_setup_path_field( + value, + &format!("{field_path}[{index}]"), + toolchain_root, + )?; + } + } + Value::Object(values) => { + for (key, value) in values { + normalize_setup_path_field(value, &format!("{field_path}.{key}"), toolchain_root)?; + } + } + _ => { + return Err(invalid_data(format!( + "Lake setup-file path field {field_path} contains a non-path value" + )) + .into()); + } + } Ok(()) } -fn validate_setup_artifact( +fn normalize_setup_artifact( toolchain_root: &Path, artifact: &str, -) -> Result<(), Box> { +) -> Result> { let artifact = Path::new(artifact); if !artifact.is_file() { return Err(invalid_data(format!( @@ -564,7 +645,6 @@ fn validate_setup_artifact( .into()); } let artifact = fs::canonicalize(artifact)?; - let toolchain_root = fs::canonicalize(toolchain_root)?; if !artifact.starts_with(&toolchain_root) { return Err(invalid_data(format!( "Lake setup-file returned an artifact outside the installed toolchain: {}", @@ -572,7 +652,7 @@ fn validate_setup_artifact( )) .into()); } - Ok(()) + Ok(artifact.strip_prefix(toolchain_root)?.to_path_buf()) } fn lake_archive_command( @@ -581,10 +661,52 @@ fn lake_archive_command( args: &[&str], ) -> Result> { let lean_bin = lean_root.join("bin"); + let isolated_home = workspace.join(".anneal-test-home"); + let isolated_xdg = workspace.join(".anneal-test-xdg"); + let isolated_lake_cache = isolated_xdg.join("cache/lake"); + for directory in [ + &isolated_home, + &isolated_xdg.join("cache"), + &isolated_xdg.join("config"), + &isolated_xdg.join("data"), + &isolated_xdg.join("state"), + &isolated_lake_cache, + ] { + fs::create_dir_all(directory)?; + } + let mut cmd = process::Command::new(lean_bin.join("lake")); - cmd.args(args) - .current_dir(workspace) - .env_remove("CI") + cmd.args(args).current_dir(workspace).env_remove("CI"); + for variable in [ + "LAKE_ARTIFACT_CACHE", + "LAKE_CACHE_ARTIFACT_ENDPOINT", + "LAKE_CACHE_DIR", + "LAKE_CACHE_KEY", + "LAKE_CACHE_REVISION_ENDPOINT", + "LAKE_CACHE_SERVICE", + "LAKE_CONFIG", + "LAKE_HOME", + "LAKE_INVALID_CONFIG", + "LAKE_NO_CACHE", + "LAKE_OVERRIDE_LEAN", + "LAKE_PKG_URL_MAP", + "LEAN_AR", + "LEAN_CC", + "LEAN_GITHASH", + "LEAN_MANUAL_ROOT", + "LEAN_PATH", + "LEAN_SRC_PATH", + "LEAN_SYSROOT", + "LEAN_WORKER_PATH", + ] { + cmd.env_remove(variable); + } + cmd.env("HOME", isolated_home) + .env("XDG_CACHE_HOME", isolated_xdg.join("cache")) + .env("XDG_CONFIG_HOME", isolated_xdg.join("config")) + .env("XDG_DATA_HOME", isolated_xdg.join("data")) + .env("XDG_STATE_HOME", isolated_xdg.join("state")) + .env("LAKE_CACHE_DIR", isolated_lake_cache) .env("LEAN_SYSROOT", lean_root) .env("MATHLIB_NO_CACHE_ON_UPDATE", "1") .env("PATH", prepend_env_paths("PATH", &[lean_bin])?); diff --git a/anneal/v2/check-flake-eval.sh b/anneal/v2/check-flake-eval.sh index 22d71f04dd..5809b77680 100644 --- a/anneal/v2/check-flake-eval.sh +++ b/anneal/v2/check-flake-eval.sh @@ -22,8 +22,12 @@ systems=( packages=( aeneas-compiled + aeneas-compiled-fast + aeneas-compiled-slow aeneas-download aeneas-metadata-files + aeneas-prepared-cache + aeneas-prepared-sources aeneas-unpacked default leantar @@ -32,8 +36,16 @@ packages=( mathlib-cache-unpacked omnibus-archive omnibus-archive-ci + omnibus-archive-ci-fast + omnibus-archive-ci-slow + omnibus-archive-fast omnibus-archive-layout-check + omnibus-archive-layout-check-fast + omnibus-archive-layout-check-slow + omnibus-archive-slow omnibus-tar + omnibus-tar-fast + omnibus-tar-slow rust-toolchain ) diff --git a/anneal/v2/compare-toolchain-archives.py b/anneal/v2/compare-toolchain-archives.py new file mode 100755 index 0000000000..868cd38360 --- /dev/null +++ b/anneal/v2/compare-toolchain-archives.py @@ -0,0 +1,804 @@ +#!/usr/bin/env python3 +# +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , 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. + +"""Compare the semantic contents of two Anneal toolchain archives. + +The fast and slow archive builds can legitimately differ in compression, tar +headers, and the contents of narrowly defined Lake bookkeeping files. They +must otherwise contain exactly the same payload. This program therefore +compares SHA-256 hashes and modes for all Lean, Rust, and non-``.lake`` Aeneas +payload files, and for all actual files below every ``.lake/build`` directory. +That includes complete ``.ilean`` code-intelligence data and its hash sidecars. + +Lake traces contain contextual command logs and dependency descriptions, so +their raw JSON need not be byte-identical. Their schema version, dependency +hash, and output hashes are canonicalized and compared. Response files, setup +JSON, and ``.lake/config`` contents may also be contextual, but their complete +path, type, link-target, and mode inventories must be identical. + +Lake artifact archives/caches, no-build markers, and temporary primer state +are rejected outright. A normal-file versus hard-link representation is +treated as an archive-storage detail when both resolve to identical bytes. + +Archives are never extracted to the filesystem. ``zstd`` streams each archive +into Python's tar reader; member paths and link targets are validated before +regular file contents are inspected. This avoids following archive-provided +links and avoids path traversal by construction. +""" + +from __future__ import annotations + +import argparse +import hashlib +import json +import os +import subprocess +import sys +import tarfile +import tempfile +from collections import Counter +from dataclasses import dataclass +from pathlib import Path +from typing import BinaryIO, Iterable + + +ZSTD_MAGIC = b"\x28\xb5\x2f\xfd" + +EXPECTED_TOP_LEVELS = {"aeneas", "lean", "rust"} + +REQUIRED_MEMBER_PATHS = { + "aeneas/bin/aeneas", + "aeneas/bin/charon", + "aeneas/bin/charon-driver", + "aeneas/backends/lean/.lake/config/aeneas/lakefile.olean", + "aeneas/packages/mathlib/.lake/config/mathlib/lakefile.olean", + "aeneas/packages/mathlib/lake-manifest.json", + "lean/bin/lake", + "lean/bin/lean", + "rust/bin/cargo", + "rust/bin/rustc", +} + +REQUIRED_EXECUTABLE_PATHS = { + "aeneas/bin/aeneas", + "aeneas/bin/charon", + "aeneas/bin/charon-driver", + "lean/bin/lake", + "lean/bin/lean", + "rust/bin/cargo", + "rust/bin/rustc", +} + +# These are path-bearing command descriptions rather than compiler outputs. +# Their bytes may differ, but their inventory is compared. Do not add broad +# suffixes such as `.json`: an arbitrary generated JSON file may be a real +# build output. In particular, every `.hash` sidecar is compiler output and +# is compared exactly. Lake traces are handled separately below: their stable +# dependency and output hashes are semantic even though their logs are not. +INVENTORY_ONLY_BUILD_SUFFIXES = ( + ".rsp", + ".setup.json", +) + +DEFAULT_MAX_MEMBERS = 1_000_000 +DEFAULT_MAX_MEMBER_BYTES = 8 * 1024**3 +DEFAULT_MAX_ARCHIVE_BYTES = 32 * 1024**3 +MAX_CANONICAL_TRACE_BYTES = 512 * 1024**2 +COPY_CHUNK_SIZE = 1024 * 1024 + + +class ArchiveInspectionError(RuntimeError): + """An archive is malformed, unsafe, or not an Anneal toolchain archive.""" + + +@dataclass(frozen=True) +class FileContent: + sha256: str + size: int + canonical_trace: bool = False + + +@dataclass(frozen=True) +class SemanticRecord: + """Content, type, and mode relevant to archive equivalence.""" + + kind: str + mode: int + sha256: str | None = None + size: int | None = None + link_target: str | None = None + + def short_description(self) -> str: + mode = f"mode={self.mode:#06o}" + if self.kind == "directory": + return f"directory, {mode}" + if self.kind == "symlink": + return f"symlink -> {self.link_target}, {mode}" + if self.sha256 is None: + return f"{self.kind}, content ignored, {mode}" + return f"sha256={self.sha256[:16]}..., {self.size} bytes, {mode}" + + +@dataclass(frozen=True) +class PendingSemanticFile: + path: str + content_path: str + mode: int + canonical_trace: bool + + +@dataclass +class ArchiveInventory: + semantic_files: dict[str, SemanticRecord] + metadata_files: dict[str, SemanticRecord] + ignored_files: Counter[str] + present_paths: set[str] + regular_like_paths: set[str] + top_levels: set[str] + member_count: int + declared_file_bytes: int + + def comparison_records(self) -> dict[str, SemanticRecord]: + records = dict(self.semantic_files) + overlap = records.keys() & self.metadata_files.keys() + if overlap: + raise AssertionError(f"records classified twice: {sorted(overlap)}") + records.update(self.metadata_files) + return records + + +@dataclass(frozen=True) +class ComparisonResult: + only_first: tuple[str, ...] + only_second: tuple[str, ...] + changed: tuple[str, ...] + + @property + def equivalent(self) -> bool: + return not (self.only_first or self.only_second or self.changed) + + +def _normalize_member_name(name: str) -> str: + if not name or "\x00" in name: + raise ArchiveInspectionError("archive contains an empty or NUL-containing path") + if name.startswith("/") or "\\" in name: + raise ArchiveInspectionError(f"archive contains a non-POSIX or absolute path: {name!r}") + + parts: list[str] = [] + for part in name.split("/"): + if part in ("", "."): + continue + if part == "..": + raise ArchiveInspectionError(f"archive path contains '..': {name!r}") + parts.append(part) + if not parts: + raise ArchiveInspectionError(f"archive path normalizes to empty: {name!r}") + return "/".join(parts) + + +def _normalize_symlink_target(member_path: str, target: str) -> str: + if not target or "\x00" in target or target.startswith("/") or "\\" in target: + raise ArchiveInspectionError( + f"unsafe symlink target for {member_path!r}: {target!r}" + ) + + parts = member_path.split("/")[:-1] + for part in target.split("/"): + if part in ("", "."): + continue + if part == "..": + if not parts: + raise ArchiveInspectionError( + f"symlink escapes archive root: {member_path!r} -> {target!r}" + ) + parts.pop() + else: + parts.append(part) + if not parts: + raise ArchiveInspectionError( + f"symlink resolves to archive root: {member_path!r} -> {target!r}" + ) + return "/".join(parts) + + +def _lake_directory_kind(path: str) -> str | None: + parts = path.split("/") + try: + index = parts.index(".lake") + except ValueError: + return None + if index + 1 >= len(parts): + return "state" + return parts[index + 1] + + +def _inventory_only_build_category(path: str) -> str | None: + for suffix in INVENTORY_ONLY_BUILD_SUFFIXES: + if path.endswith(suffix): + return { + ".rsp": "lake-response-file", + ".setup.json": "lake-setup-json", + }[suffix] + return None + + +def _classify_file(path: str) -> tuple[bool, str]: + """Return ``(is_semantic, category)`` for a non-directory member.""" + + if not path.startswith("aeneas/") and path != "aeneas": + return True, "toolchain-payload" + + lake_kind = _lake_directory_kind(path) + if lake_kind is None: + return True, "aeneas-payload" + if lake_kind == "build": + ignored = _inventory_only_build_category(path) + if ignored is not None: + return False, ignored + return True, "lake-build-output" + if lake_kind == "config": + return False, "lake-config-cache" + # Artifact caches are rejected before classification. Unknown `.lake` + # state is compared exactly rather than silently widening the exception. + return True, "lake-other-state" + + +def _is_lake_build_path(path: str) -> bool: + return path.startswith("aeneas/") and _lake_directory_kind(path) == "build" + + +def _is_lake_build_trace(path: str) -> bool: + return _is_lake_build_path(path) and path.endswith(".trace") + + +def _canonicalize_trace(data: bytes, path: str) -> bytes: + try: + document = json.loads(data) + except (UnicodeDecodeError, json.JSONDecodeError) as error: + raise ArchiveInspectionError(f"invalid Lake trace JSON in {path!r}: {error}") from error + if not isinstance(document, dict): + raise ArchiveInspectionError(f"Lake trace JSON is not an object: {path!r}") + for field in ("schemaVersion", "depHash", "outputs"): + if field not in document: + raise ArchiveInspectionError( + f"Lake trace JSON has no {field!r} field: {path!r}" + ) + canonical_document = { + field: document[field] for field in ("schemaVersion", "depHash", "outputs") + } + try: + return json.dumps( + canonical_document, + ensure_ascii=False, + allow_nan=False, + separators=(",", ":"), + sort_keys=True, + ).encode("utf-8") + except (TypeError, ValueError) as error: + raise ArchiveInspectionError( + f"cannot canonicalize Lake trace JSON in {path!r}: {error}" + ) from error + + +def _hash_stream( + stream: BinaryIO, + expected_size: int, + path: str, + *, + canonicalize_trace: bool, +) -> FileContent: + if canonicalize_trace: + if expected_size > MAX_CANONICAL_TRACE_BYTES: + raise ArchiveInspectionError( + f"Lake trace {path!r} exceeds the canonicalization limit of " + f"{MAX_CANONICAL_TRACE_BYTES} bytes" + ) + data = stream.read() + if len(data) != expected_size: + raise ArchiveInspectionError( + f"short archive member {path!r}: header says {expected_size} bytes, " + f"read {len(data)}" + ) + canonical = _canonicalize_trace(data, path) + return FileContent( + hashlib.sha256(canonical).hexdigest(), + len(canonical), + canonical_trace=True, + ) + + digest = hashlib.sha256() + size = 0 + while True: + block = stream.read(COPY_CHUNK_SIZE) + if not block: + break + size += len(block) + digest.update(block) + if size != expected_size: + raise ArchiveInspectionError( + f"short archive member {path!r}: header says {expected_size} bytes, read {size}" + ) + return FileContent(digest.hexdigest(), size) + + +def _resolve_content( + path: str, + regular_contents: dict[str, FileContent], + hardlinks: dict[str, str], + visiting: set[str] | None = None, +) -> FileContent: + if path in regular_contents: + return regular_contents[path] + target = hardlinks.get(path) + if target is None: + raise ArchiveInspectionError( + f"hard link ultimately targets unavailable content: {path!r}" + ) + visiting = set() if visiting is None else visiting + if path in visiting: + raise ArchiveInspectionError(f"hard-link cycle involving {path!r}") + visiting.add(path) + try: + return _resolve_content(target, regular_contents, hardlinks, visiting) + finally: + visiting.remove(path) + + +def _forbidden_state(path: str) -> str | None: + parts = path.split("/") + if path.endswith(".ltar"): + return "Lake artifact archive (.ltar)" + if path.endswith(".nobuild"): + return "stale no-build marker (.nobuild)" + if any(part == ".anneal-tmp" or part.endswith(".anneal-tmp") for part in parts): + return "temporary primer state (.anneal-tmp)" + if any( + part == ".lake" and index + 1 < len(parts) and parts[index + 1] == "cache" + for index, part in enumerate(parts) + ): + return "Lake artifact cache (.lake/cache)" + return None + + +def _read_tar_stream( + stream: BinaryIO, + *, + max_members: int, + max_member_bytes: int, + max_archive_bytes: int, +) -> ArchiveInventory: + semantic_files: dict[str, SemanticRecord] = {} + metadata_files: dict[str, SemanticRecord] = {} + pending_files: list[PendingSemanticFile] = [] + regular_contents: dict[str, FileContent] = {} + hardlinks: dict[str, str] = {} + ignored_files: Counter[str] = Counter() + present_paths: set[str] = set() + regular_like_paths: set[str] = set() + top_levels: set[str] = set() + declared_file_bytes = 0 + member_count = 0 + + with tarfile.open(fileobj=stream, mode="r|") as archive: + for member in archive: + member_count += 1 + if member_count > max_members: + raise ArchiveInspectionError( + f"archive has more than the allowed {max_members} members" + ) + + path = _normalize_member_name(member.name) + if path in present_paths: + raise ArchiveInspectionError(f"archive contains duplicate path: {path!r}") + present_paths.add(path) + top_levels.add(path.split("/", 1)[0]) + + forbidden = _forbidden_state(path) + if forbidden is not None: + raise ArchiveInspectionError( + f"archive contains forbidden {forbidden}: {path}" + ) + + is_semantic, category = _classify_file(path) + mode = member.mode & 0o7777 + + if member.isdir(): + record = SemanticRecord(kind="directory", mode=mode) + if is_semantic: + semantic_files[path] = record + else: + metadata_files[path] = record + ignored_files[category] += 1 + continue + + if member.isfile(): + if member.size < 0 or member.size > max_member_bytes: + raise ArchiveInspectionError( + f"archive member {path!r} has disallowed size {member.size}" + ) + declared_file_bytes += member.size + if declared_file_bytes > max_archive_bytes: + raise ArchiveInspectionError( + "archive's declared regular-file contents exceed " + f"the allowed {max_archive_bytes} bytes" + ) + + # Hash every regular file so hard links can be resolved without + # extraction. Metadata records deliberately omit the hash. + extracted = archive.extractfile(member) + if extracted is None: + raise ArchiveInspectionError(f"cannot read regular member: {path}") + canonical_trace = is_semantic and _is_lake_build_trace(path) + with extracted: + regular_contents[path] = _hash_stream( + extracted, + member.size, + path, + canonicalize_trace=canonical_trace, + ) + + regular_like_paths.add(path) + if is_semantic: + pending_files.append( + PendingSemanticFile(path, path, mode, canonical_trace) + ) + else: + metadata_files[path] = SemanticRecord(kind="file", mode=mode) + ignored_files[category] += 1 + continue + + if member.islnk(): + target = _normalize_member_name(member.linkname) + hardlinks[path] = target + regular_like_paths.add(path) + if is_semantic: + pending_files.append( + PendingSemanticFile( + path, + target, + mode, + _is_lake_build_trace(path), + ) + ) + else: + metadata_files[path] = SemanticRecord(kind="file", mode=mode) + ignored_files[category] += 1 + continue + + if member.issym(): + target = _normalize_symlink_target(path, member.linkname) + if is_semantic: + semantic_files[path] = SemanticRecord( + kind="symlink", + mode=mode, + sha256=hashlib.sha256(target.encode("utf-8")).hexdigest(), + size=0, + link_target=target, + ) + else: + metadata_files[path] = SemanticRecord( + kind="symlink", mode=mode, link_target=target + ) + ignored_files[category] += 1 + continue + + raise ArchiveInspectionError( + f"archive contains unsupported special member {path!r} " + f"(tar type {member.type!r})" + ) + + # Validate every hard link, including content-ignored metadata links. + for path in hardlinks: + _resolve_content(path, regular_contents, hardlinks) + + for pending in pending_files: + content = _resolve_content(pending.content_path, regular_contents, hardlinks) + if pending.canonical_trace and not content.canonical_trace: + raise ArchiveInspectionError( + f"Lake trace hard link {pending.path!r} targets non-trace content" + ) + semantic_files[pending.path] = SemanticRecord( + kind="file", + mode=pending.mode, + sha256=content.sha256, + size=content.size, + ) + + return ArchiveInventory( + semantic_files=semantic_files, + metadata_files=metadata_files, + ignored_files=ignored_files, + present_paths=present_paths, + regular_like_paths=regular_like_paths, + top_levels=top_levels, + member_count=member_count, + declared_file_bytes=declared_file_bytes, + ) + + +def _validate_layout(inventory: ArchiveInventory) -> None: + if inventory.top_levels != EXPECTED_TOP_LEVELS: + raise ArchiveInspectionError( + "unexpected top-level archive entries: " + f"expected {sorted(EXPECTED_TOP_LEVELS)}, got {sorted(inventory.top_levels)}" + ) + + missing = REQUIRED_MEMBER_PATHS - inventory.present_paths + if missing: + raise ArchiveInspectionError( + "archive is missing required members: " + ", ".join(sorted(missing)) + ) + + all_records = inventory.comparison_records() + bad_required = { + path + for path in REQUIRED_MEMBER_PATHS + if path not in inventory.regular_like_paths + and (path not in all_records or all_records[path].kind != "symlink") + } + if bad_required: + raise ArchiveInspectionError( + "required members are not files or links: " + ", ".join(sorted(bad_required)) + ) + + not_executable = { + path + for path in REQUIRED_EXECUTABLE_PATHS + if all_records[path].mode & 0o111 == 0 + } + if not_executable: + raise ArchiveInspectionError( + "required commands are not executable: " + + ", ".join(sorted(not_executable)) + ) + + build_outputs = { + path for path in inventory.semantic_files if _is_lake_build_path(path) + } + required_kinds = { + ".olean": any(path.endswith(".olean") for path in build_outputs), + ".ilean": any(path.endswith(".ilean") for path in build_outputs), + ".c": any(path.endswith(".c") for path in build_outputs), + "Mathlib .olean": any( + path.startswith("aeneas/packages/mathlib/.lake/build/") + and path.endswith(".olean") + for path in build_outputs + ), + } + missing_kinds = [name for name, present in required_kinds.items() if not present] + if missing_kinds: + raise ArchiveInspectionError( + "archive lacks expected Lean build output kinds: " + ", ".join(missing_kinds) + ) + + +def inspect_archive( + path: Path, + *, + zstd: str = "zstd", + max_members: int = DEFAULT_MAX_MEMBERS, + max_member_bytes: int = DEFAULT_MAX_MEMBER_BYTES, + max_archive_bytes: int = DEFAULT_MAX_ARCHIVE_BYTES, + validate_layout: bool = True, +) -> ArchiveInventory: + """Safely stream and inventory one ``.tar.zst`` toolchain archive.""" + + requested_path = path + try: + # Nix output links are commonly symlinks. Passing the resolved store + # path also avoids zstd implementations that decline symlink inputs. + path = path.resolve(strict=True) + except OSError as error: + raise ArchiveInspectionError( + f"cannot resolve archive {requested_path}: {error}" + ) from error + if not path.is_file(): + raise ArchiveInspectionError( + f"archive is not a regular file: {requested_path} (resolved to {path})" + ) + try: + with path.open("rb") as archive_file: + if archive_file.read(len(ZSTD_MAGIC)) != ZSTD_MAGIC: + raise ArchiveInspectionError(f"archive is not a standard zstd frame: {path}") + except OSError as error: + raise ArchiveInspectionError(f"cannot read archive {path}: {error}") from error + + stderr_file = tempfile.TemporaryFile() + try: + try: + process = subprocess.Popen( + [zstd, "--decompress", "--stdout", "--quiet", "--", os.fspath(path)], + stdout=subprocess.PIPE, + stderr=stderr_file, + ) + except OSError as error: + raise ArchiveInspectionError(f"cannot execute {zstd!r}: {error}") from error + + assert process.stdout is not None + inventory: ArchiveInventory | None = None + inspection_error: Exception | None = None + try: + inventory = _read_tar_stream( + process.stdout, + max_members=max_members, + max_member_bytes=max_member_bytes, + max_archive_bytes=max_archive_bytes, + ) + except Exception as error: # Preserve zstd diagnostics below. + inspection_error = error + finally: + process.stdout.close() + + if inspection_error is not None and process.poll() is None: + process.terminate() + try: + return_code = process.wait(timeout=10) + except subprocess.TimeoutExpired: + process.kill() + return_code = process.wait() + + stderr_file.seek(0) + stderr = stderr_file.read().decode("utf-8", errors="replace").strip() + if inspection_error is not None: + detail = f"; zstd: {stderr}" if stderr else "" + if isinstance(inspection_error, ArchiveInspectionError): + raise ArchiveInspectionError( + f"{path}: {inspection_error}{detail}" + ) from inspection_error + raise ArchiveInspectionError( + f"failed to read tar stream from {path}: {inspection_error}{detail}" + ) from inspection_error + if return_code != 0: + raise ArchiveInspectionError( + f"zstd failed for {path} with exit code {return_code}: {stderr}" + ) + assert inventory is not None + finally: + stderr_file.close() + + if validate_layout: + _validate_layout(inventory) + return inventory + + +def compare_inventories( + first: ArchiveInventory, second: ArchiveInventory +) -> ComparisonResult: + first_records = first.comparison_records() + second_records = second.comparison_records() + first_paths = set(first_records) + second_paths = set(second_records) + common = first_paths & second_paths + changed = tuple( + sorted(path for path in common if first_records[path] != second_records[path]) + ) + return ComparisonResult( + only_first=tuple(sorted(first_paths - second_paths)), + only_second=tuple(sorted(second_paths - first_paths)), + changed=changed, + ) + + +def _format_size(size: int) -> str: + value = float(size) + for suffix in ("B", "KiB", "MiB", "GiB", "TiB"): + if value < 1024 or suffix == "TiB": + return f"{value:.1f} {suffix}" + value /= 1024 + raise AssertionError("unreachable") + + +def _print_inventory(label: str, path: Path, inventory: ArchiveInventory) -> None: + semantic_bytes = sum( + record.size for record in inventory.semantic_files.values() if record.kind == "file" + ) + ignored = ", ".join( + f"{category}={count}" for category, count in sorted(inventory.ignored_files.items()) + ) + print( + f"{label}: {path}\n" + f" {len(inventory.semantic_files)} semantic entries " + f"({_format_size(semantic_bytes)}), {inventory.member_count} archive members" + ) + if ignored: + print(f" ignored metadata: {ignored}") + + +def _print_paths(heading: str, paths: Iterable[str], limit: int) -> None: + paths = tuple(paths) + if not paths: + return + print(f"{heading} ({len(paths)}):") + for path in paths[:limit]: + print(f" {path}") + if len(paths) > limit: + print(f" ... and {len(paths) - limit} more") + + +def _parse_args(argv: list[str]) -> argparse.Namespace: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("first_archive", type=Path, help="first actual .tar.zst archive") + parser.add_argument("second_archive", type=Path, help="second actual .tar.zst archive") + parser.add_argument( + "--zstd", default="zstd", help="zstd executable to use (default: %(default)s)" + ) + parser.add_argument( + "--max-differences", + type=int, + default=50, + help="maximum paths to print in each difference category (default: %(default)s)", + ) + parser.add_argument( + "--max-members", type=int, default=DEFAULT_MAX_MEMBERS, help=argparse.SUPPRESS + ) + parser.add_argument( + "--max-member-bytes", + type=int, + default=DEFAULT_MAX_MEMBER_BYTES, + help=argparse.SUPPRESS, + ) + parser.add_argument( + "--max-archive-bytes", + type=int, + default=DEFAULT_MAX_ARCHIVE_BYTES, + help=argparse.SUPPRESS, + ) + args = parser.parse_args(argv) + for name in ( + "max_differences", + "max_members", + "max_member_bytes", + "max_archive_bytes", + ): + if getattr(args, name) <= 0: + parser.error(f"--{name.replace('_', '-')} must be positive") + return args + + +def main(argv: list[str] | None = None) -> int: + args = _parse_args(sys.argv[1:] if argv is None else argv) + inspect_kwargs = { + "zstd": args.zstd, + "max_members": args.max_members, + "max_member_bytes": args.max_member_bytes, + "max_archive_bytes": args.max_archive_bytes, + } + try: + first = inspect_archive(args.first_archive, **inspect_kwargs) + second = inspect_archive(args.second_archive, **inspect_kwargs) + except ArchiveInspectionError as error: + print(f"ERROR: {error}", file=sys.stderr) + return 2 + + _print_inventory("first", args.first_archive, first) + _print_inventory("second", args.second_archive, second) + result = compare_inventories(first, second) + if result.equivalent: + print("Archives are semantically equivalent.") + return 0 + + print("Archives are NOT semantically equivalent.", file=sys.stderr) + _print_paths("Only in first archive", result.only_first, args.max_differences) + _print_paths("Only in second archive", result.only_second, args.max_differences) + if result.changed: + print(f"Different content, type, or mode ({len(result.changed)}):") + first_records = first.comparison_records() + second_records = second.comparison_records() + for path in result.changed[: args.max_differences]: + print(f" {path}") + print(f" first: {first_records[path].short_description()}") + print(f" second: {second_records[path].short_description()}") + if len(result.changed) > args.max_differences: + print(f" ... and {len(result.changed) - args.max_differences} more") + return 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/anneal/v2/flake.nix b/anneal/v2/flake.nix index 5a219f4bc5..97aa59546e 100644 --- a/anneal/v2/flake.nix +++ b/anneal/v2/flake.nix @@ -223,6 +223,149 @@ runHook postInstall ''; }; + + buildAeneas = { mode, prepared, seed ? null }: + let + fast = mode == "fast"; + # Build exactly the same package-library inventory in both modes. + # The fast build replays candidate artifacts; the slow build + # produces the corresponding artifacts from Lean sources. + fullPackageTargets = "@Cli/Cli @batteries/Batteries @Qq/Qq @aesop/Aesop @proofwidgets/ProofWidgets @importGraph/ImportGraph @LeanSearchClient/LeanSearchClient @plausible/Plausible @mathlib/Mathlib"; + in + pkgs.stdenv.mkDerivation ({ + pname = "aeneas-compiled-${mode}"; + version = "0.1.0"; + + # Lake records content hashes for its native artifacts. Preserve + # those bytes after validation; the omnibus derivation only + # normalizes executables outside `.lake`. + dontPatchShebangs = true; + dontPatchELF = true; + dontStrip = true; + + src = pkgs.runCommand "empty-src" {} "mkdir $out"; + + inherit prepared; + leanToolchain = self.packages.${system}.lean-toolchain; + + nativeBuildInputs = with pkgs; [ + python3 + gnutar + zstd + ]; + + buildPhase = builtins.concatStringsSep "\n" ( + [ + "export HOME=$TMPDIR/home" + "export XDG_CACHE_HOME=$TMPDIR/cache" + "mkdir -p \"$HOME\" \"$XDG_CACHE_HOME\"" + "unset CI" + "export PATH=\"$leanToolchain/bin:\$PATH\"" + "export LEAN_SYSROOT=\"$leanToolchain\"" + # Let sandboxed Lean executables find libleanshared.so. + "export LD_LIBRARY_PATH=\"$leanToolchain/lib:$leanToolchain/lib/lean:\$LD_LIBRARY_PATH\"" + # Every dependency is already vendored, and both builders must + # stay offline after the shared preparation cut point. + "export MATHLIB_NO_CACHE_ON_UPDATE=1" + "mkdir -p aeneas" + "cp -r $prepared/. aeneas/" + "chmod -R +w aeneas" + ] + ++ pkgs.lib.optionals fast [ + "cp -r $seed/. aeneas/" + "chmod -R +w aeneas" + "test -f aeneas/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Merge.olean" + ] + ++ pkgs.lib.optionals (!fast) [ + "if find aeneas -type d -name .lake -print -quit | grep -q .; then" + " echo \"ERROR: the slow build received prebuilt .lake state\" >&2" + " exit 1" + "fi" + "if find aeneas -type f \\( -name '*.hash' -o -name '*.olean' -o -name '*.ilean' \\) -print -quit | grep -q .; then" + " echo \"ERROR: the slow build received prebuilt Lean artifacts\" >&2" + " exit 1" + "fi" + ] + ++ [ + # Copying can assign fresh directory mtimes. Source/config + # files are normalized in both modes so only the fast cache + # artifacts are newer when old mode checks them. + "find 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' {} +" + "cd aeneas/backends/lean" + ] + ++ pkgs.lib.optionals fast [ + # Materialize the same complete library target inventory as the + # clean oracle. Existing candidate artifacts are accepted by + # mtime, so only absent cache entries require compilation. + (runLeanCommand "lake --no-cache --old build ${fullPackageTargets}") + (runLeanCommand "lake --no-cache --old build") + "test -f ../../packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Merge.olean" + ] + ++ pkgs.lib.optionals (!fast) [ + # There is no `.lake` state at this point. Build every vendored + # Lean library before the root package so the oracle covers the + # same candidate-artifact inventory without using its bytes. + (runLeanCommand "lake --no-cache --rehash -R build ${fullPackageTargets}") + (runLeanCommand "lake --no-cache --rehash -R build") + ] + ++ [ + # FIXME: Remove this v1-only workspace primer once generated + # workspaces migrate to v2. + "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" + "cp ${./prime-lakefile.lean} $TMPDIR/aeneas-config-primer/lakefile.lean" + "chmod +w $TMPDIR/aeneas-config-primer/lakefile.lean" + "substituteInPlace $TMPDIR/aeneas-config-primer/lakefile.lean --replace-fail @AENEAS_ROOT@ \"$PWD\"" + ] + ++ pkgs.lib.optionals fast [ + # This is the fast path's sole trace refresh traversal. + "(cd $TMPDIR/aeneas-config-primer && ${runLeanCommand "lake --no-cache run Anneal.refreshLakeTraces generated/Generated.lean"})" + ] + ++ pkgs.lib.optionals (!fast) [ + # Build the clean result in the same dependency context used by + # InfoView, without invoking the fast trace promotion script. + "(cd $TMPDIR/aeneas-config-primer && ${runLeanCommand "lake --no-cache --rehash -R setup-file generated/Generated.lean --quiet >/dev/null"})" + ] + ++ [ + "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:]=:])/[A-Za-z0-9._~-]'" + "if find . ../../packages -type f -name '*.trace' -exec grep -EIl \"\$TRACE_ABS_RE\" {} + | tee /tmp/non-relocatable-traces | grep -q .; then" + " echo \"ERROR: non-relocatable paths remain in Lake trace files\" >&2" + " cat /tmp/non-relocatable-traces >&2" + " exit 1" + "fi" + # Apply exactly the same closure pruning to the two builds. + "python3 ${./prune-lake-cache.py} --project-root . --packages-root ../../packages" + # This is a read-only assertion, not a repair round: ordinary + # hash-mode InfoView setup must accept the finished package tree. + "chmod -R a-w . ../../packages" + "(cd $TMPDIR/aeneas-config-primer && ${runLeanCommand "lake --no-cache setup-file generated/Generated.lean --no-build --quiet >/dev/null"})" + "if find . ../../packages -type f \\( -name '*.trace.nobuild' -o -name '*.anneal-tmp' \\) -print -quit | grep -q .; then" + " echo \"ERROR: Lake setup-file left repair metadata behind\" >&2" + " exit 1" + "fi" + "cd ../.." + "mkdir -p $out/backends $out/packages $out/bin" + "cp -r backends/lean $out/backends/" + "cp -r packages/* $out/packages/" + "cp -r bin/* $out/bin/" + ] + ); + } + // pkgs.lib.optionalAttrs fast { + inherit seed; + } + // pkgs.lib.optionalAttrs pkgs.stdenv.isDarwin { + preFixup = '' + # nixpkgs' Darwin fixup hook otherwise rewrites every cached + # `.dylib`/`.so` after Lake records its content hash. + fixDarwinDylibNamesIn() { :; } + ''; + }); in { packages.aeneas-download = fetchAeneas { @@ -392,127 +535,132 @@ ]; }; - # Builds the Aeneas Lean backend against vendored, relative Lake paths. - packages.aeneas-compiled = pkgs.stdenv.mkDerivation ({ - pname = "aeneas-compiled"; + # One immutable, Lean-artifact-free tree supplies identical rewritten + # sources, package topology, metadata, mtimes, and runtime tools to both + # build modes. ProofWidgets' pre-generated JavaScript and its two + # custom-target traces are source inputs; the slow builder never + # receives the candidate `.lake` seed below. + packages.aeneas-prepared-sources = pkgs.stdenv.mkDerivation ({ + pname = "aeneas-prepared-sources"; version = "0.1.0"; - # Lake records content hashes for its native artifacts. Preserve - # those bytes after the final trace refresh; runtime binaries are - # normalized later when the omnibus archive is staged. + dontPatchShebangs = true; dontPatchELF = true; dontStrip = true; src = pkgs.runCommand "empty-src" {} "mkdir $out"; - - leanToolchain = self.packages.${system}.lean-toolchain; - mathlibCache = self.packages.${system}.mathlib-cache-unpacked; aeneasUnpacked = self.packages.${system}.aeneas-unpacked; + mathlibSources = self.packages.${system}.mathlib-cache-download; - nativeBuildInputs = with pkgs; [ - python3 - gnutar - zstd + nativeBuildInputs = with pkgs; [ python3 ]; + + buildPhase = builtins.concatStringsSep "\n" [ + "mkdir -p $out/backends $out/packages $out/bin" + "cp -r $aeneasUnpacked/backends/lean $out/backends/" + "cp -r $mathlibSources/packages/* $out/packages/" + "cp \$(find $aeneasUnpacked -maxdepth 1 -type f -executable) $out/bin/" + "chmod -R +w $out" + # Delete every candidate artifact before the common cut point. + "find $out -type d \\( -name .lake -o -name .git \\) -prune -exec rm -rf {} +" + "python3 ${./rewrite-lake-vendor.py} --root $out/backends/lean --packages-dir $out/packages" + "find $out -exec touch -h -d '1970-01-01 00:00:00' {} +" + "if find $out -type d -name .lake -print -quit | grep -q .; then" + " echo \"ERROR: prepared sources still contain a .lake directory\" >&2" + " exit 1" + "fi" + "if find $out -type f \\( -name '*.hash' -o -name '*.olean' -o -name '*.ilean' -o -name '*.ltar' \\) -print -quit | grep -q .; then" + " echo \"ERROR: prepared sources still contain a Lake build artifact\" >&2" + " exit 1" + "fi" + "if find $out -type f -name '*.trace' ! -path \"$out/packages/proofwidgets/widget/package-lock.json.trace\" ! -path \"$out/packages/proofwidgets/widget/js/lake.trace\" -print -quit | grep -q .; then" + " echo \"ERROR: prepared sources contain an unexpected non-.lake trace\" >&2" + " exit 1" + "fi" + "if grep -RFl -e \"$aeneasUnpacked\" -e \"$mathlibSources\" $out >/tmp/prepared-store-paths; then" + " echo \"ERROR: prepared sources retain input-store paths\" >&2" + " cat /tmp/prepared-store-paths >&2" + " exit 1" + "fi" ]; + } // pkgs.lib.optionalAttrs pkgs.stdenv.isDarwin { + preFixup = '' + fixDarwinDylibNamesIn() { :; } + ''; + }); + + # Candidate `.lake` state is isolated from the shared source output. + # Only the fast builder has this derivation in its input graph. + packages.aeneas-prepared-cache = pkgs.stdenv.mkDerivation ({ + pname = "aeneas-prepared-cache"; + version = "0.1.0"; + + dontPatchShebangs = true; + dontPatchELF = true; + dontStrip = true; + + src = pkgs.runCommand "empty-src" {} "mkdir $out"; + aeneasUnpacked = self.packages.${system}.aeneas-unpacked; + mathlibCache = self.packages.${system}.mathlib-cache-unpacked; buildPhase = builtins.concatStringsSep "\n" [ - "export HOME=$TMPDIR" - "export PATH=\"$leanToolchain/bin:\$PATH\"" - "export LEAN_SYSROOT=\"$leanToolchain\"" - # Let sandboxed Lean executables find libleanshared.so. - "export LD_LIBRARY_PATH=\"$leanToolchain/lib:$leanToolchain/lib/lean:\$LD_LIBRARY_PATH\"" - # The cache was fetched in the FOD; do not fetch it again here. - "export MATHLIB_NO_CACHE_ON_UPDATE=1" - "mkdir -p aeneas/backends aeneas/packages" - "cp -r $aeneasUnpacked/backends/lean aeneas/backends/lean" - "chmod -R +w aeneas" - "cd aeneas/backends/lean" - "cp -r $mathlibCache/packages/* ../../packages/" - "chmod -R +w ../../packages" - # In the final archive, every Lake dependency is vendored as a path - # package. Seed those path packages with the build products that - # `lake exe cache get-` originally unpacked into Lake's ordinary - # project cache layout so the offline build does not need to rebuild - # Mathlib or its dependencies from source. - "mkdir -p ../../packages/mathlib/.lake" - "cp -r $mathlibCache/.lake/build ../../packages/mathlib/.lake/" + "mkdir -p $out/backends/lean $out/packages" + "cp -r $aeneasUnpacked/backends/lean/.lake $out/backends/lean/" + "for package_dir in $mathlibCache/packages/*; do" + " package_name=\$(basename \"$package_dir\")" + " if [ -d \"$package_dir/.lake\" ]; then" + " mkdir -p \"$out/packages/$package_name/.lake\"" + " cp -r \"$package_dir/.lake/.\" \"$out/packages/$package_name/.lake/\"" + " fi" + "done" + "mkdir -p $out/packages/mathlib/.lake" + "cp -r $mathlibCache/.lake/build $out/packages/mathlib/.lake/" + "chmod -R +w $out" "if [ -d $mathlibCache/.lake/packages ]; then" " for cached_pkg in $mathlibCache/.lake/packages/*; do" - " pkg_name=\$(basename \"\$cached_pkg\")" - " if [ -d \"\$cached_pkg/.lake\" ] && [ -d \"../../packages/\$pkg_name\" ]; then" - " mkdir -p \"../../packages/\$pkg_name/.lake\"" - " cp -r \"\$cached_pkg/.lake/.\" \"../../packages/\$pkg_name/.lake/\"" + " package_name=\$(basename \"$cached_pkg\")" + " if [ -d \"$cached_pkg/.lake\" ]; then" + " mkdir -p \"$out/packages/$package_name/.lake\"" + " cp -r \"$cached_pkg/.lake/.\" \"$out/packages/$package_name/.lake/\"" " fi" " done" - " chmod -R +w ../../packages" - "fi" - "python3 ${./rewrite-lake-vendor.py} --root . --packages-dir ../../packages" - # Rewriting Git dependencies to final vendored path dependencies - # changes Lake's dependency hashes even though the source content and - # cached artifacts came from the same upstream revision. Run the - # archive verification build in Lake's old mtime mode and make the - # rewritten source/config inputs older than the already-unpacked - # cache artifacts so Lake accepts the cache instead of deleting it - # and trying to rebuild Mathlib from source in the Nix sandbox. - "find . ../../packages -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\" {} +" - "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 workspace primer once generated - # workspaces migrate to v2. - # Anneal v1 generated workspaces require this package directly - # from the installed archive. Prime both the named package config - # and hash-mode build traces that `lake setup-file` 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" - "cp ${./prime-lakefile.lean} $TMPDIR/aeneas-config-primer/lakefile.lean" - "chmod +w $TMPDIR/aeneas-config-primer/lakefile.lean" - "substituteInPlace $TMPDIR/aeneas-config-primer/lakefile.lean --replace-fail @AENEAS_ROOT@ \"$PWD\"" - # `refreshLakeTraces` runs the same setup graph as Lean's language - # server once in old mode, computes real artifact hashes, and only - # publishes all exact hash-mode module traces after it succeeds. - "(cd $TMPDIR/aeneas-config-primer && ${runLeanCommand "lake run Anneal.refreshLakeTraces generated/Generated.lean"})" - "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" - " echo \"ERROR: non-relocatable paths remain in Lake trace files\" >&2" - " cat /tmp/non-relocatable-traces >&2" - " exit 1" "fi" - # Prune unused Lean modules and bulky upstream metadata. - "python3 ${./prune-lake-cache.py} --project-root . --packages-root ../../packages" - # This is an assertion, not another refresh round: the ordinary - # hash-mode command used by Lean InfoView must accept the finished - # package tree without writing any repair metadata. - "chmod -R a-w . ../../packages" - "(cd $TMPDIR/aeneas-config-primer && ${runLeanCommand "lake setup-file generated/Generated.lean --no-build --no-cache --quiet >/dev/null"})" - "if find . ../../packages -type f -name \"*.trace.nobuild\" -print -quit | grep -q .; then" - " echo \"ERROR: Lake setup-file left no-build repair traces behind\" >&2" + # A clean build records reference usages from `...? ... says ...` + # terms that these two candidate `.ilean` files omit. Their + # `.olean` files are byte-identical to the clean result. Leave just + # the stale code-intelligence outputs absent so the fast build + # regenerates them while replaying the rest of the candidate cache. + "for ilean in backends/lean/.lake/build/lib/lean/Aeneas/Tactic/Step/Step.ilean packages/mathlib/.lake/build/lib/lean/Mathlib/Tactic/NormNum/Ineq.ilean; do" + " rm -f \"$out/$ilean\" \"$out/$ilean.hash\"" + "done" + "test -f $out/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Merge.olean" + "if find $out -type f ! -path '*/.lake/*' -print -quit | grep -q .; then" + " echo \"ERROR: prepared cache contains a file outside .lake\" >&2" " exit 1" "fi" - "cd ../.." - "mkdir -p $out/backends $out/packages" - "cp -r backends/lean $out/backends/" - "cp -r packages/* $out/packages/" - "mkdir -p $out/bin" - "cp \$(find $aeneasUnpacked -maxdepth 1 -type f -executable) $out/bin/" ]; } // pkgs.lib.optionalAttrs pkgs.stdenv.isDarwin { preFixup = '' - # nixpkgs' Darwin fixup hook otherwise rewrites every cached - # `.dylib`/`.so` after Lake records its content hash. fixDarwinDylibNamesIn() { :; } ''; }); + packages.aeneas-compiled-fast = buildAeneas { + mode = "fast"; + prepared = self.packages.${system}.aeneas-prepared-sources; + seed = self.packages.${system}.aeneas-prepared-cache; + }; + + packages.aeneas-compiled-slow = buildAeneas { + mode = "slow"; + prepared = self.packages.${system}.aeneas-prepared-sources; + }; + + # Existing users and releases retain the efficient implementation. + packages.aeneas-compiled = self.packages.${system}.aeneas-compiled-fast; + # Stages the relocatable toolchain bundle before compression. - packages.omnibus-tar = pkgs.stdenv.mkDerivation { - pname = "anneal-toolchain-omnibus-tar"; + packages.omnibus-tar-fast = pkgs.stdenv.mkDerivation { + pname = "anneal-toolchain-omnibus-tar-fast"; version = "0.1.0"; src = pkgs.runCommand "empty-src" {} "mkdir $out"; @@ -524,7 +672,7 @@ file ]; - aeneasBuild = self.packages.${system}.aeneas-compiled; + aeneasBuild = self.packages.${system}.aeneas-compiled-fast; rustToolchain = self.packages.${system}.rust-toolchain; leanToolchain = self.packages.${system}.lean-toolchain; @@ -540,6 +688,15 @@ "mkdir -p $TMPDIR/dist_staging/aeneas" "cp -r $aeneasBuild/* $TMPDIR/dist_staging/aeneas/" "chmod -R +w $TMPDIR/dist_staging/aeneas" + # Setup descriptions are compiler invocation scratch files. Three + # upstream Batteries cache entries also retain export lists that a + # clean build no longer produces; other export lists are required + # by AeneasMeta's native closure and must remain in the archive. + "find $TMPDIR/dist_staging/aeneas -type f -name '*.setup.json' -delete" + "for export in Batteries/Data/Array/Match Batteries/Data/String/Basic Batteries/Data/String/Matcher; do" + " rm -f \"$TMPDIR/dist_staging/aeneas/packages/batteries/.lake/build/ir/$export.c.o.export\"" + " rm -f \"$TMPDIR/dist_staging/aeneas/packages/batteries/.lake/build/ir/$export.c.o.export.hash\"" + "done" ] ++ pkgs.lib.optionals pkgs.stdenv.isLinux [ # Remove Nix dynamic-linker and RPATH references from ELF binaries. "echo \"Cleaning up Nix store references...\"" @@ -558,7 +715,7 @@ " fi" "done" ] ++ [ - "TRACE_ABS_RE='(^|[\"[:space:]=:])/(nix/store|build|private/tmp/nix-build|ANNEAL_PLACEHOLDER_ROOT)'" + "TRACE_ABS_RE='(^|[\"[:space:]=:])/[A-Za-z0-9._~-]'" "if find $TMPDIR/dist_staging -type f -name \"*.trace\" -exec grep -EIl \"\$TRACE_ABS_RE\" {} + | tee /tmp/non-relocatable-staged-traces | grep -q .; then" " echo \"ERROR: non-relocatable paths remain in staged Lake trace files\" >&2" " cat /tmp/non-relocatable-staged-traces >&2" @@ -577,10 +734,17 @@ ]); }; + packages.omnibus-tar-slow = self.packages.${system}.omnibus-tar-fast.overrideAttrs (_: { + pname = "anneal-toolchain-omnibus-tar-slow"; + aeneasBuild = self.packages.${system}.aeneas-compiled-slow; + }); + + packages.omnibus-tar = self.packages.${system}.omnibus-tar-fast; + # Final compressed toolchain archive. This is the local-development # default, so keep compression fast. - packages.omnibus-archive = pkgs.stdenv.mkDerivation { - pname = "anneal-toolchain-omnibus"; + packages.omnibus-archive-fast = pkgs.stdenv.mkDerivation { + pname = "anneal-toolchain-omnibus-fast"; version = "0.1.0"; src = pkgs.runCommand "empty-src" {} "mkdir $out"; @@ -589,7 +753,7 @@ zstd ]; - omnibusTar = self.packages.${system}.omnibus-tar; + omnibusTar = self.packages.${system}.omnibus-tar-fast; ANNEAL_ZSTD_LEVEL = 1; @@ -600,21 +764,34 @@ ]; }; + packages.omnibus-archive-slow = self.packages.${system}.omnibus-archive-fast.overrideAttrs (_: { + pname = "anneal-toolchain-omnibus-slow"; + omnibusTar = self.packages.${system}.omnibus-tar-slow; + }); + + packages.omnibus-archive = self.packages.${system}.omnibus-archive-fast; + # CI caches this archive across runs, so use a moderate compression # level that keeps cache/artifact size under control without making # from-scratch PR rebuilds pay the level-19 CPU cost. - packages.omnibus-archive-ci = self.packages.${system}.omnibus-archive.overrideAttrs (_: { + packages.omnibus-archive-ci-fast = self.packages.${system}.omnibus-archive-fast.overrideAttrs (_: { ANNEAL_ZSTD_LEVEL = 6; }); - packages.omnibus-archive-layout-check = + packages.omnibus-archive-ci-slow = self.packages.${system}.omnibus-archive-slow.overrideAttrs (_: { + ANNEAL_ZSTD_LEVEL = 6; + }); + + packages.omnibus-archive-ci = self.packages.${system}.omnibus-archive-ci-fast; + + packages.omnibus-archive-layout-check-fast = pkgs.runCommand "anneal-toolchain-omnibus-layout-check" { nativeBuildInputs = with pkgs; [ gnutar zstd ]; - archive = self.packages.${system}.omnibus-archive-ci; + archive = self.packages.${system}.omnibus-archive-ci-fast; } '' set -euo pipefail @@ -668,6 +845,15 @@ cp "$TMPDIR/archive/entries" "$out/entries" ''; + packages.omnibus-archive-layout-check-slow = + self.packages.${system}.omnibus-archive-layout-check-fast.overrideAttrs (_: { + name = "anneal-toolchain-omnibus-layout-check-slow"; + archive = self.packages.${system}.omnibus-archive-ci-slow; + }); + + packages.omnibus-archive-layout-check = + self.packages.${system}.omnibus-archive-layout-check-fast; + packages.rust-toolchain = fetchRustToolchain { inherit rustDate; sha256 = rustToolchainSha256; diff --git a/anneal/v2/prune-lake-cache.py b/anneal/v2/prune-lake-cache.py index b0eb8eaa5e..ecde676a97 100644 --- a/anneal/v2/prune-lake-cache.py +++ b/anneal/v2/prune-lake-cache.py @@ -156,7 +156,8 @@ def prune_package(pkg_dir: Path, mathlib_closure: set[str] | None) -> None: print(f"Pruning package at: {pkg_dir}") traces_dir = pkg_dir / ".lake" / "build" / "lib" / "lean" if not traces_dir.exists(): - print(f"No build traces found for {pkg_dir}, skipping pruning.") + print(f"No build traces found for {pkg_dir}; pruning package metadata only.") + remove_package_metadata(pkg_dir) return all_lean_files = [] diff --git a/anneal/v2/rewrite-lake-vendor.py b/anneal/v2/rewrite-lake-vendor.py index e61fc99283..966dcaf3a9 100755 --- a/anneal/v2/rewrite-lake-vendor.py +++ b/anneal/v2/rewrite-lake-vendor.py @@ -34,7 +34,13 @@ def package_dirs(packages_dir: Path) -> dict[str, Path]: def replace_require_toml_blocks(path: Path, packages: dict[str, Path]) -> bool: content = path.read_text() - block_re = re.compile(r"(?ms)^\s*\[\[require\]\]\s*\n(?:(?!^\s*\[\[).*\n?)*") + # Match one TOML array-table block line by line. Using DOTALL here makes + # `.*` consume later `[[lean_lib]]` and other array tables, silently + # deleting package targets when the require block is replaced. + block_re = re.compile( + r"(?m)^[ \t]*\[\[require\]\][ \t]*\r?\n" + r"(?:(?!^[ \t]*\[)[^\r\n]*(?:\r?\n|\Z))*" + ) changed = False @@ -151,7 +157,7 @@ def rewrite_trace_prefixes( prefixes = trace_prefixes(root, packages_dir, packages, extra_prefixes) package_root_patterns = [ re.compile( - rf"(?]|$)" + ) count = 0 for trace in [*root.rglob("*.trace"), *(t for p in packages.values() for t in p.rglob("*.trace"))]: @@ -183,6 +195,12 @@ def rewrite_trace_prefixes( new_content = pattern.sub("", new_content) for pattern in root_package_patterns: new_content = pattern.sub("", new_content) + # Release artifacts can be produced outside Nix. Normalize the Lean + # executable and ProofWidgets working directory even when their full + # upstream prefixes are not known to this derivation. + new_content = lean_executable_pattern.sub("lean/bin/lean", new_content) + if "proofwidgets/widget/" in trace.as_posix(): + new_content = proofwidgets_root_pattern.sub("widget", new_content) if new_content != content: trace.write_text(new_content) count += 1 diff --git a/anneal/v2/tests/test_compare_toolchain_archives.py b/anneal/v2/tests/test_compare_toolchain_archives.py new file mode 100644 index 0000000000..eaf42f6c0c --- /dev/null +++ b/anneal/v2/tests/test_compare_toolchain_archives.py @@ -0,0 +1,458 @@ +#!/usr/bin/env python3 +# +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , 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. + +"""Focused tests for compare-toolchain-archives.py.""" + +from __future__ import annotations + +import importlib.util +import io +import json +import shutil +import subprocess +import sys +import tarfile +import tempfile +import unittest +from pathlib import Path + + +SCRIPT = Path(__file__).resolve().parents[1] / "compare-toolchain-archives.py" +SPEC = importlib.util.spec_from_file_location("compare_toolchain_archives", SCRIPT) +assert SPEC is not None and SPEC.loader is not None +compare_toolchain_archives = importlib.util.module_from_spec(SPEC) +sys.modules[SPEC.name] = compare_toolchain_archives +SPEC.loader.exec_module(compare_toolchain_archives) + + +FileEntry = tuple[str, bytes, int] +HardLinkEntry = tuple[str, str, int] + + +def ilean_bytes( + *, + usages: list[list[object]] | None = None, + decls: dict[str, object] | None = None, + reference_key: str = "ref-key", + definition: object = None, +) -> bytes: + document = { + "decls": {"Aeneas.test": [1, 2, 3, 4]} if decls is None else decls, + "directImports": [["Init", False, False, False]], + "module": "Aeneas", + "references": { + reference_key: { + "definition": definition, + "usages": [[1, 2, 3, 4, "Aeneas.test"]] + if usages is None + else usages, + } + }, + "version": 5, + } + return json.dumps(document, separators=(",", ":"), sort_keys=True).encode() + + +def trace_bytes( + *, + dep_hash: str = "0123456789abcdef", + output_hash: str = "fedcba9876543210", + context: str = "context", +) -> bytes: + document = { + "schemaVersion": "2025-09-10", + "depHash": dep_hash, + "outputs": {"i": f"{output_hash}.ilean"}, + "inputs": [[context, "1111111111111111"]], + "log": [{"level": "trace", "message": context}], + "synthetic": False, + } + return json.dumps(document, separators=(",", ":"), sort_keys=True).encode() + + +def minimal_entries() -> list[FileEntry | HardLinkEntry]: + return [ + ("aeneas/bin/aeneas", b"aeneas-bin", 0o755), + ("aeneas/bin/charon", b"charon-bin", 0o755), + ("aeneas/bin/charon-driver", b"charon-driver-bin", 0o755), + ( + "aeneas/backends/lean/.lake/config/aeneas/lakefile.olean", + b"aeneas-config", + 0o444, + ), + ( + "aeneas/packages/mathlib/.lake/config/mathlib/lakefile.olean", + b"mathlib-config", + 0o444, + ), + ("aeneas/packages/mathlib/lake-manifest.json", b"{}\n", 0o444), + ("aeneas/backends/lean/lakefile.lean", b"import Lake\n", 0o444), + ( + "aeneas/backends/lean/.lake/build/lib/lean/Aeneas.olean", + b"aeneas-olean", + 0o444, + ), + ( + "aeneas/backends/lean/.lake/build/lib/lean/Aeneas.ilean", + ilean_bytes(), + 0o444, + ), + ( + "aeneas/backends/lean/.lake/build/ir/Aeneas.c", + b"/* generated C */\n", + 0o444, + ), + ( + "aeneas/packages/mathlib/.lake/build/lib/lean/Mathlib/Init.olean", + b"mathlib-olean", + 0o444, + ), + ("lean/bin/lake", b"lake-bin", 0o755), + ("lean/bin/lean", b"lean-bin", 0o755), + ("lean/lib/lean/Init.olean", b"lean-library", 0o444), + ("rust/bin/cargo", b"cargo-bin", 0o755), + ("rust/bin/rustc", b"rustc-bin", 0o755), + ("rust/lib/rustlib/components", b"rustc\ncargo\n", 0o444), + ] + + +def replace_file( + entries: list[FileEntry | HardLinkEntry], path: str, data: bytes, mode: int +) -> None: + for index, entry in enumerate(entries): + if entry[0] == path: + entries[index] = (path, data, mode) + return + raise AssertionError(f"missing fixture entry: {path}") + + +def make_archive( + directory: Path, + name: str, + entries: list[FileEntry | HardLinkEntry], + *, + compression_level: int = 1, + mtime: int = 0, +) -> Path: + tar_path = directory / f"{name}.tar" + with tarfile.open(tar_path, "w", format=tarfile.PAX_FORMAT) as archive: + for entry in entries: + path = entry[0] + info = tarfile.TarInfo(path) + info.mtime = mtime + info.uid = 123 + info.gid = 456 + if isinstance(entry[1], bytes): + _, data, mode = entry + info.size = len(data) + info.mode = mode + archive.addfile(info, io.BytesIO(data)) + else: + _, target, mode = entry + info.type = tarfile.LNKTYPE + info.linkname = target + info.mode = mode + archive.addfile(info) + + archive_path = directory / f"{name}.tar.zst" + with archive_path.open("wb") as output: + subprocess.run( + ["zstd", "--quiet", f"-{compression_level}", "--stdout", "--", tar_path], + check=True, + stdout=output, + ) + return archive_path + + +@unittest.skipUnless(shutil.which("zstd"), "zstd is required for archive tests") +class CompareToolchainArchivesTests(unittest.TestCase): + def inspect(self, archive: Path): + return compare_toolchain_archives.inspect_archive(archive) + + def test_ignores_only_contextual_metadata_content_differences(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + directory = Path(tmp) + first_entries = minimal_entries() + second_entries = minimal_entries() + trace = "aeneas/backends/lean/.lake/build/lib/lean/Aeneas.trace" + first_entries.append((trace, trace_bytes(context="first context"), 0o444)) + second_entries.append((trace, trace_bytes(context="second context"), 0o444)) + metadata = [ + "aeneas/backends/lean/.lake/build/ir/Aeneas.setup.json", + "aeneas/backends/lean/.lake/build/ir/Aeneas.rsp", + ] + for path in metadata: + first_entries.append((path, b"first context", 0o444)) + second_entries.append((path, b"second context", 0o444)) + replace_file( + second_entries, + "aeneas/backends/lean/.lake/config/aeneas/lakefile.olean", + b"different context-dependent config", + 0o444, + ) + + first = make_archive(directory, "first", first_entries, compression_level=1, mtime=1) + second = make_archive( + directory, "second", second_entries, compression_level=9, mtime=999 + ) + + result = compare_toolchain_archives.compare_inventories( + self.inspect(first), self.inspect(second) + ) + self.assertTrue(result.equivalent) + + def test_ilean_usages_are_semantic(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + directory = Path(tmp) + first_entries = minimal_entries() + second_entries = minimal_entries() + path = "aeneas/backends/lean/.lake/build/lib/lean/Aeneas.ilean" + replace_file( + first_entries, + path, + ilean_bytes(usages=[[1, 2, 3, 4, "Aeneas.test"]]), + 0o444, + ) + replace_file( + second_entries, + path, + ilean_bytes(usages=[[99, 98, 97, 96, "Aeneas.test"]]), + 0o444, + ) + + result = compare_toolchain_archives.compare_inventories( + self.inspect(make_archive(directory, "first", first_entries)), + self.inspect(make_archive(directory, "second", second_entries)), + ) + self.assertEqual(result.changed, (path,)) + + def test_ilean_declarations_reference_keys_and_definitions_are_semantic(self) -> None: + variants = { + "declaration": ilean_bytes(decls={"Aeneas.changed": [1, 2, 3, 4]}), + "reference key": ilean_bytes(reference_key="different-reference"), + "definition": ilean_bytes(definition=[5, 6, 7, 8]), + } + for index, (label, changed_ilean) in enumerate(variants.items()): + with self.subTest(label=label), tempfile.TemporaryDirectory() as tmp: + directory = Path(tmp) + first_entries = minimal_entries() + second_entries = minimal_entries() + path = "aeneas/backends/lean/.lake/build/lib/lean/Aeneas.ilean" + replace_file(second_entries, path, changed_ilean, 0o444) + result = compare_toolchain_archives.compare_inventories( + self.inspect(make_archive(directory, f"first-{index}", first_entries)), + self.inspect(make_archive(directory, f"second-{index}", second_entries)), + ) + self.assertEqual(result.changed, (path,)) + + def test_compares_all_hash_sidecar_content(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + directory = Path(tmp) + first_entries = minimal_entries() + second_entries = minimal_entries() + olean_hash = ( + "aeneas/backends/lean/.lake/build/lib/lean/Aeneas.olean.hash" + ) + ilean_hash = ( + "aeneas/backends/lean/.lake/build/lib/lean/Aeneas.ilean.hash" + ) + first_entries.extend( + [(olean_hash, b"first", 0o444), (ilean_hash, b"first", 0o444)] + ) + second_entries.extend( + [(olean_hash, b"second", 0o444), (ilean_hash, b"second", 0o444)] + ) + + result = compare_toolchain_archives.compare_inventories( + self.inspect(make_archive(directory, "first", first_entries)), + self.inspect(make_archive(directory, "second", second_entries)), + ) + self.assertEqual(result.changed, tuple(sorted((ilean_hash, olean_hash)))) + + def test_compares_trace_dependency_and_output_hashes(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + directory = Path(tmp) + path = "aeneas/backends/lean/.lake/build/lib/lean/Aeneas.trace" + first_entries = minimal_entries() + [(path, trace_bytes(), 0o444)] + variants = { + "dependency": trace_bytes(dep_hash="1111111111111111"), + "output": trace_bytes(output_hash="2222222222222222"), + } + first = self.inspect(make_archive(directory, "first", first_entries)) + for index, (label, changed_trace) in enumerate(variants.items()): + with self.subTest(label=label): + second_entries = minimal_entries() + [(path, changed_trace, 0o444)] + result = compare_toolchain_archives.compare_inventories( + first, + self.inspect( + make_archive(directory, f"second-{index}", second_entries) + ), + ) + self.assertEqual(result.changed, (path,)) + + def test_detects_build_output_and_executable_status_changes(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + directory = Path(tmp) + first_entries = minimal_entries() + second_entries = minimal_entries() + replace_file( + second_entries, + "aeneas/backends/lean/.lake/build/lib/lean/Aeneas.olean", + b"different-olean", + 0o444, + ) + replace_file( + second_entries, + "lean/lib/lean/Init.olean", + b"lean-library", + 0o555, + ) + + first = self.inspect(make_archive(directory, "first", first_entries)) + second = self.inspect(make_archive(directory, "second", second_entries)) + result = compare_toolchain_archives.compare_inventories(first, second) + + self.assertFalse(result.equivalent) + self.assertEqual(result.only_first, ()) + self.assertEqual(result.only_second, ()) + self.assertEqual( + set(result.changed), + { + "aeneas/backends/lean/.lake/build/lib/lean/Aeneas.olean", + "lean/lib/lean/Init.olean", + }, + ) + + def test_rejects_non_executable_required_command(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + directory = Path(tmp) + entries = minimal_entries() + replace_file(entries, "lean/bin/lean", b"lean-bin", 0o644) + with self.assertRaisesRegex( + compare_toolchain_archives.ArchiveInspectionError, + "required commands are not executable", + ): + self.inspect(make_archive(directory, "non-executable", entries)) + + def test_detects_non_aeneas_toolchain_payload_changes(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + directory = Path(tmp) + first_entries = minimal_entries() + second_entries = minimal_entries() + lean_path = "lean/lib/lean/Init.olean" + rust_path = "rust/lib/rustlib/components" + replace_file(second_entries, lean_path, b"different Lean library", 0o444) + replace_file(second_entries, rust_path, b"different Rust components", 0o444) + + result = compare_toolchain_archives.compare_inventories( + self.inspect(make_archive(directory, "first", first_entries)), + self.inspect(make_archive(directory, "second", second_entries)), + ) + self.assertEqual(set(result.changed), {lean_path, rust_path}) + + def test_treats_hard_link_storage_as_equivalent_to_regular_file(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + directory = Path(tmp) + first_entries = minimal_entries() + second_entries = minimal_entries() + output = "aeneas/backends/lean/.lake/build/lib/lean/Aeneas.olean" + shared = "aeneas/backends/lean/.lake/build/lib/lean/Shared.olean" + first_entries.append((shared, b"aeneas-olean", 0o444)) + second_entries.append((shared, b"aeneas-olean", 0o444)) + for index, entry in enumerate(second_entries): + if entry[0] == output: + second_entries[index] = (output, shared, 0o444) + break + else: + self.fail("fixture output not found") + + first = self.inspect(make_archive(directory, "first", first_entries)) + second = self.inspect(make_archive(directory, "second", second_entries)) + result = compare_toolchain_archives.compare_inventories(first, second) + self.assertTrue(result.equivalent) + + def test_metadata_path_and_mode_inventories_must_match(self) -> None: + trace = "aeneas/backends/lean/.lake/build/lib/lean/Extra.trace" + config = "aeneas/backends/lean/.lake/config/aeneas/extra.json" + with tempfile.TemporaryDirectory() as tmp: + directory = Path(tmp) + metadata_entries = [ + (trace, trace_bytes(context="first"), 0o444), + (config, b"first", 0o444), + ] + first_entries = minimal_entries() + metadata_entries + changed_mode = minimal_entries() + [ + (trace, trace_bytes(context="second"), 0o644), + (config, b"second", 0o444), + ] + first = self.inspect(make_archive(directory, "first", first_entries)) + + mode_result = compare_toolchain_archives.compare_inventories( + first, self.inspect(make_archive(directory, "mode", changed_mode)) + ) + self.assertEqual(mode_result.changed, (trace,)) + + for index, missing_path in enumerate((trace, config)): + with self.subTest(missing=missing_path): + missing_entries = minimal_entries() + [ + entry for entry in metadata_entries if entry[0] != missing_path + ] + missing_result = compare_toolchain_archives.compare_inventories( + first, + self.inspect( + make_archive(directory, f"missing-{index}", missing_entries) + ), + ) + self.assertEqual(missing_result.only_first, (missing_path,)) + + def test_resolves_archive_input_symlink(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + directory = Path(tmp) + archive = make_archive(directory, "archive", minimal_entries()) + link = directory / "nix-output-link.tar.zst" + link.symlink_to(archive.name) + inventory = self.inspect(link) + self.assertIn("lean/bin/lean", inventory.semantic_files) + + def test_rejects_parent_relative_archive_member(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + directory = Path(tmp) + entries = minimal_entries() + entries.append(("../escape", b"bad", 0o644)) + archive = make_archive(directory, "unsafe", entries) + with self.assertRaisesRegex( + compare_toolchain_archives.ArchiveInspectionError, + "path contains '\\.\\.'", + ): + self.inspect(archive) + + def test_rejects_forbidden_lake_and_primer_state(self) -> None: + forbidden_paths = { + "ltar": "aeneas/backends/lean/.lake/build/Aeneas.ltar", + "cache": "aeneas/backends/lean/.lake/cache/artifacts/content.olean", + "nobuild": ( + "aeneas/backends/lean/.lake/build/lib/lean/Aeneas.trace.nobuild" + ), + "primer temporary state": "aeneas/backends/lean/.anneal-tmp/output", + } + for index, (label, path) in enumerate(forbidden_paths.items()): + with self.subTest(label=label), tempfile.TemporaryDirectory() as tmp: + directory = Path(tmp) + entries = minimal_entries() + [(path, b"forbidden", 0o444)] + archive = make_archive(directory, f"forbidden-{index}", entries) + with self.assertRaisesRegex( + compare_toolchain_archives.ArchiveInspectionError, + "forbidden", + ): + self.inspect(archive) + + +if __name__ == "__main__": + unittest.main() diff --git a/anneal/v2/tests/test_prune_lake_cache.py b/anneal/v2/tests/test_prune_lake_cache.py index 596603415c..597dc9c60a 100644 --- a/anneal/v2/tests/test_prune_lake_cache.py +++ b/anneal/v2/tests/test_prune_lake_cache.py @@ -105,6 +105,20 @@ def test_keeps_all_non_mathlib_modules(self) -> None: self.assertTrue((package / ".lake" / "build" / "lib" / "lean" / "Aesop" / "Unused.olean").is_file()) self.assertFalse((package / "docs").exists()) + def test_prunes_metadata_without_build_traces(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + package = Path(tmp) / "Cli" + + write(package / "Cli" / "Basic.lean") + write(package / "README.md", "unused package metadata\n") + write(package / ".github" / "workflows" / "ci.yml", "name: unused\n") + + prune_lake_cache.prune_package(package, mathlib_closure=set()) + + self.assertTrue((package / "Cli" / "Basic.lean").is_file()) + self.assertFalse((package / "README.md").exists()) + self.assertFalse((package / ".github").exists()) + if __name__ == "__main__": unittest.main() diff --git a/anneal/v2/tests/test_rewrite_lake_vendor.py b/anneal/v2/tests/test_rewrite_lake_vendor.py index 380b6e763d..5ba3a1b120 100644 --- a/anneal/v2/tests/test_rewrite_lake_vendor.py +++ b/anneal/v2/tests/test_rewrite_lake_vendor.py @@ -31,6 +31,70 @@ def write(path: Path, contents: str = "") -> None: class RewriteLakeVendorTests(unittest.TestCase): + def test_toml_rewrite_preserves_following_array_tables(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + packages_dir = root / "packages" + batteries = packages_dir / "batteries" + batteries.mkdir(parents=True) + lakefile = root / "aesop" / "lakefile.toml" + write( + lakefile, + """name = "aesop" + +[[require]] +name = "batteries" +scope = "leanprover-community" +rev = "v4.30.0-rc2" + +[[lean_lib]] +name = "Aesop" + +[[lean_lib]] +name = "AesopTest" +globs = ["AesopTest.+"] +""", + ) + + changed = rewrite_lake_vendor.replace_require_toml_blocks( + lakefile, {"batteries": batteries} + ) + + self.assertTrue(changed) + rewritten = lakefile.read_text(encoding="utf-8") + self.assertIn('path = "../packages/batteries"', rewritten) + self.assertNotIn("scope =", rewritten) + self.assertNotIn("rev =", rewritten) + self.assertEqual(rewritten.count("[[lean_lib]]"), 2) + self.assertIn('name = "Aesop"', rewritten) + self.assertIn('name = "AesopTest"', rewritten) + + def test_toml_rewrite_preserves_following_regular_table(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + batteries = root / "packages" / "batteries" + batteries.mkdir(parents=True) + lakefile = root / "aesop" / "lakefile.toml" + write( + lakefile, + """[[require]] +name = "batteries" +scope = "leanprover-community" + +[leanOptions] +pp.unicode.fun = true +""", + ) + + changed = rewrite_lake_vendor.replace_require_toml_blocks( + lakefile, {"batteries": batteries} + ) + + self.assertTrue(changed) + rewritten = lakefile.read_text(encoding="utf-8") + self.assertIn("[leanOptions]", rewritten) + self.assertIn("pp.unicode.fun = true", rewritten) + def test_rewrites_upstream_aeneas_backend_trace_prefix(self) -> None: with tempfile.TemporaryDirectory() as tmp: root = Path(tmp) / "aeneas" / "backends" / "lean" @@ -61,6 +125,36 @@ def test_rewrites_upstream_aeneas_backend_trace_prefix(self) -> None: self.assertNotIn("backends/lean", rewritten) self.assertIn("AeneasMeta/Utils.lean", rewritten) + def test_rewrites_external_lean_and_proofwidgets_prefixes(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) / "aeneas" / "backends" / "lean" + packages_dir = Path(tmp) / "aeneas" / "packages" + proofwidgets = packages_dir / "proofwidgets" + trace = proofwidgets / "widget" / "js" / "lake.trace" + write( + trace, + """{ + "log": [{"message": "/Users/wjn/ProofWidgets4/widget> npm run build"}], + "inputs": [["/Users/wjn/ProofWidgets4/widget/src", "1234"]], + "lean": "/var/lib/runner/.elan/toolchains/lean4/bin/lean File.lean" +} +""", + ) + + count = rewrite_lake_vendor.rewrite_trace_prefixes( + root=root, + packages_dir=packages_dir, + packages={"proofwidgets": proofwidgets}, + extra_prefixes=[], + ) + + self.assertEqual(count, 1) + rewritten = trace.read_text(encoding="utf-8") + self.assertNotIn("/Users/wjn", rewritten) + self.assertNotIn("/var/lib", rewritten) + self.assertIn("widget/src", rewritten) + self.assertIn("lean/bin/lean File.lean", rewritten) + if __name__ == "__main__": unittest.main()