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()