From 47d907d6fa27610a0900f075c0bec879777107a9 Mon Sep 17 00:00:00 2001 From: Mark Dittmer Date: Thu, 4 Jun 2026 01:15:33 +0000 Subject: [PATCH] [anneal] Move setup and CI onto Nix archive Share the exocrate installer between Anneal and v2, and have non-v2 Anneal install the same Nix-built omnibus archive that v2 already produces. The generated Lean workspace can then use the archive layout directly instead of cloning and rewriting Lake dependencies at runtime. Update Anneal CI to build the archive with Nix, install it before root tests and example checks, and run the Lean-heavy integration suite serially. The workflow no longer depends on a Docker image that pre-bakes the old setup output. gherrit-pr-id: Gefzjo7bqy3imk4ti4im5wep4jz3upvrm --- .github/workflows/anneal.yml | 505 ++----- anneal/Cargo.lock | 1214 ++------------- anneal/Cargo.toml | 27 +- anneal/Dockerfile | 39 +- anneal/build.rs | 54 + anneal/docker.sh | 18 +- anneal/src/aeneas.rs | 611 +++----- anneal/src/charon.rs | 8 +- anneal/src/main.rs | 12 +- anneal/src/resolve.rs | 70 +- anneal/src/setup.rs | 1295 ++-------------- anneal/src/util.rs | 39 +- .../allow_sorry_fallbacks/expected.stderr | 20 +- .../fixtures/cfg_blind_spot/expected.stderr | 6 +- .../test_7_1_phantom_fn/expected.stderr | 6 +- .../test_7_3_ghost_spec/expected.stderr | 6 +- .../test_8_2_unions/expected.stderr | 14 +- .../expand_output/expected-aeneas.stdout | 7 + .../expand_output/expected-all.stdout | 7 + .../expand_output/expected-anneal.stdout | 1 + .../fixtures/extern_never_verified/out.txt | 10 + .../external_path_dependency/anneal.toml | 11 + .../source/external_dep/Cargo.toml | 4 + .../source/external_dep/src/lib.rs | 3 + .../source/workspace/Cargo.toml | 3 + .../source/workspace/app/Cargo.toml | 7 + .../source/workspace/app/src/lib.rs | 3 + .../generate_output/expected-generate.stdout | 4 +- .../expected.stderr | 142 +- .../source/src/lib.rs | 2 + .../size_of_align_of/source/src/lib.rs | 4 +- .../fixtures/split_artifact/expected.stderr | 6 +- .../fixtures/target_selection/expected.stderr | 6 +- anneal/tests/fixtures/unions/expected.stderr | 14 +- .../fixtures/weird_functions/expected.stderr | 4 +- anneal/tests/integration.rs | 1321 ++++++++++------- anneal/v2/Cargo.lock | 92 +- anneal/v2/chase-aeneas-versions.sh | 14 +- anneal/v2/flake.nix | 36 +- anneal/v2/rewrite-lake-vendor.py | 62 +- exocrate/Cargo.lock | 225 +-- exocrate/Cargo.toml | 5 +- exocrate/src/lib.rs | 84 +- exocrate/src/sync.rs | 4 +- 44 files changed, 1833 insertions(+), 4192 deletions(-) create mode 100644 anneal/tests/fixtures/external_path_dependency/anneal.toml create mode 100644 anneal/tests/fixtures/external_path_dependency/source/external_dep/Cargo.toml create mode 100644 anneal/tests/fixtures/external_path_dependency/source/external_dep/src/lib.rs create mode 100644 anneal/tests/fixtures/external_path_dependency/source/workspace/Cargo.toml create mode 100644 anneal/tests/fixtures/external_path_dependency/source/workspace/app/Cargo.toml create mode 100644 anneal/tests/fixtures/external_path_dependency/source/workspace/app/src/lib.rs diff --git a/.github/workflows/anneal.yml b/.github/workflows/anneal.yml index c30a4b8d3d..20e8600c1b 100644 --- a/.github/workflows/anneal.yml +++ b/.github/workflows/anneal.yml @@ -29,222 +29,20 @@ env: CARGO_ZEROCOPY_AUTO_INSTALL_TOOLCHAIN: 1 jobs: - build_docker_env: - name: Build Docker image - runs-on: ubuntu-latest - permissions: - contents: write # Required to push benchmark data to the storage branch - packages: write # required to push docker caches to ghcr.io - steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - with: - persist-credentials: false - - - name: Set up Docker Buildx - uses: docker/setup-buildx-action@4d04d5d9486b7bd6fa91e7baf45bbb4f8b9deedd # v4.0.0 - - - name: Log in to the Container registry - uses: docker/login-action@9780b0c442fbb1117ed29e0efdff1e18412f7567 # v3.3.0 - with: - registry: ghcr.io - username: ${{ github.actor }} - password: ${{ secrets.GITHUB_TOKEN }} - - - name: Generate sanitized Docker tag - id: docker_tag - env: - REF_NAME: ${{ github.ref_name }} - shell: bash - run: | - echo "tag=${REF_NAME//\//-}" >> "$GITHUB_OUTPUT" - - - name: Get UID/GID - id: get_uid - run: | - echo "uid=$(id -u)" >> "$GITHUB_OUTPUT" - echo "gid=$(id -g)" >> "$GITHUB_OUTPUT" - - - name: Start build timer - id: start_timer - run: echo "start=$(date +%s)" >> "$GITHUB_OUTPUT" - - - name: Build Docker image (Dry Run) - id: build_dry - uses: docker/build-push-action@d08e5c354a6adb9ed34480a06d141179aa583294 # v7.0.0 - with: - context: anneal - file: anneal/Dockerfile - push: false - tags: ghcr.io/google/zerocopy/anneal:${{ steps.docker_tag.outputs.tag }} - provenance: false - # Use zstd compression at level 19 to minimize image size and maximize - # decompression speed on matrix runners. This shifts the heavy - # compression work to the runner used for building the image, saving - # time in the consumer jobs that pull the image. Level 19 is the - # practical maximum for standard use. - outputs: type=image,compression=zstd,compression-level=19,force-compression=true - build-args: | - UID=${{ steps.get_uid.outputs.uid }} - GID=${{ steps.get_uid.outputs.gid }} - cache-from: | - type=registry,ref=ghcr.io/google/zerocopy/anneal-cache:${{ steps.docker_tag.outputs.tag }} - type=registry,ref=ghcr.io/google/zerocopy/anneal-cache:main - # External pull requests have read-only package permissions, so they - # can consume GHCR caches but cannot export updated cache layers. - cache-to: ${{ (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository) && format('type=registry,ref=ghcr.io/google/zerocopy/anneal-cache:{0},mode=max', steps.docker_tag.outputs.tag) || '' }} - - - name: Record build time - env: - START_TIME: ${{ steps.start_timer.outputs.start }} - run: | - end=$(date +%s) - start=$START_TIME - duration=$((end - start)) - echo "Docker Build Time: $duration seconds" - echo "[{\"name\": \"Docker Build Time\", \"unit\": \"seconds\", \"value\": $duration}]" > build_time.json - - - name: Store build time benchmark - uses: benchmark-action/github-action-benchmark@a60cea5bc7b49e15c1f58f411161f99e0df48372 # v1.22.0 - with: - name: Docker Build Time - tool: 'customSmallerIsBetter' - output-file-path: build_time.json - gh-pages-branch: benchmark-data - # External pull requests cannot push benchmark data to the - # `benchmark-data` branch. - auto-push: ${{ github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository }} - save-data-file: ${{ github.ref == 'refs/heads/main' }} - benchmark-data-dir-path: dashboard - fail-on-alert: false - github-token: ${{ secrets.GITHUB_TOKEN }} - - - name: Check if remote image matches - id: check_remote - shell: bash - env: - DOCKER_TAG: ${{ steps.docker_tag.outputs.tag }} - LOCAL_DIGEST: ${{ steps.build_dry.outputs.digest }} - run: | - # Fetch the digest of the remote image - REMOTE_DIGEST=$(docker manifest inspect ghcr.io/google/zerocopy/anneal:$DOCKER_TAG | jq -r '.manifests[0].digest') - - echo "Remote digest: $REMOTE_DIGEST" - echo "Local digest: $LOCAL_DIGEST" - - if [ "$REMOTE_DIGEST" = "$LOCAL_DIGEST" ]; then - echo "match=true" >> "$GITHUB_OUTPUT" - else - echo "match=false" >> "$GITHUB_OUTPUT" - fi - continue-on-error: true # Handle case where remote tag doesn't exist yet - - # The build portion of this step will always be cached thanks to the - # dry-run build above. - - name: Build and push Docker image - # External pull requests cannot write the PR-specific image tag to GHCR; - # trusted runs still push, so unexpected GHCR write failures stay loud. - if: steps.check_remote.outputs.match != 'true' && (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository) - uses: docker/build-push-action@d08e5c354a6adb9ed34480a06d141179aa583294 # v7.0.0 - # NOTE: All arguments here must match the dry-run step above exactly - # in order to ensure we hit the cache for the local build! - with: - context: anneal - file: anneal/Dockerfile - push: true - tags: ghcr.io/google/zerocopy/anneal:${{ steps.docker_tag.outputs.tag }} - provenance: false - outputs: type=image,compression=zstd,compression-level=19,force-compression=true - build-args: | - UID=${{ steps.get_uid.outputs.uid }} - GID=${{ steps.get_uid.outputs.gid }} - cache-from: | - type=registry,ref=ghcr.io/google/zerocopy/anneal-cache:${{ steps.docker_tag.outputs.tag }} - type=registry,ref=ghcr.io/google/zerocopy/anneal-cache:main - # External pull requests have read-only package permissions, so they - # can consume GHCR caches but cannot export updated cache layers. - cache-to: ${{ (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository) && format('type=registry,ref=ghcr.io/google/zerocopy/anneal-cache:{0},mode=max', steps.docker_tag.outputs.tag) || '' }} - - measure_image_size: - # This job measures the size of the Docker image built in the previous step - # and records it to maintain a history of resource usage over time. - name: Measure Docker image size - runs-on: ubuntu-latest - needs: build_docker_env - # We only run this on the main branch (and the test branch for verification) - # to ensure we only track history for merged code. - if: github.ref == 'refs/heads/main' || github.ref == 'refs/heads/anneal-dashboards' - permissions: - contents: write # Required to push benchmark data to the storage branch - packages: read # Required to pull the Docker image from GHCR - steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - with: - persist-credentials: false - - - name: Set up Docker Buildx - uses: docker/setup-buildx-action@4d04d5d9486b7bd6fa91e7baf45bbb4f8b9deedd # v4.0.0 - - - name: Log in to the Container registry - uses: docker/login-action@9780b0c442fbb1117ed29e0efdff1e18412f7567 # v3.3.0 - with: - registry: ghcr.io - username: ${{ github.actor }} - password: ${{ secrets.GITHUB_TOKEN }} - - - name: Generate sanitized Docker tag - # We need to replace slashes in branch names with hyphens to form a valid - # Docker tag, matching the logic used in the build job. - id: docker_tag - env: - REF_NAME: ${{ github.ref_name }} - shell: bash - run: | - echo "tag=${REF_NAME//\//-}" >> "$GITHUB_OUTPUT" - - - name: Pull image - # We pull the image we just built and tag it locally so we can inspect it. - run: | - docker pull ghcr.io/google/zerocopy/anneal:${STEPS_DOCKER_TAG_OUTPUTS_TAG} - docker tag ghcr.io/google/zerocopy/anneal:${STEPS_DOCKER_TAG_OUTPUTS_TAG} anneal-ci:local - env: - STEPS_DOCKER_TAG_OUTPUTS_TAG: ${{ steps.docker_tag.outputs.tag }} - - - name: Measure size - # We use docker image inspect to get the size in bytes and convert it to - # Megabytes for easier reading on the dashboard. - id: measure - run: | - size=$(docker image inspect anneal-ci:local --format '{{.Size}}') - size_mb=$((size / 1024 / 1024)) - echo "Image size: $size_mb MB" - echo "[{\"name\": \"Docker Image Size\", \"unit\": \"Megabytes\", \"value\": $size_mb}]" > output.json - - - name: Store benchmark result - # We use github-action-benchmark to manage the history of image sizes. - # It is configured to store results in a dedicated branch to avoid - # complex cache management. - uses: benchmark-action/github-action-benchmark@a60cea5bc7b49e15c1f58f411161f99e0df48372 # v1.22.0 - with: - name: Docker Image Size - tool: 'customSmallerIsBetter' - output-file-path: output.json - gh-pages-branch: benchmark-data - auto-push: true - benchmark-data-dir-path: dashboard - fail-on-alert: false - github-token: ${{ secrets.GITHUB_TOKEN }} anneal_tests: name: Anneal Tests runs-on: ubuntu-latest - needs: build_docker_env - # External pull requests cannot push the Docker image these jobs pull from - # GHCR. Skip the consumer jobs in that case rather than failing on an - # expected permission denial. - if: github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository + needs: v2_nix_cache permissions: + actions: read # Required to download the toolchain artifact. contents: write # Required to push benchmark data to the storage branch - packages: read # required to pull docker caches from ghcr.io + env: + ANNEAL_TOOLCHAIN_DIR: ${{ github.workspace }}/anneal/target/anneal-toolchain + __ZEROCOPY_LOCAL_DEV: 1 + RUSTFLAGS: "" + RUSTDOCFLAGS: "" + RUST_TEST_THREADS: "1" steps: - name: Record job start time id: job_start_time @@ -254,65 +52,33 @@ jobs: with: persist-credentials: false - - name: Set up Docker Buildx - uses: docker/setup-buildx-action@4d04d5d9486b7bd6fa91e7baf45bbb4f8b9deedd # v4.0.0 - - - name: Log in to the Container registry - uses: docker/login-action@9780b0c442fbb1117ed29e0efdff1e18412f7567 # v3.3.0 + - name: Install stable Rust + uses: dtolnay/rust-toolchain@e97e2d8cc328f1b50210efc529dca0028893a2d9 # zizmor: ignore[superfluous-actions] with: - registry: ghcr.io - username: ${{ github.actor }} - password: ${{ secrets.GITHUB_TOKEN }} - - - name: Generate sanitized Docker tag - id: docker_tag - env: - REF_NAME: ${{ github.ref_name }} - shell: bash - run: | - echo "tag=${REF_NAME//\//-}" >> "$GITHUB_OUTPUT" - - - name: Get UID/GID - id: get_uid - run: | - echo "uid=$(id -u)" >> "$GITHUB_OUTPUT" - echo "gid=$(id -g)" >> "$GITHUB_OUTPUT" + toolchain: stable - - name: Pull and tag image - run: | - start=$(date +%s) - docker pull ghcr.io/google/zerocopy/anneal:${STEPS_DOCKER_TAG_OUTPUTS_TAG} - end=$(date +%s) - duration=$((end - start)) - echo "Docker Pull Time: $duration seconds" - echo "[{\"name\": \"Docker Pull Time\", \"unit\": \"seconds\", \"value\": $duration}]" > pull_time.json - - docker tag ghcr.io/google/zerocopy/anneal:${STEPS_DOCKER_TAG_OUTPUTS_TAG} anneal-ci:local - env: - STEPS_DOCKER_TAG_OUTPUTS_TAG: ${{ steps.docker_tag.outputs.tag }} + - name: Download Anneal toolchain archive + uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 # v7.0.0 + with: + name: anneal-exocrate.tar.zst + path: anneal/v2/target # Ensure `llms-full.txt` file is up-to-date. - name: Check doc generation - run: | - # We intentionally omit the `--rm` flag here. In the GitHub Actions - # environment, Docker's container removal process can take over 5 - # minutes to complete after the tests finish. Since the runner VM is - # destroyed at the end of the job, leaving the container is safe and - # saves time. - docker run -v $GITHUB_WORKSPACE/anneal:/workspace anneal-ci:local cargo run -p doc_gen -- --check + run: cargo run -p doc_gen -- --check + working-directory: anneal + + - name: Install Anneal toolchain archive + run: cargo run setup --local-archive v2/target/anneal-exocrate.tar.zst + working-directory: anneal # Run unit tests separately, as they're much less likely to have bugs # during local development, and this makes the GitHub Actions output # easier to skim (in particular, it's clear at a glance whether a failure # is due to unit or integration tests). - name: Run unit tests - run: | - # We intentionally omit the `--rm` flag here. In the GitHub Actions - # environment, Docker's container removal process can take over 5 - # minutes to complete after the tests finish. Since the runner VM is - # destroyed at the end of the job, leaving the container is safe and - # saves time. - docker run -v $GITHUB_WORKSPACE/anneal:/workspace anneal-ci:local cargo test --verbose --bin cargo-anneal + run: cargo test --verbose --bin cargo-anneal + working-directory: anneal # We duplicate running unit tests since they're very cheap compared to # integration tests, and this way it's easier to be sure that we run all @@ -321,31 +87,25 @@ jobs: - name: Run all tests run: | start=$(date +%s) - # We intentionally omit the `--rm` flag here. In the GitHub Actions - # environment, Docker's container removal process can take over 5 - # minutes to complete after the tests finish. Since the runner VM is - # destroyed at the end of the job, leaving the container is safe and - # saves time. - docker run -v $GITHUB_WORKSPACE/anneal:/workspace anneal-ci:local cargo test --verbose + cargo test --verbose end=$(date +%s) duration=$((end - start)) echo "Test Time: $duration seconds" echo "[{\"name\": \"Test Time\", \"unit\": \"seconds\", \"value\": $duration}]" > test_time.json + working-directory: anneal - name: Combine benchmarks env: JOB_START_TIME_UNIX: ${{ steps.job_start_time.outputs.unix }} run: | - total_duration=$(( $(date +%s) - $JOB_START_TIME_UNIX )) + total_duration=$(( $(date +%s) - JOB_START_TIME_UNIX )) echo "Total CI Duration (All Steps): $total_duration seconds" echo "[{\"name\": \"Total CI Duration (All Steps)\", \"unit\": \"seconds\", \"value\": $total_duration}]" > total_time.json jq -n \ - --slurpfile pull pull_time.json \ - --slurpfile test test_time.json \ + --slurpfile test anneal/test_time.json \ --slurpfile total total_time.json \ '[ - $pull[0][0], $test[0][0], $total[0][0] ]' > output.json @@ -366,14 +126,15 @@ jobs: verify_examples: name: Verify example (${{ matrix.example }}) runs-on: ubuntu-latest - needs: build_docker_env - # External pull requests cannot push the Docker image these jobs pull from - # GHCR. Skip the consumer jobs in that case rather than failing on an - # expected permission denial. - if: github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository + needs: v2_nix_cache permissions: + actions: read # Required to download the toolchain artifact. contents: read - packages: read # required to pull docker caches from ghcr.io + env: + ANNEAL_TOOLCHAIN_DIR: ${{ github.workspace }}/anneal/target/anneal-toolchain + __ZEROCOPY_LOCAL_DEV: 1 + RUSTFLAGS: "" + RUSTDOCFLAGS: "" strategy: fail-fast: false matrix: @@ -402,36 +163,20 @@ jobs: with: persist-credentials: false - - name: Set up Docker Buildx - uses: docker/setup-buildx-action@4d04d5d9486b7bd6fa91e7baf45bbb4f8b9deedd # v4.0.0 - - - name: Log in to the Container registry - uses: docker/login-action@9780b0c442fbb1117ed29e0efdff1e18412f7567 # v3.3.0 + - name: Install stable Rust + uses: dtolnay/rust-toolchain@e97e2d8cc328f1b50210efc529dca0028893a2d9 # zizmor: ignore[superfluous-actions] with: - registry: ghcr.io - username: ${{ github.actor }} - password: ${{ secrets.GITHUB_TOKEN }} - - - name: Generate sanitized Docker tag - id: docker_tag - env: - REF_NAME: ${{ github.ref_name }} - shell: bash - run: | - echo "tag=${REF_NAME//\//-}" >> "$GITHUB_OUTPUT" + toolchain: stable - - name: Get UID/GID - id: get_uid - run: | - echo "uid=$(id -u)" >> "$GITHUB_OUTPUT" - echo "gid=$(id -g)" >> "$GITHUB_OUTPUT" + - name: Download Anneal toolchain archive + uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 # v7.0.0 + with: + name: anneal-exocrate.tar.zst + path: anneal/v2/target - - name: Pull and tag image - run: | - docker pull ghcr.io/google/zerocopy/anneal:${STEPS_DOCKER_TAG_OUTPUTS_TAG} - docker tag ghcr.io/google/zerocopy/anneal:${STEPS_DOCKER_TAG_OUTPUTS_TAG} anneal-ci:local - env: - STEPS_DOCKER_TAG_OUTPUTS_TAG: ${{ steps.docker_tag.outputs.tag }} + - name: Install Anneal toolchain archive + run: cargo run setup --local-archive v2/target/anneal-exocrate.tar.zst + working-directory: anneal - name: Verify example env: @@ -450,12 +195,7 @@ jobs: echo "Verifying $example (expect failure: $expect_failure)" - # We intentionally omit the `--rm` flag here. In the GitHub Actions - # environment, Docker's container removal process can take over 5 - # minutes to complete after the tests finish. Since the runner VM is - # destroyed at the end of the job, leaving the container is safe and - # saves time. - if docker run -v $GITHUB_WORKSPACE/anneal:/workspace -e __ZEROCOPY_LOCAL_DEV=1 anneal-ci:local cargo run verify --unsound-allow-is-valid --example "$example"; then + if cargo run verify --unsound-allow-is-valid --example "$example"; then if [ "$expect_failure" -eq 1 ]; then echo "::error::Example $example succeeded but was expected to fail." exit 1 @@ -470,25 +210,54 @@ jobs: exit 1 fi fi + working-directory: anneal + # Build the Nix-produced toolchain archive once and fan out the exact archive + # as a workflow artifact. This avoids forcing every downstream matrix runner + # to realize the same Nix closure through Magic Nix Cache, which can run into + # GitHub Actions cache throttling under parallel fan-out. v2_nix_cache: - name: Warm Nix Cache for V2 + name: Build Anneal Toolchain Archive runs-on: ubuntu-latest - needs: build_docker_env permissions: contents: read - id-token: write # Required to exchange GitHub OIDC tokens for Determinate Systems Cache API access steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 with: persist-credentials: false + # Restore a local Nix binary cache populated only by trusted `main` + # pushes. Pull requests and merge-queue runs may read the default-branch + # cache, but they never save their own entries there; that keeps sibling + # PRs from publishing toolchain archives for each other. This cache is + # only for cross-run reuse in the builder job. The workflow artifact below + # remains the cross-job fan-out mechanism for the current run. + # + # Keep the key inputs in sync with the local files that influence + # `.#omnibus-archive-ci`. It intentionally excludes most Anneal source + # files so ordinary PRs can reuse the archive built from `main`. + - name: Restore Anneal main Nix binary cache + id: restore_anneal_main_nix_cache + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5 + 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') }} + + # 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 + # `main` or to sibling PRs. Keep this separate from the trusted main cache + # so untrusted PR output cannot publish a shared substituter. + - name: Restore Anneal PR Nix binary cache + id: restore_anneal_pr_nix_cache + if: github.event_name == 'pull_request' + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5 + 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') }} + - name: Install Nix uses: DeterminateSystems/determinate-nix-action@441b9e401ac050c38a07d8313748c5c2d17e8aff # v3.6.1 - - name: Run Magic Nix Cache - uses: DeterminateSystems/magic-nix-cache-action@908b263ff629f4cc17666315b7fd3ec127c6244d # v14 - # On Ubuntu 24.04 (currently `ubuntu-latest`), AppArmor restricts unprivileged user namespaces by default. # The Nix build sandbox runs `steam-run` (which uses `bubblewrap`/`bwrap`) during the `mathlib-cache-download` # phase to create an FHS environment. `bwrap` requires creating a user namespace to set up uid mappings, @@ -501,8 +270,21 @@ jobs: - name: Enable unprivileged user namespaces (Ubuntu 24.04) run: sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0 - - name: Warm Nix Cache - run: nix build .#omnibus-archive + - name: Build Anneal toolchain archive + run: | + set -euo pipefail + mkdir -p target + nix_args=() + for cache in target/nix-cache-main target/nix-cache-pr; do + if [ -f "$cache/nix-cache-info" ]; then + nix_args+=(--extra-substituters "file://$PWD/$cache/?trusted=1") + fi + done + + nix build "${nix_args[@]}" .#omnibus-archive-ci --out-link target/anneal-exocrate.tar.zst + archive="$(readlink -f target/anneal-exocrate.tar.zst)" + rm target/anneal-exocrate.tar.zst + cp "$archive" target/anneal-exocrate.tar.zst working-directory: anneal/v2 # Re-enable the AppArmor namespace restriction to restore the runner host's default security posture. @@ -511,48 +293,75 @@ jobs: if: always() run: sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=1 + # Populate the default-branch cache only from trusted `main` pushes. + # GitHub's dependency-cache scoping makes entries saved from `main` + # visible to PRs targeting `main`, while entries from PR merge refs are + # isolated to that PR. Saving only here keeps the cache useful across PRs + # without letting a PR publish an archive for unrelated runs. + - name: Populate Anneal Nix binary cache + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && steps.restore_anneal_main_nix_cache.outputs.cache-hit != 'true' + run: | + set -euo pipefail + mkdir -p target/nix-cache-main + # The archive is already zstd-compressed, so keep the Nix binary-cache + # wrapper cheap; higher levels add CPU time for negligible size wins. + nix copy .#omnibus-archive-ci \ + --to "file://$PWD/target/nix-cache-main/?compression=zstd&compression-level=1&trusted=1" + working-directory: anneal/v2 + + - name: Save Anneal Nix binary cache + if: github.event_name == 'push' && github.ref == 'refs/heads/main' && steps.restore_anneal_main_nix_cache.outputs.cache-hit != 'true' + uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5 + with: + path: anneal/v2/target/nix-cache-main + key: ${{ steps.restore_anneal_main_nix_cache.outputs.cache-primary-key }} + + - name: Populate Anneal PR Nix binary cache + if: github.event_name == 'pull_request' && steps.restore_anneal_pr_nix_cache.outputs.cache-hit != 'true' + run: | + set -euo pipefail + mkdir -p target/nix-cache-pr + # PR-local caches optimize repeated pushes to the same PR. The + # archive itself uses zstd level 6; keep this wrapper at level 1. + nix copy .#omnibus-archive-ci \ + --to "file://$PWD/target/nix-cache-pr/?compression=zstd&compression-level=1&trusted=1" + working-directory: anneal/v2 + + - name: Save Anneal PR Nix binary cache + if: github.event_name == 'pull_request' && steps.restore_anneal_pr_nix_cache.outputs.cache-hit != 'true' + uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5 + with: + path: anneal/v2/target/nix-cache-pr + key: ${{ steps.restore_anneal_pr_nix_cache.outputs.cache-primary-key }} + + - name: Upload Anneal toolchain archive + uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0 + with: + name: anneal-exocrate.tar.zst + path: anneal/v2/target/anneal-exocrate.tar.zst + if-no-files-found: error + retention-days: 1 + compression-level: 0 + v2: name: Run V2 tests runs-on: ubuntu-latest - # Depending on `v2_nix_cache` avoids duplicate work and ensure `nix build ...` step for this job is fast. - needs: [build_docker_env, v2_nix_cache] + # Depending on `v2_nix_cache` avoids duplicate Nix builds; this job only + # downloads the exact archive that the builder job produced. + needs: v2_nix_cache permissions: + actions: read # Required to download the toolchain artifact. contents: read - id-token: write # Required to exchange GitHub OIDC tokens for Determinate Systems Cache API access steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 with: persist-credentials: false - - name: Install Nix - uses: DeterminateSystems/determinate-nix-action@441b9e401ac050c38a07d8313748c5c2d17e8aff # v3.6.1 - - - name: Run Magic Nix Cache - uses: DeterminateSystems/magic-nix-cache-action@908b263ff629f4cc17666315b7fd3ec127c6244d # v14 - - # On Ubuntu 24.04 (currently `ubuntu-latest`), AppArmor restricts unprivileged user namespaces by default. - # The Nix build sandbox runs `steam-run` (which uses `bubblewrap`/`bwrap`) during the `mathlib-cache-download` - # phase to create an FHS environment. `bwrap` requires creating a user namespace to set up uid mappings, - # which fails with "Permission denied" unless this restriction is temporarily disabled on the host. - # - # We temporarily disable it right before the `nix build` step and re-enable it immediately after - # to maintain the principle of least privilege. - # - # FIXME(#3412): Deduplicate this with what's repeated above? - - name: Enable unprivileged user namespaces (Ubuntu 24.04) - run: sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0 - - - name: Build outside-cargo dependencies (cached) - run: | - mkdir -p target - nix build .#omnibus-archive --out-link target/anneal-exocrate.tar.zst - working-directory: anneal/v2 - - # Re-enable the AppArmor namespace restriction to restore the runner host's default security posture. - # `if: always()` ensures this cleanup step runs even if the Nix build fails. - - name: Restore AppArmor restriction - if: always() - run: sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=1 + - name: Download Anneal toolchain archive + uses: actions/download-artifact@37930b1c2abaa49bbe596cd826c3c89aef350131 # v7.0.0 + with: + name: anneal-exocrate.tar.zst + path: anneal/v2/target # FIXME: Pin this nightly to the same Rust date encoded in # anneal/v2/flake.nix, or derive it from the archive metadata, so v2 CI is @@ -579,7 +388,7 @@ jobs: # https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/collaborating-on-repositories-with-code-quality-features/troubleshooting-required-status-checks#handling-skipped-but-required-checks if: failure() runs-on: ubuntu-latest - needs: [build_docker_env, anneal_tests, verify_examples, measure_image_size, v2_nix_cache, v2] + needs: [anneal_tests, verify_examples, v2_nix_cache, v2] steps: - name: Mark the job as failed run: exit 1 diff --git a/anneal/Cargo.lock b/anneal/Cargo.lock index 511519e2d7..bde098220d 100644 --- a/anneal/Cargo.lock +++ b/anneal/Cargo.lock @@ -107,12 +107,6 @@ dependencies = [ "wait-timeout", ] -[[package]] -name = "atomic-waker" -version = "1.1.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1505bd5d3d116872e7271a6d4e16d81d0c8570876c8de68093a09ac269d8aac0" - [[package]] name = "autocfg" version = "1.5.0" @@ -223,9 +217,8 @@ dependencies = [ "console", "dashmap", "datatest-stable", - "dirs", "env_logger", - "flate2", + "exocrate", "fs2", "indicatif", "log", @@ -235,14 +228,12 @@ dependencies = [ "quote", "rayon", "regex", - "reqwest", "serde", "serde_json", "sha2", "similar", "strip-ansi-escapes", "syn", - "tar", "tempfile", "thiserror 2.0.18", "toml", @@ -304,6 +295,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b7a4d3ec6524d28a329fc53654bbadc9bdd7b0431f5d65f1a56ffb28a1ee5283" dependencies = [ "find-msvc-tools", + "jobserver", + "libc", "shlex", ] @@ -313,12 +306,6 @@ version = "1.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" -[[package]] -name = "cfg_aliases" -version = "0.2.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "613afe47fcd5fac7ccf1db93babcb082c5994d996f20b8b159f2ad1658eb5724" - [[package]] name = "clap" version = "4.6.0" @@ -411,7 +398,7 @@ version = "3.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "faf9468729b8cbcea668e36183cb69d317348c2e08e994829fb56ebfdfbaac34" dependencies = [ - "windows-sys 0.61.2", + "windows-sys 0.52.0", ] [[package]] @@ -432,32 +419,6 @@ dependencies = [ "windows-sys 0.61.2", ] -[[package]] -name = "core-foundation" -version = "0.9.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "91e195e091a93c46f7102ec7818a2aa394e1e1771c3ab4825963fa03e45afb8f" -dependencies = [ - "core-foundation-sys", - "libc", -] - -[[package]] -name = "core-foundation" -version = "0.10.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b2a6cd9ae233e7f62ba4e9353e81a88df7fc8a5987b8d445b4d90c879bd156f6" -dependencies = [ - "core-foundation-sys", - "libc", -] - -[[package]] -name = "core-foundation-sys" -version = "0.8.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "773648b94d0e5d620f64f280777445740e61fe701025087ec8b57f45c791888b" - [[package]] name = "cpufeatures" version = "0.2.17" @@ -583,17 +544,6 @@ dependencies = [ "windows-sys 0.61.2", ] -[[package]] -name = "displaydoc" -version = "0.2.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "97369cbbc041bc366949bc74d34658d6cda5621039731c6310521892a3a20ae0" -dependencies = [ - "proc-macro2", - "quote", - "syn", -] - [[package]] name = "doc_gen" version = "0.1.0" @@ -614,15 +564,6 @@ version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "34aa73646ffb006b8f5147f3dc182bd4bcb190227ce861fc4a4844bf8e3cb2c0" -[[package]] -name = "encoding_rs" -version = "0.8.35" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "75030f3c4f45dafd7586dd6780965a8c7e8e285a5ecb86713e63a79c5b2766f3" -dependencies = [ - "cfg-if", -] - [[package]] name = "env_filter" version = "1.0.1" @@ -659,7 +600,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb" dependencies = [ "libc", - "windows-sys 0.61.2", + "windows-sys 0.52.0", ] [[package]] @@ -668,6 +609,21 @@ version = "0.5.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5692dd7b5a1978a5aeb0ce83b7655c58ca8efdcb79d21036ea249da95afec2c6" +[[package]] +name = "exocrate" +version = "0.1.0" +dependencies = [ + "dirs", + "fs2", + "log", + "sha2", + "sha2-const", + "tar", + "tempfile", + "ureq", + "zstd", +] + [[package]] name = "eyre" version = "0.6.12" @@ -731,42 +687,12 @@ dependencies = [ "num-traits", ] -[[package]] -name = "fnv" -version = "1.0.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1" - [[package]] name = "foldhash" version = "0.1.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d9c4f5dac5e15c24eb999c26181a6ca40b39fe946cbe4c263c7209467bc83af2" -[[package]] -name = "foreign-types" -version = "0.3.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f6f339eb8adc052cd2ca78910fda869aefa38d22d5cb648e6485e4d3fc06f3b1" -dependencies = [ - "foreign-types-shared", -] - -[[package]] -name = "foreign-types-shared" -version = "0.1.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "00b0228411908ca8685dba7fc2cdd70ec9990a6e753e89b6ac91a84c40fbaf4b" - -[[package]] -name = "form_urlencoded" -version = "1.2.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cb4cb245038516f5f85277875cdaa4f7d2c9a0fa0468de06ed190163b1581fcf" -dependencies = [ - "percent-encoding", -] - [[package]] name = "fs2" version = "0.4.3" @@ -777,55 +703,6 @@ dependencies = [ "winapi", ] -[[package]] -name = "futures-channel" -version = "0.3.32" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "07bbe89c50d7a535e539b8c17bc0b49bdb77747034daa8087407d655f3f7cc1d" -dependencies = [ - "futures-core", - "futures-sink", -] - -[[package]] -name = "futures-core" -version = "0.3.32" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7e3450815272ef58cec6d564423f6e755e25379b217b0bc688e295ba24df6b1d" - -[[package]] -name = "futures-io" -version = "0.3.32" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cecba35d7ad927e23624b22ad55235f2239cfa44fd10428eecbeba6d6a717718" - -[[package]] -name = "futures-sink" -version = "0.3.32" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c39754e157331b013978ec91992bde1ac089843443c49cbc7f46150b0fad0893" - -[[package]] -name = "futures-task" -version = "0.3.32" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "037711b3d59c33004d3856fbdc83b99d4ff37a24768fa1be9ce3538a1cde4393" - -[[package]] -name = "futures-util" -version = "0.3.32" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "389ca41296e6190b48053de0321d02a77f32f8a5d2461dd38762c0593805c6d6" -dependencies = [ - "futures-core", - "futures-io", - "futures-sink", - "futures-task", - "memchr", - "pin-project-lite", - "slab", -] - [[package]] name = "generic-array" version = "0.14.7" @@ -843,10 +720,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ff2abc00be7fca6ebc474524697ae276ad847ad0a6b3faa4bcb027e9a4614ad0" dependencies = [ "cfg-if", - "js-sys", "libc", "wasi", - "wasm-bindgen", ] [[package]] @@ -856,11 +731,9 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "899def5c37c4fd7b2664648c28120ecec138e4d395b459e5ca34f9cce2dd77fd" dependencies = [ "cfg-if", - "js-sys", "libc", "r-efi 5.3.0", "wasip2", - "wasm-bindgen", ] [[package]] @@ -882,25 +755,6 @@ version = "0.32.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e629b9b98ef3dd8afe6ca2bd0f89306cec16d43d907889945bc5d6687f2f13c7" -[[package]] -name = "h2" -version = "0.4.13" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2f44da3a8150a6703ed5d34e164b875fd14c2cdab9af1252a9a1020bde2bdc54" -dependencies = [ - "atomic-waker", - "bytes", - "fnv", - "futures-core", - "futures-sink", - "http", - "indexmap", - "slab", - "tokio", - "tokio-util", - "tracing", -] - [[package]] name = "hashbrown" version = "0.14.5" @@ -938,223 +792,18 @@ dependencies = [ "itoa", ] -[[package]] -name = "http-body" -version = "1.0.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1efedce1fb8e6913f23e0c92de8e62cd5b772a67e7b3946df930a62566c93184" -dependencies = [ - "bytes", - "http", -] - -[[package]] -name = "http-body-util" -version = "0.1.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b021d93e26becf5dc7e1b75b1bed1fd93124b374ceb73f43d4d4eafec896a64a" -dependencies = [ - "bytes", - "futures-core", - "http", - "http-body", - "pin-project-lite", -] - [[package]] name = "httparse" version = "1.10.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6dbf3de79e51f3d586ab4cb9d5c3e2c14aa28ed23d180cf89b4df0454a69cc87" -[[package]] -name = "hyper" -version = "1.9.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6299f016b246a94207e63da54dbe807655bf9e00044f73ded42c3ac5305fbcca" -dependencies = [ - "atomic-waker", - "bytes", - "futures-channel", - "futures-core", - "h2", - "http", - "http-body", - "httparse", - "itoa", - "pin-project-lite", - "smallvec", - "tokio", - "want", -] - -[[package]] -name = "hyper-rustls" -version = "0.27.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e3c93eb611681b207e1fe55d5a71ecf91572ec8a6705cdb6857f7d8d5242cf58" -dependencies = [ - "http", - "hyper", - "hyper-util", - "rustls", - "rustls-pki-types", - "tokio", - "tokio-rustls", - "tower-service", - "webpki-roots", -] - -[[package]] -name = "hyper-tls" -version = "0.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "70206fc6890eaca9fde8a0bf71caa2ddfc9fe045ac9e5c70df101a7dbde866e0" -dependencies = [ - "bytes", - "http-body-util", - "hyper", - "hyper-util", - "native-tls", - "tokio", - "tokio-native-tls", - "tower-service", -] - -[[package]] -name = "hyper-util" -version = "0.1.20" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "96547c2556ec9d12fb1578c4eaf448b04993e7fb79cbaad930a656880a6bdfa0" -dependencies = [ - "base64", - "bytes", - "futures-channel", - "futures-util", - "http", - "http-body", - "hyper", - "ipnet", - "libc", - "percent-encoding", - "pin-project-lite", - "socket2", - "system-configuration", - "tokio", - "tower-service", - "tracing", - "windows-registry", -] - -[[package]] -name = "icu_collections" -version = "2.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2984d1cd16c883d7935b9e07e44071dca8d917fd52ecc02c04d5fa0b5a3f191c" -dependencies = [ - "displaydoc", - "potential_utf", - "utf8_iter", - "yoke", - "zerofrom", - "zerovec", -] - -[[package]] -name = "icu_locale_core" -version = "2.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "92219b62b3e2b4d88ac5119f8904c10f8f61bf7e95b640d25ba3075e6cac2c29" -dependencies = [ - "displaydoc", - "litemap", - "tinystr", - "writeable", - "zerovec", -] - -[[package]] -name = "icu_normalizer" -version = "2.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c56e5ee99d6e3d33bd91c5d85458b6005a22140021cc324cea84dd0e72cff3b4" -dependencies = [ - "icu_collections", - "icu_normalizer_data", - "icu_properties", - "icu_provider", - "smallvec", - "zerovec", -] - -[[package]] -name = "icu_normalizer_data" -version = "2.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "da3be0ae77ea334f4da67c12f149704f19f81d1adf7c51cf482943e84a2bad38" - -[[package]] -name = "icu_properties" -version = "2.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bee3b67d0ea5c2cca5003417989af8996f8604e34fb9ddf96208a033901e70de" -dependencies = [ - "icu_collections", - "icu_locale_core", - "icu_properties_data", - "icu_provider", - "zerotrie", - "zerovec", -] - -[[package]] -name = "icu_properties_data" -version = "2.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e2bbb201e0c04f7b4b3e14382af113e17ba4f63e2c9d2ee626b720cbce54a14" - -[[package]] -name = "icu_provider" -version = "2.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "139c4cf31c8b5f33d7e199446eff9c1e02decfc2f0eec2c8d71f65befa45b421" -dependencies = [ - "displaydoc", - "icu_locale_core", - "writeable", - "yoke", - "zerofrom", - "zerotrie", - "zerovec", -] - [[package]] name = "id-arena" version = "2.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3d3067d79b975e8844ca9eb072e16b31c3c1c36928edf9c6789548c524d0d954" -[[package]] -name = "idna" -version = "1.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3b0875f23caa03898994f6ddc501886a45c7d3d62d04d2d90788d47be1b1e4de" -dependencies = [ - "idna_adapter", - "smallvec", - "utf8_iter", -] - -[[package]] -name = "idna_adapter" -version = "1.2.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3acae9609540aa318d1bc588455225fb2085b9ed0c4f6bd0d9d5bcd86f1a0344" -dependencies = [ - "icu_normalizer", - "icu_properties", -] - [[package]] name = "indenter" version = "0.3.4" @@ -1187,22 +836,6 @@ dependencies = [ "web-time", ] -[[package]] -name = "ipnet" -version = "2.12.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d98f6fed1fde3f8c21bc40a1abb88dd75e67924f9cffc3ef95607bad8017f8e2" - -[[package]] -name = "iri-string" -version = "0.7.12" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "25e659a4bb38e810ebc252e53b5814ff908a8c58c2a9ce2fae1bbec24cbf4e20" -dependencies = [ - "memchr", - "serde", -] - [[package]] name = "is_ci" version = "1.2.0" @@ -1245,14 +878,22 @@ dependencies = [ "syn", ] +[[package]] +name = "jobserver" +version = "0.1.34" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9afb3de4395d6b3e67a780b6de64b51c978ecf11cb9a462c66be7d4ca9039d33" +dependencies = [ + "getrandom 0.3.4", + "libc", +] + [[package]] name = "js-sys" version = "0.3.94" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2e04e2ef80ce82e13552136fabeef8a5ed1f985a96805761cbb9a2c34e7664d9" dependencies = [ - "cfg-if", - "futures-util", "once_cell", "wasm-bindgen", ] @@ -1311,12 +952,6 @@ version = "0.12.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "32a66949e030da00e8c7d4434b251670a91556f4144941d37452769c25d58a53" -[[package]] -name = "litemap" -version = "0.8.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "92daf443525c4cce67b150400bc2316076100ce0b3686209eb8cf3c31612e6f0" - [[package]] name = "lock_api" version = "0.4.14" @@ -1332,12 +967,6 @@ version = "0.4.29" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5e5032e24019045c762d3c0f28f5b6b8bbf38563a65908389bf7978758920897" -[[package]] -name = "lru-slab" -version = "0.1.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "112b39cec0b298b6c1999fee3e31427f74f676e4cb9879ed1a121b43661a4154" - [[package]] name = "memchr" version = "2.8.0" @@ -1374,12 +1003,6 @@ dependencies = [ "syn", ] -[[package]] -name = "mime" -version = "0.3.17" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6877bb514081ee2a7ff5ef9de3281f14a4dd4bceac4c09388074a6b5df8a139a" - [[package]] name = "miniz_oxide" version = "0.8.9" @@ -1390,34 +1013,6 @@ dependencies = [ "simd-adler32", ] -[[package]] -name = "mio" -version = "1.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "50b7e5b27aa02a74bac8c3f23f448f8d87ff11f92d3aac1a6ed369ee08cc56c1" -dependencies = [ - "libc", - "wasi", - "windows-sys 0.61.2", -] - -[[package]] -name = "native-tls" -version = "0.2.18" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "465500e14ea162429d264d44189adc38b199b62b1c21eea9f69e4b73cb03bbf2" -dependencies = [ - "libc", - "log", - "openssl", - "openssl-probe", - "openssl-sys", - "schannel", - "security-framework", - "security-framework-sys", - "tempfile", -] - [[package]] name = "normalize-line-endings" version = "0.3.0" @@ -1454,49 +1049,6 @@ version = "1.70.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "384b8ab6d37215f3c5301a95a4accb5d64aa607f1fcb26a11b5303878451b4fe" -[[package]] -name = "openssl" -version = "0.10.80" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a45fa2aa886c42762255da344f0a0d313e254066c46aad76f300c3d3da62d967" -dependencies = [ - "bitflags", - "cfg-if", - "foreign-types", - "libc", - "openssl-macros", - "openssl-sys", -] - -[[package]] -name = "openssl-macros" -version = "0.1.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a948666b637a0f465e8564c73e89d4dde00d72d4d473cc972f390fc3dcee7d9c" -dependencies = [ - "proc-macro2", - "quote", - "syn", -] - -[[package]] -name = "openssl-probe" -version = "0.2.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7c87def4c32ab89d880effc9e097653c8da5d6ef28e6b539d313baaacfbafcbe" - -[[package]] -name = "openssl-sys" -version = "0.9.116" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f28a22dc7140cda5f096e5e7724a6962ca81a7f8bfd2979f9b18c11af56318c4" -dependencies = [ - "cc", - "libc", - "pkg-config", - "vcpkg", -] - [[package]] name = "option-ext" version = "0.2.0" @@ -1561,24 +1113,6 @@ dependencies = [ "portable-atomic", ] -[[package]] -name = "potential_utf" -version = "0.1.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0103b1cef7ec0cf76490e969665504990193874ea05c85ff9bab8b911d0a0564" -dependencies = [ - "zerovec", -] - -[[package]] -name = "ppv-lite86" -version = "0.2.21" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "85eae3c4ed2f50dcfe72643da4befc30deadb458a9b590d720cde2f2b1e97da9" -dependencies = [ - "zerocopy", -] - [[package]] name = "predicates" version = "3.1.4" @@ -1637,61 +1171,6 @@ dependencies = [ "unicode-ident", ] -[[package]] -name = "quinn" -version = "0.11.9" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b9e20a958963c291dc322d98411f541009df2ced7b5a4f2bd52337638cfccf20" -dependencies = [ - "bytes", - "cfg_aliases", - "pin-project-lite", - "quinn-proto", - "quinn-udp", - "rustc-hash", - "rustls", - "socket2", - "thiserror 2.0.18", - "tokio", - "tracing", - "web-time", -] - -[[package]] -name = "quinn-proto" -version = "0.11.14" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "434b42fec591c96ef50e21e886936e66d3cc3f737104fdb9b737c40ffb94c098" -dependencies = [ - "bytes", - "getrandom 0.3.4", - "lru-slab", - "rand", - "ring", - "rustc-hash", - "rustls", - "rustls-pki-types", - "slab", - "thiserror 2.0.18", - "tinyvec", - "tracing", - "web-time", -] - -[[package]] -name = "quinn-udp" -version = "0.5.14" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "addec6a0dcad8a8d96a771f815f0eaf55f9d1805756410b39f5fa81332574cbd" -dependencies = [ - "cfg_aliases", - "libc", - "once_cell", - "socket2", - "tracing", - "windows-sys 0.60.2", -] - [[package]] name = "quote" version = "1.0.45" @@ -1713,35 +1192,6 @@ version = "6.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f8dcc9c7d52a811697d2151c701e0d08956f92b0e24136cf4cf27b57a6a0d9bf" -[[package]] -name = "rand" -version = "0.9.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "44c5af06bb1b7d3216d91932aed5265164bf384dc89cd6ba05cf59a35f5f76ea" -dependencies = [ - "rand_chacha", - "rand_core", -] - -[[package]] -name = "rand_chacha" -version = "0.9.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d3022b5f1df60f26e1ffddd6c66e8aa15de382ae63b3a0c1bfc0e4d3e3f325cb" -dependencies = [ - "ppv-lite86", - "rand_core", -] - -[[package]] -name = "rand_core" -version = "0.9.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "76afc826de14238e6e8c374ddcc1fa19e374fd8dd986b0d2af0d02377261d83c" -dependencies = [ - "getrandom 0.3.4", -] - [[package]] name = "rayon" version = "1.11.0" @@ -1820,52 +1270,6 @@ version = "0.8.10" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "dc897dd8d9e8bd1ed8cdad82b5966c3e0ecae09fb1907d58efaa013543185d0a" -[[package]] -name = "reqwest" -version = "0.12.28" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eddd3ca559203180a307f12d114c268abf583f59b03cb906fd0b3ff8646c1147" -dependencies = [ - "base64", - "bytes", - "encoding_rs", - "futures-channel", - "futures-core", - "futures-util", - "h2", - "http", - "http-body", - "http-body-util", - "hyper", - "hyper-rustls", - "hyper-tls", - "hyper-util", - "js-sys", - "log", - "mime", - "native-tls", - "percent-encoding", - "pin-project-lite", - "quinn", - "rustls", - "rustls-pki-types", - "serde", - "serde_json", - "serde_urlencoded", - "sync_wrapper", - "tokio", - "tokio-native-tls", - "tokio-rustls", - "tower", - "tower-http", - "tower-service", - "url", - "wasm-bindgen", - "wasm-bindgen-futures", - "web-sys", - "webpki-roots", -] - [[package]] name = "ring" version = "0.17.14" @@ -1886,12 +1290,6 @@ version = "0.1.27" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b50b8869d9fc858ce7266cce0194bd74df58b9d0e3f6df3a9fc8eb470d95c09d" -[[package]] -name = "rustc-hash" -version = "2.1.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "94300abf3f1ae2e2b8ffb7b58043de3d399c73fa6f4b73826402a5c457614dbe" - [[package]] name = "rustc_version" version = "0.4.1" @@ -1923,7 +1321,7 @@ dependencies = [ "errno", "libc", "linux-raw-sys", - "windows-sys 0.61.2", + "windows-sys 0.52.0", ] [[package]] @@ -1932,6 +1330,7 @@ version = "0.23.37" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "758025cb5fccfd3bc2fd74708fd4682be41d99e5dff73c377c0646c6012c73a4" dependencies = [ + "log", "once_cell", "ring", "rustls-pki-types", @@ -1946,7 +1345,6 @@ version = "1.14.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "be040f8b0a225e40375822a563fa9524378b9d63112f53e19ffff34df5d33fdd" dependencies = [ - "web-time", "zeroize", ] @@ -1967,12 +1365,6 @@ version = "1.0.22" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b39cdef0fa800fc44525c84ccb54a029961a8215f9619753635a9c0d2538d46d" -[[package]] -name = "ryu" -version = "1.0.23" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9774ba4a74de5f7b1c1451ed6cd5285a32eddb5cccb8cc655a4e50009e06477f" - [[package]] name = "same-file" version = "1.0.6" @@ -1982,44 +1374,12 @@ dependencies = [ "winapi-util", ] -[[package]] -name = "schannel" -version = "0.1.29" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "91c1b7e4904c873ef0710c1f407dde2e6287de2bebc1bbbf7d430bb7cbffd939" -dependencies = [ - "windows-sys 0.61.2", -] - [[package]] name = "scopeguard" version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" -[[package]] -name = "security-framework" -version = "3.7.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b7f4bc775c73d9a02cde8bf7b2ec4c9d12743edf609006c7facc23998404cd1d" -dependencies = [ - "bitflags", - "core-foundation 0.10.1", - "core-foundation-sys", - "libc", - "security-framework-sys", -] - -[[package]] -name = "security-framework-sys" -version = "2.17.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6ce2691df843ecc5d231c0b14ece2acc3efb62c0a398c7e1d875f3983ce020e3" -dependencies = [ - "core-foundation-sys", - "libc", -] - [[package]] name = "semver" version = "1.0.27" @@ -2083,18 +1443,6 @@ dependencies = [ "serde", ] -[[package]] -name = "serde_urlencoded" -version = "0.7.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d3491c14715ca2294c4d6a88f15e84739788c1d030eed8c110436aafdaa2f3fd" -dependencies = [ - "form_urlencoded", - "itoa", - "ryu", - "serde", -] - [[package]] name = "sha2" version = "0.10.9" @@ -2106,6 +1454,12 @@ dependencies = [ "digest", ] +[[package]] +name = "sha2-const" +version = "0.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dbb83f144cbda94be5d2278400eee9e0a03eb68b5504349943655b7b1603c4af" + [[package]] name = "sharded-slab" version = "0.1.7" @@ -2133,28 +1487,12 @@ version = "2.7.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bbbb5d9659141646ae647b42fe094daf6c6192d1620870b449d9557f748b2daa" -[[package]] -name = "slab" -version = "0.4.12" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0c790de23124f9ab44544d7ac05d60440adc586479ce501c1d6d7da3cd8c9cf5" - [[package]] name = "smallvec" version = "1.15.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "67b1b7a3b5fe4f1376887184045fcf45c69e92af734b7aaddc05fb777b6fbd03" -[[package]] -name = "socket2" -version = "0.6.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3a766e1110788c36f4fa1c2b71b387a7815aa65f88ce0229841826633d93723e" -dependencies = [ - "libc", - "windows-sys 0.61.2", -] - [[package]] name = "spanned" version = "0.4.1" @@ -2166,12 +1504,6 @@ dependencies = [ "color-eyre", ] -[[package]] -name = "stable_deref_trait" -version = "1.2.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6ce2be8dc25455e1f91df71bfa12ad37d7af1092ae736f3a6cd0e37bc7810596" - [[package]] name = "streaming-iterator" version = "0.1.9" @@ -2231,47 +1563,6 @@ dependencies = [ "unicode-ident", ] -[[package]] -name = "sync_wrapper" -version = "1.0.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0bf256ce5efdfa370213c1dabab5935a12e49f2c58d15e9eac2870d3b4f27263" -dependencies = [ - "futures-core", -] - -[[package]] -name = "synstructure" -version = "0.13.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "728a70f3dbaf5bab7f0c4b1ac8d7ae5ea60a4b5549c8a5914361c99147a709d2" -dependencies = [ - "proc-macro2", - "quote", - "syn", -] - -[[package]] -name = "system-configuration" -version = "0.7.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a13f3d0daba03132c0aa9767f98351b3488edc2c100cda2d2ec2b04f3d8d3c8b" -dependencies = [ - "bitflags", - "core-foundation 0.9.4", - "system-configuration-sys", -] - -[[package]] -name = "system-configuration-sys" -version = "0.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e1d1b10ced5ca923a1fcb8d03e96b8d3268065d724548c0211415ff6ac6bac4" -dependencies = [ - "core-foundation-sys", - "libc", -] - [[package]] name = "tar" version = "0.4.46" @@ -2293,7 +1584,7 @@ dependencies = [ "getrandom 0.4.2", "once_cell", "rustix", - "windows-sys 0.61.2", + "windows-sys 0.52.0", ] [[package]] @@ -2371,78 +1662,6 @@ dependencies = [ "cfg-if", ] -[[package]] -name = "tinystr" -version = "0.8.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c8323304221c2a851516f22236c5722a72eaa19749016521d6dff0824447d96d" -dependencies = [ - "displaydoc", - "zerovec", -] - -[[package]] -name = "tinyvec" -version = "1.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3e61e67053d25a4e82c844e8424039d9745781b3fc4f32b8d55ed50f5f667ef3" -dependencies = [ - "tinyvec_macros", -] - -[[package]] -name = "tinyvec_macros" -version = "0.1.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1f3ccbac311fea05f86f61904b462b55fb3df8837a366dfc601a0161d0532f20" - -[[package]] -name = "tokio" -version = "1.51.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2bd1c4c0fc4a7ab90fc15ef6daaa3ec3b893f004f915f2392557ed23237820cd" -dependencies = [ - "bytes", - "libc", - "mio", - "pin-project-lite", - "socket2", - "windows-sys 0.61.2", -] - -[[package]] -name = "tokio-native-tls" -version = "0.3.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bbae76ab933c85776efabc971569dd6119c580d8f5d448769dec1764bf796ef2" -dependencies = [ - "native-tls", - "tokio", -] - -[[package]] -name = "tokio-rustls" -version = "0.26.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1729aa945f29d91ba541258c8df89027d5792d85a8841fb65e8bf0f4ede4ef61" -dependencies = [ - "rustls", - "tokio", -] - -[[package]] -name = "tokio-util" -version = "0.7.18" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9ae9cec805b01e8fc3fd2fe289f89149a9b66dd16786abd8b19cfa7b48cb0098" -dependencies = [ - "bytes", - "futures-core", - "futures-sink", - "pin-project-lite", - "tokio", -] - [[package]] name = "toml" version = "0.8.23" @@ -2484,51 +1703,6 @@ version = "0.1.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5d99f8c9a7727884afe522e9bd5edbfc91a3312b36a77b5fb8926e4c31a41801" -[[package]] -name = "tower" -version = "0.5.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ebe5ef63511595f1344e2d5cfa636d973292adc0eec1f0ad45fae9f0851ab1d4" -dependencies = [ - "futures-core", - "futures-util", - "pin-project-lite", - "sync_wrapper", - "tokio", - "tower-layer", - "tower-service", -] - -[[package]] -name = "tower-http" -version = "0.6.8" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d4e6559d53cc268e5031cd8429d05415bc4cb4aefc4aa5d6cc35fbf5b924a1f8" -dependencies = [ - "bitflags", - "bytes", - "futures-util", - "http", - "http-body", - "iri-string", - "pin-project-lite", - "tower", - "tower-layer", - "tower-service", -] - -[[package]] -name = "tower-layer" -version = "0.3.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "121c2a6cda46980bb0fcd1647ffaf6cd3fc79a013de288782836f6df9c48780e" - -[[package]] -name = "tower-service" -version = "0.3.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8df9b6e13f2d32c91b9bd719c00d1958837bc7dec474d94952798cc8e69eeec3" - [[package]] name = "tracing" version = "0.1.44" @@ -2600,12 +1774,6 @@ dependencies = [ "tree-sitter", ] -[[package]] -name = "try-lock" -version = "0.2.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e421abadd41a4225275504ea4d6566923418b7f05506fbc9c0fe86ba7396114b" - [[package]] name = "typenum" version = "1.19.0" @@ -2687,22 +1855,39 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8ecb6da28b8a351d773b68d5825ac39017e680750f980f3a1a85cd8dd28a47c1" [[package]] -name = "url" -version = "2.5.8" +name = "ureq" +version = "3.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ff67a8a4397373c3ef660812acab3268222035010ab8680ec4215f38ba3d0eed" +checksum = "dea7109cdcd5864d4eeb1b58a1648dc9bf520360d7af16ec26d0a9354bafcfc0" dependencies = [ - "form_urlencoded", - "idna", + "base64", + "flate2", + "log", "percent-encoding", - "serde", + "rustls", + "rustls-pki-types", + "ureq-proto", + "utf8-zero", + "webpki-roots", ] [[package]] -name = "utf8_iter" -version = "1.0.4" +name = "ureq-proto" +version = "0.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e994ba84b0bd1b1b0cf92878b7ef898a5c1760108fe7b6010327e274917a808c" +dependencies = [ + "base64", + "http", + "httparse", + "log", +] + +[[package]] +name = "utf8-zero" +version = "0.8.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b6c140620e7ffbb22c2dee59cafe6084a59b5ffc27a8859a5f0d494b5d52b6be" +checksum = "b8c0a043c9540bae7c578c88f91dda8bd82e59ae27c21baca69c8b191aaf5a6e" [[package]] name = "utf8parse" @@ -2716,12 +1901,6 @@ version = "0.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ba73ea9cf16a25df0c8caa16c51acb937d5712a8429db78a3ee29d5dcacd3a65" -[[package]] -name = "vcpkg" -version = "0.2.15" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "accd4ea62f7bb7a82fe23066fb0957d48ef677f6eeb8215f372f52e48bb32426" - [[package]] name = "version_check" version = "0.9.5" @@ -2756,15 +1935,6 @@ dependencies = [ "winapi-util", ] -[[package]] -name = "want" -version = "0.3.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bfa7760aed19e106de2c7c0b581b509f2f25d3dacaf737cb82ac61bc6d760b0e" -dependencies = [ - "try-lock", -] - [[package]] name = "wasi" version = "0.11.1+wasi-snapshot-preview1" @@ -2802,16 +1972,6 @@ dependencies = [ "wasm-bindgen-shared", ] -[[package]] -name = "wasm-bindgen-futures" -version = "0.4.67" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "03623de6905b7206edd0a75f69f747f134b7f0a2323392d664448bf2d3c5d87e" -dependencies = [ - "js-sys", - "wasm-bindgen", -] - [[package]] name = "wasm-bindgen-macro" version = "0.2.117" @@ -2878,16 +2038,6 @@ dependencies = [ "semver", ] -[[package]] -name = "web-sys" -version = "0.3.94" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cd70027e39b12f0849461e08ffc50b9cd7688d942c1c8e3c7b22273236b4dd0a" -dependencies = [ - "js-sys", - "wasm-bindgen", -] - [[package]] name = "web-time" version = "1.1.0" @@ -2929,7 +2079,7 @@ version = "0.1.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c2a7b1c03c876122aa43f3020e6c3c3ee5c05081c9a00739faf7503aeba10d22" dependencies = [ - "windows-sys 0.61.2", + "windows-sys 0.52.0", ] [[package]] @@ -2944,51 +2094,13 @@ version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5" -[[package]] -name = "windows-registry" -version = "0.6.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "02752bf7fbdcce7f2a27a742f798510f3e5ad88dbe84871e5168e2120c3d5720" -dependencies = [ - "windows-link", - "windows-result", - "windows-strings", -] - -[[package]] -name = "windows-result" -version = "0.4.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7781fa89eaf60850ac3d2da7af8e5242a5ea78d1a11c49bf2910bb5a73853eb5" -dependencies = [ - "windows-link", -] - -[[package]] -name = "windows-strings" -version = "0.5.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7837d08f69c77cf6b07689544538e017c1bfcf57e34b4c0ff58e6c2cd3b37091" -dependencies = [ - "windows-link", -] - [[package]] name = "windows-sys" version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" dependencies = [ - "windows-targets 0.52.6", -] - -[[package]] -name = "windows-sys" -version = "0.60.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f2f500e4d28234f72040990ec9d39e3a6b950f9f22d3dba18416c35882612bcb" -dependencies = [ - "windows-targets 0.53.5", + "windows-targets", ] [[package]] @@ -3006,31 +2118,14 @@ version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" dependencies = [ - "windows_aarch64_gnullvm 0.52.6", - "windows_aarch64_msvc 0.52.6", - "windows_i686_gnu 0.52.6", - "windows_i686_gnullvm 0.52.6", - "windows_i686_msvc 0.52.6", - "windows_x86_64_gnu 0.52.6", - "windows_x86_64_gnullvm 0.52.6", - "windows_x86_64_msvc 0.52.6", -] - -[[package]] -name = "windows-targets" -version = "0.53.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4945f9f551b88e0d65f3db0bc25c33b8acea4d9e41163edf90dcd0b19f9069f3" -dependencies = [ - "windows-link", - "windows_aarch64_gnullvm 0.53.1", - "windows_aarch64_msvc 0.53.1", - "windows_i686_gnu 0.53.1", - "windows_i686_gnullvm 0.53.1", - "windows_i686_msvc 0.53.1", - "windows_x86_64_gnu 0.53.1", - "windows_x86_64_gnullvm 0.53.1", - "windows_x86_64_msvc 0.53.1", + "windows_aarch64_gnullvm", + "windows_aarch64_msvc", + "windows_i686_gnu", + "windows_i686_gnullvm", + "windows_i686_msvc", + "windows_x86_64_gnu", + "windows_x86_64_gnullvm", + "windows_x86_64_msvc", ] [[package]] @@ -3039,96 +2134,48 @@ version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" -[[package]] -name = "windows_aarch64_gnullvm" -version = "0.53.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a9d8416fa8b42f5c947f8482c43e7d89e73a173cead56d044f6a56104a6d1b53" - [[package]] name = "windows_aarch64_msvc" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" -[[package]] -name = "windows_aarch64_msvc" -version = "0.53.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b9d782e804c2f632e395708e99a94275910eb9100b2114651e04744e9b125006" - [[package]] name = "windows_i686_gnu" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b" -[[package]] -name = "windows_i686_gnu" -version = "0.53.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "960e6da069d81e09becb0ca57a65220ddff016ff2d6af6a223cf372a506593a3" - [[package]] name = "windows_i686_gnullvm" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" -[[package]] -name = "windows_i686_gnullvm" -version = "0.53.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fa7359d10048f68ab8b09fa71c3daccfb0e9b559aed648a8f95469c27057180c" - [[package]] name = "windows_i686_msvc" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" -[[package]] -name = "windows_i686_msvc" -version = "0.53.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1e7ac75179f18232fe9c285163565a57ef8d3c89254a30685b57d83a38d326c2" - [[package]] name = "windows_x86_64_gnu" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" -[[package]] -name = "windows_x86_64_gnu" -version = "0.53.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9c3842cdd74a865a8066ab39c8a7a473c0778a3f29370b5fd6b4b9aa7df4a499" - [[package]] name = "windows_x86_64_gnullvm" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" -[[package]] -name = "windows_x86_64_gnullvm" -version = "0.53.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0ffa179e2d07eee8ad8f57493436566c7cc30ac536a3379fdf008f47f6bb7ae1" - [[package]] name = "windows_x86_64_msvc" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" -[[package]] -name = "windows_x86_64_msvc" -version = "0.53.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d6bbff5f0aada427a1e5a6da5f1f98158182f26556f345ac9e04d36d0ebed650" - [[package]] name = "winnow" version = "0.7.15" @@ -3226,12 +2273,6 @@ dependencies = [ "wasmparser", ] -[[package]] -name = "writeable" -version = "0.6.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1ffae5123b2d3fc086436f8834ae3ab053a283cfac8fe0a0b8eaae044768a4c4" - [[package]] name = "xattr" version = "1.6.1" @@ -3242,70 +2283,6 @@ dependencies = [ "rustix", ] -[[package]] -name = "yoke" -version = "0.8.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "abe8c5fda708d9ca3df187cae8bfb9ceda00dd96231bed36e445a1a48e66f9ca" -dependencies = [ - "stable_deref_trait", - "yoke-derive", - "zerofrom", -] - -[[package]] -name = "yoke-derive" -version = "0.8.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "de844c262c8848816172cef550288e7dc6c7b7814b4ee56b3e1553f275f1858e" -dependencies = [ - "proc-macro2", - "quote", - "syn", - "synstructure", -] - -[[package]] -name = "zerocopy" -version = "0.8.48" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eed437bf9d6692032087e337407a86f04cd8d6a16a37199ed57949d415bd68e9" -dependencies = [ - "zerocopy-derive", -] - -[[package]] -name = "zerocopy-derive" -version = "0.8.48" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "70e3cd084b1788766f53af483dd21f93881ff30d7320490ec3ef7526d203bad4" -dependencies = [ - "proc-macro2", - "quote", - "syn", -] - -[[package]] -name = "zerofrom" -version = "0.1.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "69faa1f2a1ea75661980b013019ed6687ed0e83d069bc1114e2cc74c6c04c4df" -dependencies = [ - "zerofrom-derive", -] - -[[package]] -name = "zerofrom-derive" -version = "0.1.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "11532158c46691caf0f2593ea8358fed6bbf68a0315e80aae9bd41fbade684a1" -dependencies = [ - "proc-macro2", - "quote", - "syn", - "synstructure", -] - [[package]] name = "zeroize" version = "1.8.2" @@ -3313,40 +2290,35 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b97154e67e32c85465826e8bcc1c59429aaaf107c1e4a9e53c8d8ccd5eff88d0" [[package]] -name = "zerotrie" -version = "0.2.4" +name = "zmij" +version = "1.0.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0f9152d31db0792fa83f70fb2f83148effb5c1f5b8c7686c3459e361d9bc20bf" -dependencies = [ - "displaydoc", - "yoke", - "zerofrom", -] +checksum = "b8848ee67ecc8aedbaf3e4122217aff892639231befc6a1b58d29fff4c2cabaa" [[package]] -name = "zerovec" -version = "0.11.6" +name = "zstd" +version = "0.13.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "90f911cbc359ab6af17377d242225f4d75119aec87ea711a880987b18cd7b239" +checksum = "e91ee311a569c327171651566e07972200e76fcfe2242a4fa446149a3881c08a" dependencies = [ - "yoke", - "zerofrom", - "zerovec-derive", + "zstd-safe", ] [[package]] -name = "zerovec-derive" -version = "0.11.3" +name = "zstd-safe" +version = "7.2.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "625dc425cab0dca6dc3c3319506e6593dcb08a9f387ea3b284dbd52a92c40555" +checksum = "8f49c4d5f0abb602a93fb8736af2a4f4dd9512e36f7f570d66e65ff867ed3b9d" dependencies = [ - "proc-macro2", - "quote", - "syn", + "zstd-sys", ] [[package]] -name = "zmij" -version = "1.0.21" +name = "zstd-sys" +version = "2.0.16+zstd.1.5.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b8848ee67ecc8aedbaf3e4122217aff892639231befc6a1b58d29fff4c2cabaa" +checksum = "91e19ebc2adc8f83e43039e79776e3fda8ca919132d68a1fed6a5faca2683748" +dependencies = [ + "cc", + "pkg-config", +] diff --git a/anneal/Cargo.toml b/anneal/Cargo.toml index 7ade4f2fd4..c20b7da954 100644 --- a/anneal/Cargo.toml +++ b/anneal/Cargo.toml @@ -21,6 +21,25 @@ publish = true exclude = [".*", "testdata"] +# FIXME: Replace these placeholder archive URLs and hashes before publishing +# this crate; `cargo anneal setup` uses this metadata by default when callers +# do not provide a local archive. +[package.metadata.exocrate.linux.x86_64] +sha256 = "ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad" +url = "https://example.com/linux-x86_64.tar.zst" + +[package.metadata.exocrate.macos.x86_64] +sha256 = "ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad" +url = "https://example.com/macos-x86_64.tar.zst" + +[package.metadata.exocrate.linux.aarch64] +sha256 = "ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad" +url = "https://example.com/linux-aarch64.tar.zst" + +[package.metadata.exocrate.macos.aarch64] +sha256 = "ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad" +url = "https://example.com/macos-aarch64.tar.zst" + [dependencies] anyhow = "1.0.102" cargo_metadata = "0.23.1" @@ -46,16 +65,14 @@ thiserror = "2.0.18" walkdir = "2.5.0" indicatif = { version = "0.18.4", features = ["improved_unicode"] } console = "0.16.3" +exocrate = { path = "../exocrate" } sha2 = "0.10" fs2 = "0.4" toml = "0.8" -reqwest = { version = "0.12", features = ["blocking", "rustls-tls"] } -dirs = "6.0" tempfile = "3.27.0" -tar = "0.4" -flate2 = "1.1" [build-dependencies] +sha2 = "0.10" toml = "0.8" [dev-dependencies] @@ -89,7 +106,7 @@ aeneas_rev = "42c0e90dacf486f7d3ed5b6cde3a9a81f04915a4" # The Lean toolchain version to use. This must match the version of Lean used # by Aeneas in the `lean-toolchain` file in the commit above. -lean_toolchain = "leanprover/lean4:v4.28.0-rc1" +lean_toolchain = "leanprover/lean4:v4.30.0-rc2" # The Rust toolchain required by Charon. # diff --git a/anneal/Dockerfile b/anneal/Dockerfile index 17f97c8df6..37a9a03d84 100644 --- a/anneal/Dockerfile +++ b/anneal/Dockerfile @@ -1,6 +1,6 @@ FROM python:3.11-slim AS extractor WORKDIR /app -COPY Cargo.toml ./ +COPY anneal/Cargo.toml ./ # Remove the [workspace] section so it can be built as a standalone package. # Also inject tree-sitter dependencies used by doc_gen to cache them too. RUN sed '1,2d' Cargo.toml > Cargo.toml.no_workspace && \ @@ -51,23 +51,22 @@ ENV ANNEAL_INTEGRATION_TARGET_DIR=/cache/anneal_target # via a volume mount, causing dependencies to be rebuilt once in the volume. # This double-build is intentional to support both environments efficiently. ENV CARGO_TARGET_DIR=/opt/anneal_target -WORKDIR /workspace +WORKDIR /workspace/anneal # Copy the workspace configuration (without workspace section) and lockfile. COPY --from=extractor --chown=anneal:anneal /app/Cargo.toml.no_workspace ./Cargo.toml -COPY --chown=anneal:anneal Cargo.lock ./ +COPY --chown=anneal:anneal anneal/Cargo.lock ./ -# Copy source files needed for setup. -COPY --chown=anneal:anneal src/setup.rs src/util.rs ./src/ -COPY --chown=anneal:anneal build.rs ./ -COPY --chown=anneal:anneal tools/prune_mathlib.py ./tools/ +# Copy source files needed to compile dependency-heavy modules. +COPY --chown=anneal:anneal anneal/src/setup.rs ./src/ +COPY --chown=anneal:anneal exocrate/Cargo.toml /workspace/exocrate/Cargo.toml +COPY --chown=anneal:anneal exocrate/src /workspace/exocrate/src +COPY --chown=anneal:anneal anneal/build.rs ./ -# Create a minimal `main.rs` that runs setup, and a dummy test file. -# This allows us to build all dependencies (including dev-dependencies) -# in the image while still being able to run `setup`. It also avoids taking -# a dependency on *most* source files, avoiding unnecessary container rebuilds -# when source files change. -RUN echo 'mod setup; mod util; fn main() -> anyhow::Result<()> { setup::run_setup() }' > src/main.rs && \ +# Create a minimal `main.rs` and a dummy test file. +# This allows us to build dependencies in the image without copying the full +# source tree, avoiding unnecessary container rebuilds when source files change. +RUN echo 'mod setup; fn main() {}' > src/main.rs && \ mkdir tests && echo 'fn main() {}' > tests/integration.rs # Build dependencies to cache them in the image. @@ -78,19 +77,9 @@ RUN echo 'mod setup; mod util; fn main() -> anyhow::Result<()> { setup::run_setu RUN cargo build && \ cargo build --tests -# Pre-build Lean libraries using the minimal binary. -# -# We also generate the import graph and prune unused Mathlib artifacts here -# to reduce the image size. This must be done after `cargo run` because that -# command fetches and builds the dependencies. +# Use a stable shared install root inside test containers. CI installs the +# Nix-built archive here before invoking tests or examples. ENV ANNEAL_TOOLCHAIN_DIR=/opt/anneal_toolchain -RUN cargo run && \ - chmod -R u+w /opt/anneal_toolchain && \ - LEAN_DIR=$(find /opt/anneal_toolchain/.anneal/toolchain/ -type d -path "*/backends/lean" | head -n 1) && \ - cd $LEAN_DIR && \ - lake exe graph /workspace/imports.dot --to Aeneas,Aeneas.Std.Core,Aeneas.Std.WP,Aeneas.Tactic.Solver.ScalarTac,Aeneas.Std.Scalar.Core --include-deps && \ - python3 /workspace/tools/prune_mathlib.py /workspace/imports.dot ../../packages/mathlib && \ - chmod -R a-w /opt/anneal_toolchain # Ensure the integration target directory exists. RUN mkdir -p /cache/anneal_target diff --git a/anneal/build.rs b/anneal/build.rs index 4685aec69f..dbbacebd99 100644 --- a/anneal/build.rs +++ b/anneal/build.rs @@ -1,5 +1,7 @@ use std::fs; +use sha2::{Digest as _, Sha256}; + /// This build script reads toolchain versioning metadata from `Cargo.toml` and /// exposes it to the Rust compiler via environment variables. /// @@ -17,6 +19,8 @@ fn main() { let cargo_toml: toml::Value = toml::from_str(&cargo_toml_content).expect("failed to parse Cargo.toml"); + println!("cargo:rustc-env=ANNEAL_EXOCRATE_VERSION_SLUG={}", exocrate_version_slug()); + // We expect the metadata to be under `[package.metadata.build_rs]`. let build_rs_metadata = cargo_toml .get("package") @@ -72,4 +76,54 @@ fn main() { } } } + + if let Some(exocrate_metadata) = cargo_toml + .get("package") + .and_then(|p| p.get("metadata")) + .and_then(|m| m.get("exocrate")) + .and_then(|e| e.as_table()) + { + for (os, os_table) in exocrate_metadata { + let Some(os_table) = os_table.as_table() else { + continue; + }; + for (arch, config) in os_table { + let Some(config) = config.as_table() else { + continue; + }; + let env_platform = format!("{}_{}", os, arch).to_uppercase(); + + for key in ["sha256", "url"] { + let value = config.get(key).and_then(|v| v.as_str()).unwrap_or_else(|| { + panic!("package.metadata.exocrate.{os}.{arch}.{key} must be a string") + }); + println!( + "cargo:rustc-env=ANNEAL_EXOCRATE_{}_{}={}", + env_platform, + key.to_uppercase(), + value + ); + } + } + } + } +} + +fn exocrate_version_slug() -> String { + let mut hasher = Sha256::new(); + for path in ["Cargo.toml", "Cargo.lock"] { + hasher.update(path.as_bytes()); + hasher.update(fs::read(path).unwrap_or_else(|err| panic!("failed to read {path}: {err}"))); + } + hasher.update( + std::env::var("CARGO_CFG_TARGET_OS") + .expect("CARGO_CFG_TARGET_OS is set by Cargo") + .as_bytes(), + ); + hasher.update( + std::env::var("CARGO_CFG_TARGET_ARCH") + .expect("CARGO_CFG_TARGET_ARCH is set by Cargo") + .as_bytes(), + ); + format!("{:x}", hasher.finalize()) } diff --git a/anneal/docker.sh b/anneal/docker.sh index 49e400a1c8..d0d9ae3085 100755 --- a/anneal/docker.sh +++ b/anneal/docker.sh @@ -34,14 +34,16 @@ if [ "${DOCKER_CMD[0]}" = "podman" ]; then ARG_GID=1001 fi -# Resolve the directory paths required to mount the workspace volume into the -# container. This assumes that the script is located in the root of the -# `anneal` workspace. -DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" >/dev/null 2>&1 && pwd)" +# Resolve the directory paths required to build the image and mount the +# workspace volume into the container. The Docker build context is the repo +# worktree root so the Dockerfile can copy both `anneal/` and the root-level +# `exocrate/` crate. +ANNEAL_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" >/dev/null 2>&1 && pwd)" +WORKTREE_DIR="$(cd "$ANNEAL_DIR/.." >/dev/null 2>&1 && pwd)" # To avoid pollution between different git worktrees, we generate a unique # worktree ID and store it in a file. This ensures each worktree gets its own # isolated cache volume and Docker image tag. -WORKTREE_ID_FILE="$DIR/.docker-worktree-id" +WORKTREE_ID_FILE="$ANNEAL_DIR/.docker-worktree-id" if [ ! -f "$WORKTREE_ID_FILE" ]; then if command -v uuidgen >/dev/null 2>&1; then uuidgen > "$WORKTREE_ID_FILE" @@ -63,7 +65,7 @@ BUILD_CACHE=$(mktemp) # and capture its output to prevent terminal spam during cached runs. If the # build takes longer than 5 seconds, we assume a rebuild is occurring and # stream the output to the terminal so the developer knows why it is pausing. -DOCKER_BUILDKIT=1 "${DOCKER_CMD[@]}" build --progress=plain --build-arg UID=$ARG_UID --build-arg GID=$ARG_GID -t "$IMAGE_NAME" -f "$DIR/Dockerfile" "$DIR" > "$BUILD_CACHE" 2>&1 & +DOCKER_BUILDKIT=1 "${DOCKER_CMD[@]}" build --progress=plain --build-arg UID=$ARG_UID --build-arg GID=$ARG_GID -t "$IMAGE_NAME" -f "$ANNEAL_DIR/Dockerfile" "$WORKTREE_DIR" > "$BUILD_CACHE" 2>&1 & BUILD_PID=$! # Wait up to 5 seconds for the build to finish silently. @@ -185,10 +187,10 @@ done # Determine the user's current working directory relative to the repository. # This path is passed to Docker so that the container executes the requested # command in the same relative directory as the caller. -REL_PATH=$(realpath --relative-to="$DIR" "$(pwd)" 2>/dev/null || echo ".") +REL_PATH=$(realpath --relative-to="$WORKTREE_DIR" "$(pwd)" 2>/dev/null || echo "anneal") WORKDIR="/workspace/$REL_PATH" exec "${DOCKER_CMD[@]}" run "${DOCKER_FLAGS[@]}" \ - -v "$DIR:/workspace" \ + -v "$WORKTREE_DIR:/workspace" \ -w "$WORKDIR" \ "$IMAGE_NAME" "$@" diff --git a/anneal/src/aeneas.rs b/anneal/src/aeneas.rs index 0088e6943e..534cc43e4f 100644 --- a/anneal/src/aeneas.rs +++ b/anneal/src/aeneas.rs @@ -11,11 +11,12 @@ // back to Rust. use std::{ + ffi::OsString, fmt::Write, fs, io::{BufRead, BufReader}, - path::Path, - process::{Command, Stdio}, + path::{Path, PathBuf}, + process::Stdio, sync::{Arc, Mutex}, }; @@ -92,6 +93,7 @@ pub fn run_aeneas( .context("Failed to write Lean toolchain")?; let mut lake_roots = vec!["Generated".to_string()]; + let toolchain = crate::setup::Toolchain::resolve()?; for artifact in artifacts { if artifact.start_from.is_empty() { @@ -120,7 +122,6 @@ pub fn run_aeneas( std::fs::create_dir_all(&output_dir).context("Failed to create Aeneas output directory")?; - let toolchain = crate::setup::Toolchain::resolve()?; let mut cmd = toolchain.command(Tool::Aeneas); cmd.args(["-backend", "lean"]) @@ -269,11 +270,14 @@ pub fn run_aeneas( // 4. Write Lakefile // - // If `ANNEAL_AENEAS_DIR` is set (e.g., in CI or local development via Docker), - // we use it. Otherwise, we default to the managed toolchain directory. - let toolchain = crate::setup::Toolchain::resolve()?; - let path = toolchain.root.display(); - let aeneas_dep = format!(r#"require aeneas from "{path}/backends/lean""#); + // Aeneas and its Lean dependencies are unpacked from the managed archive. + let path = materialize_aeneas_dependency(&tmp_lean_root, &lean_root, &toolchain)?; + let aeneas_dep = format!( + r#"-- Aeneas rev: {} +require aeneas from "{}""#, + env!("ANNEAL_AENEAS_REV"), + path.display() + ); let roots_str = lake_roots.iter().map(|r| format!("`{}", r)).collect::>().join(", "); @@ -333,6 +337,130 @@ lean_lib «User» where Ok(()) } +fn materialize_aeneas_dependency( + tmp_lean_root: &Path, + lean_root: &Path, + toolchain: &crate::setup::Toolchain, +) -> Result { + let vendor_root = tmp_lean_root.join("vendor").join("aeneas"); + let lean_dst = vendor_root.join("backends").join("lean"); + let packages_dst = vendor_root.join("packages"); + + println!("Materializing packages by copying from toolchain..."); + copy_toolchain_tree_writable(&toolchain.aeneas_lean_dir(), &lean_dst) + .context("Failed to copy Aeneas Lean package from toolchain")?; + copy_toolchain_tree_writable(&toolchain.aeneas_root().join("packages"), &packages_dst) + .context("Failed to copy Aeneas Lean dependencies from toolchain")?; + + Ok(lean_root.join("vendor").join("aeneas").join("backends").join("lean")) +} + +fn copy_toolchain_tree_writable(src: &Path, dst: &Path) -> Result<()> { + if dst.exists() { + fs::remove_dir_all(dst) + .with_context(|| format!("Failed to remove stale directory {}", dst.display()))?; + } + + let mut entries = WalkDir::new(src).into_iter(); + while let Some(entry) = entries.next() { + let entry = entry.with_context(|| format!("Failed to walk {}", src.display()))?; + let path = entry.path(); + let rel = path.strip_prefix(src).with_context(|| { + format!("Failed to relativize {} against {}", path.display(), src.display()) + })?; + let target = dst.join(rel); + + if is_lake_build_dir(rel) { + // The Nix-built archive already contains Lake build caches for the + // immutable Aeneas dependency tree. Link those caches back to the + // read-only toolchain instead of copying several GiB of `.olean` + // files into every generated Lean workspace. The surrounding + // package/config/source files are still copied below so Lake can + // update small mutable metadata such as `.lake/config`. + if let Some(parent) = target.parent() { + fs::create_dir_all(parent).with_context(|| { + format!("Failed to create parent directory {}", parent.display()) + })?; + } + create_symlink(path, &target).with_context(|| { + format!( + "Failed to link prebuilt Lake cache {} to {}", + path.display(), + target.display() + ) + })?; + entries.skip_current_dir(); + } else if entry.file_type().is_dir() { + fs::create_dir_all(&target) + .with_context(|| format!("Failed to create directory {}", target.display()))?; + } else if entry.file_type().is_symlink() { + let link = fs::read_link(path) + .with_context(|| format!("Failed to read symlink {}", path.display()))?; + if let Some(parent) = target.parent() { + fs::create_dir_all(parent).with_context(|| { + format!("Failed to create parent directory {}", parent.display()) + })?; + } + create_symlink(&link, &target) + .with_context(|| format!("Failed to copy symlink {}", target.display()))?; + } else if entry.file_type().is_file() { + if let Some(parent) = target.parent() { + fs::create_dir_all(parent).with_context(|| { + format!("Failed to create parent directory {}", parent.display()) + })?; + } + fs::copy(path, &target).with_context(|| { + format!("Failed to copy {} to {}", path.display(), target.display()) + })?; + make_writable(&target)?; + } + } + + for entry in WalkDir::new(dst).contents_first(true) { + let entry = entry.with_context(|| format!("Failed to walk {}", dst.display()))?; + if !entry.file_type().is_symlink() { + make_writable(entry.path())?; + } + } + + Ok(()) +} + +fn is_lake_build_dir(rel: &Path) -> bool { + rel.file_name().is_some_and(|name| name == "build") + && rel.parent().and_then(Path::file_name).is_some_and(|name| name == ".lake") +} + +#[cfg(unix)] +fn create_symlink(src: &Path, dst: &Path) -> std::io::Result<()> { + std::os::unix::fs::symlink(src, dst) +} + +#[cfg(windows)] +fn create_symlink(src: &Path, dst: &Path) -> std::io::Result<()> { + if src.is_dir() { + std::os::windows::fs::symlink_dir(src, dst) + } else { + std::os::windows::fs::symlink_file(src, dst) + } +} + +fn make_writable(path: &Path) -> Result<()> { + let metadata = + fs::symlink_metadata(path).with_context(|| format!("Failed to stat {}", path.display()))?; + if metadata.file_type().is_symlink() { + return Ok(()); + } + let mut perms = metadata.permissions(); + if perms.readonly() { + #[allow(clippy::permissions_set_readonly_false)] + perms.set_readonly(false); + fs::set_permissions(path, perms) + .with_context(|| format!("Failed to make {} writable", path.display()))?; + } + Ok(()) +} + /// Generates Anneal `Specs.lean` and writes `Generated.lean`, but does not run the `lake build`. pub fn generate_lean_workspace(roots: &LockedRoots, artifacts: &[AnnealArtifact]) -> Result<()> { let lean_generated_root = roots.lean_generated_root(); @@ -375,219 +503,6 @@ pub fn generate_lean_workspace(roots: &LockedRoots, artifacts: &[AnnealArtifact] write_if_changed(&lean_generated_root.join("Generated.lean"), &generated_imports) .context("Failed to write Generated.lean")?; - // To avoid a slow full rebuild of dependencies in the newly generated - // workspace, we manually materialize the dependencies and fix up Lake's - // build trace files. - // - // Lake records absolute paths in its trace files. By default, when we - // generate a workspace and run `lake build`, Lake clones the dependencies - // into the workspace's `.lake/packages` directory. Since the paths in the - // clone do not match the paths in the toolchain where dependencies were - // pre-built, Lake considers the traces invalid and rebuilds everything. - // - // We bypass this by: - // - Manually writing the manifest with local file URLs. - // - Copying the pre-built dependency directories directly from the - // toolchain to avoid cloning (using our symlink-optimized materialize - // helper). - // - Post-processing the trace files to replace toolchain paths with - // workspace paths. - - // We read the `lake-manifest.json` generated during toolchain setup, - // modify it to include Aeneas as a dependency, and write it directly - // to the workspace. This prevents Lake from running dependency - // resolution and post-update hooks that would attempt to download - // external assets. - println!("Writing modified manifest to generated workspace..."); - let lean_root = roots.lean_root(); - let toolchain = crate::setup::Toolchain::resolve()?; - let toolchain_manifest_path = - toolchain.root.join("backends").join("lean").join("lake-manifest.json"); - let user_manifest_path = lean_root.join("lake-manifest.json"); - - if toolchain_manifest_path.exists() { - let content = fs::read_to_string(&toolchain_manifest_path) - .context("Failed to read toolchain manifest")?; - let mut manifest: serde_json::Value = - serde_json::from_str(&content).context("Failed to parse toolchain manifest")?; - - // Change name to anneal_verification - manifest["name"] = serde_json::Value::String("anneal_verification".to_string()); - - // Read Aeneas HEAD commit hash from the static file in the - // toolchain. This avoids invoking Git at runtime, which would crash - // inside Docker containers due to Git's "dubious ownership" - // security checks (due to mapped UIDs). - let toolchain_aeneas_dir = toolchain.root.join("backends").join("lean"); - let commit_file = toolchain_aeneas_dir.join("aeneas-commit.txt"); - let aeneas_rev = fs::read_to_string(&commit_file) - .with_context(|| format!("Failed to read static Aeneas commit hash from {}. Please re-run `cargo anneal setup`.", commit_file.display()))? - .trim() - .to_string(); - - // Inject aeneas dependency - let aeneas_dep = serde_json::json!({ - "configFile": "lakefile.lean", - "inherited": false, - "inputRev": "main", - "manifestFile": "lake-manifest.json", - "name": "aeneas", - "rev": aeneas_rev, - "scope": "", - "subDir": null, - "type": "git", - "url": format!("file://{}", toolchain_aeneas_dir.to_str().unwrap()) - }); - - if let Some(packages) = manifest["packages"].as_array_mut() { - // Rewrite any path dependencies (like mathlib) from the - // toolchain's relative structure (../../packages/mathlib) to - // the project's local sandbox structure - // (.lake/packages/mathlib). - for pkg in packages.iter_mut() { - if pkg["type"] == "path" { - if let Some(dir_str) = pkg["dir"].as_str() { - if dir_str == "../../packages/mathlib" { - pkg["dir"] = - serde_json::Value::String(".lake/packages/mathlib".to_string()); - } - } - } - } - - packages.insert(0, aeneas_dep); - } else { - bail!("Manifest packages is not an array"); - } - - let new_content = serde_json::to_string_pretty(&manifest) - .context("Failed to serialize modified manifest")?; - fs::write(&user_manifest_path, new_content).context("Failed to write user manifest")?; - } else { - bail!("Toolchain manifest missing at {}", toolchain_manifest_path.display()); - } - - // We manually materialize Aeneas and all resolved dependencies from - // the toolchain into the workspace's `.lake/packages` directory. - // We use our optimized symlink materializer to avoid physical copies. - println!("Materializing packages by copying from toolchain..."); - let user_project_packages = lean_root.join(".lake").join("packages"); - - // Ensure .lake/packages exists - fs::create_dir_all(&user_project_packages) - .context("Failed to create .lake/packages directory")?; - - // Copy Aeneas - let toolchain_aeneas_dir = toolchain.root.join("backends").join("lean"); - let user_aeneas_dir = user_project_packages.join("aeneas"); - - if toolchain_aeneas_dir.exists() { - materialize_package_optimized(&toolchain_aeneas_dir, &user_aeneas_dir) - .context("Failed to materialize Aeneas package")?; - - // Rename the Aeneas precompiled configuration directory from - // `[anonymous]` to `aeneas`, and patch its trace file so that - // Lake validates the precompiled configuration without - // re-elaborating it. - let anon_config = user_aeneas_dir.join(".lake").join("config").join("[anonymous]"); - let user_config = user_aeneas_dir.join(".lake").join("config").join("aeneas"); - if anon_config.exists() { - fs::create_dir_all(user_config.parent().unwrap()) - .context("Failed to create config parent directory")?; - fs::rename(&anon_config, &user_config) - .context("Failed to rename Aeneas precompiled config directory")?; - - let trace_file = user_config.join("lakefile.olean.trace"); - if trace_file.exists() { - let content = fs::read_to_string(&trace_file) - .context("Failed to read Aeneas config trace file")?; - let new_content = content.replace("[anonymous]", "aeneas"); - fs::write(&trace_file, new_content) - .context("Failed to write patched Aeneas config trace file")?; - } - } - - // Add Git remote 'origin' to match manifest - let status = Command::new("git") - .args([ - "remote", - "add", - "origin", - &format!("file://{}", toolchain_aeneas_dir.to_str().unwrap()), - ]) - .current_dir(&user_aeneas_dir) - .status() - .context("Failed to run `git remote add` in Aeneas clone")?; - if !status.success() { - bail!("`git remote add` failed in Aeneas clone"); - } - } - - // Copy dependencies - let toolchain_packages_dir = toolchain.root.join("packages"); - if toolchain_packages_dir.exists() { - for entry in fs::read_dir(&toolchain_packages_dir) - .context("Failed to read toolchain packages directory")? - { - let entry = entry.context("Failed to read directory entry")?; - let path = entry.path(); - if path.is_dir() { - let pkg_name = path.file_name().unwrap().to_str().unwrap(); - let user_pkg_dir = user_project_packages.join(pkg_name); - - materialize_package_optimized(&path, &user_pkg_dir) - .with_context(|| format!("Failed to materialize package {}", pkg_name))?; - - // Update Git remote URL to match manifest - let status = Command::new("git") - .args([ - "remote", - "set-url", - "origin", - &format!("file://{}", path.to_str().unwrap()), - ]) - .current_dir(&user_pkg_dir) - .status() - .context("Failed to run `git remote set-url` in package clone")?; - if !status.success() { - bail!("`git remote set-url` failed in package clone for {}", pkg_name); - } - } - } - } - - // Finally, we fix the non-portable absolute paths embedded in Lake's - // `.trace` files. We replace all occurrences of paths pointing to the - // toolchain with the corresponding paths in the workspace's clone - // directory. This convinces Lake that the pre-built artifacts are - // valid for the current workspace location. - println!("Post-processing traces in the clone..."); - let toolchain_aeneas = toolchain.root.join("backends").join("lean"); - let toolchain_aeneas_str = toolchain_aeneas.to_str().unwrap(); - let user_project_aeneas = user_project_packages.join("aeneas"); - let user_project_aeneas_str = user_project_aeneas.to_str().unwrap(); - let toolchain_packages_str = toolchain_packages_dir.to_str().unwrap(); - let user_project_packages_str = user_project_packages.to_str().unwrap(); - - // Process all packages in .lake/packages - if user_project_packages.exists() { - for entry in - fs::read_dir(&user_project_packages).context("Failed to read user project packages")? - { - let entry = entry.context("Failed to read directory entry")?; - let path = entry.path(); - if path.is_dir() { - crate::util::patch_trace_files( - &path.join(".lake").join("build"), - &[ - (toolchain_aeneas_str, user_project_aeneas_str), - (toolchain_packages_str, user_project_packages_str), - ], - )?; - } - } - } - Ok(()) } @@ -600,12 +515,8 @@ pub fn verify_lean_workspace(roots: &LockedRoots, artifacts: &[AnnealArtifact]) /// Runs the Lean build process and diagnostics. /// -/// This function: -/// 1. Patches `lake-manifest.json` if `ANNEAL_AENEAS_DIR` is set (for local dev). -/// 2. Fetches Mathlib cache to avoid rebuilding it. -/// 3. Builds the project with `lake build`. -/// 4. Executes the `Diagnostics.lean` script to check proofs. -/// 5. Parses JSON output from the script and maps it back to Rust source. +/// This function builds the generated project, runs Lean diagnostics, and maps +/// diagnostics back to Rust source. fn run_lake(roots: &LockedRoots, artifacts: &[AnnealArtifact]) -> Result<()> { let generated = roots.lean_generated_root(); let lean_root = generated.parent().unwrap(); @@ -613,9 +524,10 @@ fn run_lake(roots: &LockedRoots, artifacts: &[AnnealArtifact]) -> Result<()> { // 2. Build the project (dependencies only) let toolchain = crate::setup::Toolchain::resolve()?; - let mut cmd = toolchain.command(Tool::Lake); - cmd.args(["build", "Generated", "Anneal"]); + let mut cmd = std::process::Command::new(toolchain.lean_bin().join("lake")); + cmd.args(["--keep-toolchain", "--old", "build", "Generated", "Anneal"]); cmd.current_dir(lean_root); + configure_lake_command(&mut cmd, &toolchain)?; cmd.stdout(Stdio::piped()); cmd.stderr(Stdio::piped()); @@ -689,9 +601,10 @@ fn run_lake(roots: &LockedRoots, artifacts: &[AnnealArtifact]) -> Result<()> { let specs_rel_path = format!("generated/{}/{}", slug, artifact.lean_spec_file_name()); let toolchain = crate::setup::Toolchain::resolve()?; - let mut cmd = toolchain.command(Tool::Lake); - cmd.args(["env", "lean", "--json", &specs_rel_path]); + let mut cmd = std::process::Command::new(toolchain.lean_bin().join("lake")); + cmd.args(["--keep-toolchain", "env", "lean", "--json", &specs_rel_path]); cmd.current_dir(lean_root); + configure_lake_command(&mut cmd, &toolchain)?; cmd.stdout(Stdio::piped()); cmd.stderr(Stdio::piped()); @@ -799,6 +712,64 @@ fn run_lake(roots: &LockedRoots, artifacts: &[AnnealArtifact]) -> Result<()> { Ok(()) } +fn configure_lake_command( + cmd: &mut std::process::Command, + toolchain: &crate::setup::Toolchain, +) -> Result<()> { + // FIXME: Replace this with a cleaner toolchain/archive contract. + // + // The Nix-built archive contains prebuilt Lake outputs for the vendored + // Aeneas package, and `materialize_aeneas_dependency` links each generated + // verification workspace's `vendor/aeneas/backends/lean/.lake/build` back + // to that read-only archive cache. That is only sound if Lake evaluates the + // vendored Aeneas package with the same build configuration that was used + // when the archive was produced. + // + // Aeneas' Lakefile currently makes one of those build settings depend on + // the ambient `CI` environment variable: + // + // precompileModules := (IO.getEnv "CI").isNone + // + // Our archive is built without `CI` in the environment, but GitHub Actions + // sets `CI=true` for normal workflow steps. If we let that variable reach + // this child process, Lake observes a different Aeneas package config than + // the one recorded in the archive traces. It then invalidates the prebuilt + // cache and attempts to rebuild/remove files below the symlinked + // `.lake/build`, which fails because those archive files are intentionally + // read-only. + // + // Scrubbing `CI` here keeps local runs, example CI jobs, and the integration + // test harness aligned with the archive build environment. A cleaner future + // solution would make the archive's Lake configuration explicit and + // environment-independent, or otherwise arrange for Anneal to request the + // exact same Aeneas build variant that the archive contains. + cmd.env_remove("CI"); + + cmd.env("LEAN_SYSROOT", toolchain.lean_sysroot()); + cmd.env("MATHLIB_NO_CACHE_ON_UPDATE", "1"); + cmd.env("PATH", prepend_paths_to_env_var("PATH", &[toolchain.lean_bin()])?); + + let lib_env_var = + if cfg!(target_os = "macos") { "DYLD_LIBRARY_PATH" } else { "LD_LIBRARY_PATH" }; + cmd.env( + lib_env_var, + prepend_paths_to_env_var( + lib_env_var, + &[toolchain.lean_sysroot().join("lib"), toolchain.lean_sysroot().join("lib/lean")], + )?, + ); + + Ok(()) +} + +fn prepend_paths_to_env_var(var_name: &str, new_paths: &[PathBuf]) -> Result { + let mut paths = new_paths.to_vec(); + if let Some(existing) = std::env::var_os(var_name) { + paths.extend(std::env::split_paths(&existing)); + } + std::env::join_paths(paths).with_context(|| format!("Failed to prepend paths to {var_name}")) +} + /// Resolves a Lean diagnostic to a Rust source location. /// /// This uses the JSON source map generated during `src/generate.rs` to map @@ -999,184 +970,6 @@ fn write_if_changed(path: &std::path::Path, content: &str) -> Result<()> { Ok(()) } -/// Helper to make a copied file writable inside the project sandbox. -fn make_file_writable(path: &Path) -> Result<()> { - let mut perms = fs::metadata(path)?.permissions(); - #[allow(clippy::permissions_set_readonly_false)] - perms.set_readonly(false); - fs::set_permissions(path, perms).context("Failed to set write permissions")?; - Ok(()) -} - -/// Helper to recursively restore write permissions to a physically copied -/// directory (e.g., `.git`) inside the project sandbox. This is safe -/// because it does not contain symlinks. -fn make_dir_writable_recursive(path: &Path) -> Result<()> { - let walker = WalkDir::new(path).into_iter(); - for entry in walker { - let entry = entry.context("Failed to walk directory for write permissions")?; - make_file_writable(entry.path())?; - } - Ok(()) -} - -/// Helper to recursively copy a directory using the system `cp -r` -/// command. This is used for small directories like `.git` which contain -/// only metadata. -fn copy_dir_recursive(src: &Path, dest: &Path) -> Result<()> { - let status = Command::new("cp") - .args(["-r", src.to_str().unwrap(), dest.to_str().unwrap()]) - .status() - .context("Failed to run cp -r for directory copy")?; - if !status.success() { - bail!("cp -r failed for {}", src.display()); - } - Ok(()) -} - -/// Walk the source build directory recursively, creating all -/// subdirectories, copying `.trace` files physically (so they can be -/// patched), and symlinking all other files (like `.olean` binaries) to -/// save space and time. -fn materialize_build_dir_optimized(src_build: &Path, dest_build: &Path) -> Result<()> { - let walker = WalkDir::new(src_build).into_iter(); - for entry in walker { - let entry = entry.context("Failed to walk source build directory")?; - let path = entry.path(); - let rel_path = path.strip_prefix(src_build).unwrap(); - let dest_path = dest_build.join(rel_path); - - if path.is_dir() { - fs::create_dir_all(&dest_path) - .with_context(|| format!("Failed to create directory {}", dest_path.display()))?; - } else if path.is_file() { - if path.extension().map_or(false, |ext| ext == "trace") { - // Copy .trace file physically so we can patch its paths! - fs::copy(path, &dest_path) - .with_context(|| format!("Failed to copy trace file {}", path.display()))?; - make_file_writable(&dest_path)?; - } else { - // Create symlink for .olean or other binary build files - #[cfg(unix)] - std::os::unix::fs::symlink(path, &dest_path) - .with_context(|| format!("Failed to symlink build file {}", path.display()))?; - } - } - } - Ok(()) -} - -/// Materializes a pre-built toolchain package inside the user project's -/// `.lake/packages` directory in an optimized way. -/// -/// Instead of physically copying the package (which is slow), it only -/// copies metadata files and the `.git` directory, and creates symbolic -/// links for the massive source directories and `.lake/build` directory. -fn materialize_package_optimized(src_dir: &Path, dest_dir: &Path) -> Result<()> { - if dest_dir.exists() { - fs::remove_dir_all(dest_dir).context("Failed to remove existing package directory")?; - } - fs::create_dir_all(dest_dir).context("Failed to create package directory")?; - - for entry in fs::read_dir(src_dir).context("Failed to read source package directory")? { - let entry = entry.context("Failed to read directory entry")?; - let path = entry.path(); - let file_name = path.file_name().unwrap().to_str().unwrap(); - - if path.is_file() { - // Copy top-level metadata files - if file_name == "lakefile.lean" - || file_name == "lakefile.toml" - || file_name == "lean-toolchain" - || file_name == "lake-manifest.json" - { - let dest_file = dest_dir.join(file_name); - fs::copy(&path, &dest_file) - .with_context(|| format!("Failed to copy file {}", file_name))?; - make_file_writable(&dest_file)?; - } else if path.extension().map_or(false, |ext| ext == "lean") { - // Symlink root-level Lean source files (like - // Aeneas.lean, Qq.lean, Aesop.lean) - #[cfg(unix)] - std::os::unix::fs::symlink(&path, dest_dir.join(file_name)) - .with_context(|| format!("Failed to symlink root Lean file {}", file_name))?; - } - } else if path.is_dir() { - let pkg_name = dest_dir.file_name().unwrap().to_str().unwrap(); - if file_name == ".git" { - // Copy the .git directory so Lake thinks it's a valid - // git clone. - let dest_git = dest_dir.join(".git"); - copy_dir_recursive(&path, &dest_git)?; - make_dir_writable_recursive(&dest_git)?; - } else if file_name == "widget" && pkg_name == "proofwidgets" { - // Special case: proofwidgets has a custom JS widget - // compilation step that writes to - // `widget/package-lock.json.hash` and runs `npm - // install`. We must physically copy this folder and - // make it writable so it can execute locally inside the - // sandbox without writing to the toolchain. - let dest_widget = dest_dir.join("widget"); - copy_dir_recursive(&path, &dest_widget)?; - make_dir_writable_recursive(&dest_widget)?; - } else if file_name == ".lake" { - // Recreate the `.lake` structure and copy - // precompiled build and config data. - let src_build = path.join("build"); - let src_config = path.join("config"); - let dest_lake = dest_dir.join(".lake"); - let dest_build = dest_lake.join("build"); - let dest_config = dest_lake.join("config"); - - if src_build.exists() { - fs::create_dir_all(&dest_build) - .context("Failed to create dest build directory")?; - materialize_build_dir_optimized(&src_build, &dest_build)?; - } - - if src_config.exists() { - // Copy precompiled config - // physically and make it - // writable. - copy_dir_recursive(&src_config, &dest_config)?; - make_dir_writable_recursive(&dest_config)?; - - // Adjust the package index (`idx`) - // in the trace file. Since Aeneas - // is prepended at index 0 in the - // sandbox manifest, every other - // dependency's index shifts by +1. - // - // We parse the trace JSON, increment - // the `idx` field, and write it back. - let trace_file = dest_config.join(pkg_name).join("lakefile.olean.trace"); - if trace_file.exists() { - let content = fs::read_to_string(&trace_file) - .context("Failed to read trace file during config load")?; - if let Ok(mut json) = serde_json::from_str::(&content) { - if let Some(idx) = json["idx"].as_i64() { - json["idx"] = serde_json::Value::Number((idx + 1).into()); - let new_content = serde_json::to_string_pretty(&json) - .context("Failed to serialize patched config trace")?; - fs::write(&trace_file, new_content) - .context("Failed to write patched config trace file")?; - } - } - } - } - } else { - // This is a source directory (e.g., `Mathlib/`, - // `Aeneas/`, `Batteries/`). We create a SYMLINK to it - // from the toolchain to share all .lean files! - #[cfg(unix)] - std::os::unix::fs::symlink(&path, dest_dir.join(file_name)) - .with_context(|| format!("Failed to symlink directory {}", file_name))?; - } - } - } - Ok(()) -} - #[cfg(test)] mod tests { use std::path::PathBuf; diff --git a/anneal/src/charon.rs b/anneal/src/charon.rs index 945fb20dde..7e33bda392 100644 --- a/anneal/src/charon.rs +++ b/anneal/src/charon.rs @@ -40,10 +40,6 @@ pub fn run_charon(args: &Args, roots: &LockedRoots, packages: &[AnnealArtifact]) let toolchain = crate::setup::Toolchain::resolve()?; - let rust_sysroot = toolchain.root.join("rust"); - let rust_bin = rust_sysroot.join("bin"); - let rust_lib = rust_sysroot.join("lib"); - // Helper closure to prepend a path to an existing environment variable, // separating them with a colon if the variable is not empty. This is used // to inject our managed Rust toolchain paths before the system paths. @@ -57,11 +53,11 @@ pub fn run_charon(args: &Args, roots: &LockedRoots, packages: &[AnnealArtifact]) combined }; - let new_path = prepend_to_env_var("PATH", rust_bin); + let new_path = prepend_to_env_var("PATH", toolchain.rust_bin()); let lib_env_var = if cfg!(target_os = "macos") { "DYLD_LIBRARY_PATH" } else { "LD_LIBRARY_PATH" }; - let new_lib_path = prepend_to_env_var(lib_env_var, rust_lib); + let new_lib_path = prepend_to_env_var(lib_env_var, toolchain.rust_lib()); for artifact in packages { if artifact.start_from.is_empty() { diff --git a/anneal/src/main.rs b/anneal/src/main.rs index 05748849d8..3d363b977d 100644 --- a/anneal/src/main.rs +++ b/anneal/src/main.rs @@ -87,16 +87,20 @@ fn main() -> anyhow::Result<()> { println!(); println!("To manually build and experiment:"); println!(" 1. cd {}", lean_root.display()); - println!(" 2. LAKE_CACHE_DIR={} lake build", toolchain.cache_dir().display()); + println!( + " 2. LAKE_CACHE_DIR={} {} --keep-toolchain build", + toolchain.cache_dir().display(), + toolchain.lean_bin().join("lake").display() + ); Ok(()) })?; } - Commands::Setup(resolve::SetupArgs {}) => { - setup::run_setup()?; + Commands::Setup(args) => { + setup::run_setup(setup::SetupArgs { local_archive: args.local_archive })?; } Commands::ToolchainPath => { let toolchain = setup::Toolchain::resolve()?; - println!("{}", toolchain.root.display()); + println!("{}", toolchain.bin_dir().display()); } Commands::Expand(expand_args) => { prepare_and_run(&expand_args.resolve_args, |locked_roots, packages| { diff --git a/anneal/src/resolve.rs b/anneal/src/resolve.rs index 3294916e47..9a44f65296 100644 --- a/anneal/src/resolve.rs +++ b/anneal/src/resolve.rs @@ -68,7 +68,11 @@ pub struct Args { } #[derive(Parser, Debug)] -pub struct SetupArgs {} +pub struct SetupArgs { + /// Install dependencies from a locally built exocrate archive. + #[arg(long, value_name = "path-to-local-archive")] + pub local_archive: Option, +} #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] #[repr(u8)] @@ -224,16 +228,9 @@ pub fn resolve_roots(args: &Args) -> Result { args.features.forward_metadata(&mut cmd); let metadata = cmd.exec().context("Failed to run 'cargo metadata'")?; - // We enforce that all local dependencies are contained within the workspace - // root. This is a temporary limitation to simplify the verification model - // and ensure a "hermetic-like" boundary for analysis. It prevents issues - // where experimental or local forks of dependencies might be picked up - // unpredictably, or where Charon might struggle to locate source files - // outside the standard project structure. - check_for_external_deps(&metadata)?; - let selected_packages = resolve_packages(&metadata, &args.workspace, args.manifest.manifest_path.as_deref())?; + check_selected_packages_in_workspace(&metadata, &selected_packages)?; let (anneal_global_root, anneal_run_root) = resolve_run_roots(&metadata); let mut roots = Roots { @@ -442,39 +439,38 @@ fn resolve_targets<'a>( Ok(selected_artifacts) } -// TODO: Eventually, we'll want to support external path dependencies by -// analyzing them in-place or ensuring they are accessible to Charon. +// TODO: Eventually, we'll want to support selected packages outside the Cargo +// workspace root by analyzing them in-place or teaching downstream stages how +// to map those source files. -/// Scans the package graph to ensure all local dependencies are contained -/// within the workspace root. Returns an error if an external path dependency -/// is found. -pub fn check_for_external_deps(metadata: &Metadata) -> Result<()> { - log::trace!("check_for_external_deps"); +/// Ensures every selected verification root is contained within the workspace root. +fn check_selected_packages_in_workspace(metadata: &Metadata, packages: &[&Package]) -> Result<()> { + log::trace!("check_selected_packages_in_workspace"); // Canonicalize workspace root to handle symlinks correctly let workspace_root = fs::canonicalize(&metadata.workspace_root) .context("Failed to canonicalize workspace root")?; - for pkg in &metadata.packages { - // We only care about packages that are "local" (source is None). - // If source is Some(...), it's from crates.io or git, which is fine - // (handled by Cargo). - if pkg.source.is_none() { - let pkg_path = pkg.manifest_path.as_std_path(); - - // Canonicalize the package path for comparison - let canonical_pkg_path = fs::canonicalize(pkg_path) - .with_context(|| format!("Failed to canonicalize path for package {}", pkg.name))?; - - // Check if the package lives outside the workspace tree - if !canonical_pkg_path.starts_with(&workspace_root) { - anyhow::bail!( - "Unsupported external dependency: '{}' at {:?}.\n\ - Anneal currently only supports verifying workspaces where all local \ - dependencies are contained within the workspace root.", - pkg.name, - pkg_path - ); - } + for pkg in packages { + let pkg_path = pkg.manifest_path.as_std_path(); + + // Canonicalize the package path for comparison + let canonical_pkg_path = fs::canonicalize(pkg_path) + .with_context(|| format!("Failed to canonicalize path for package {}", pkg.name))?; + + // We only constrain the packages Anneal will scan as verification + // roots. Cargo metadata may also include build-only local path + // dependencies from the Anneal implementation itself, such as the + // repository-root `exocrate` helper crate when running + // `cargo run verify`. Rejecting those would make Anneal's own package + // layout constrain user verification. + if !canonical_pkg_path.starts_with(&workspace_root) { + anyhow::bail!( + "Unsupported external package: '{}' at {:?}.\n\ + Anneal currently only supports verifying packages contained \ + within the workspace root.", + pkg.name, + pkg_path + ); } } diff --git a/anneal/src/setup.rs b/anneal/src/setup.rs index e864ed8af1..ba84910a82 100644 --- a/anneal/src/setup.rs +++ b/anneal/src/setup.rs @@ -1,1107 +1,191 @@ //! Subcommand for installing Anneal dependencies. -//! -//! This module handles the automated download, verification, and installation -//! of `charon`, `charon-driver`, and `aeneas`. -use std::{fs, io::Read, path::Path, process::Command}; +use std::{path::PathBuf, process::Command}; -use anyhow::{Context, Result, bail}; -use flate2::read::GzDecoder; -use sha2::{Digest, Sha256}; -use tar::Archive; -use tempfile; -use walkdir::WalkDir; +use anyhow::Context as _; -use crate::util::DirLock; - -const MOCK_RUSTC_HASH: [u8; 32] = const { - decode_hex("0d98244543ccb295295e0e9b335fbace9e06e8121bbdad6135773bca27f507f5") - .expect("valid hex") -}; -const MOCK_RUST_STD_HASH: [u8; 32] = const { - decode_hex("31d62a14beb156f010188c39cb5e6069fa6f4f0d48e06f961a9888cf9263d8c6") - .expect("valid hex") -}; -const MOCK_RUSTC_DEV_HASH: [u8; 32] = const { - decode_hex("7680c83ea3ab6bae514155ee3924d9b452e6f6c852552a266943142806653a8c") - .expect("valid hex") -}; -const MOCK_LLVM_TOOLS_HASH: [u8; 32] = const { - decode_hex("c44c8e08c9e1411589402262a960226918d5051f77bd76912a3cb09c3393f198") - .expect("valid hex") -}; -const MOCK_MIRI_HASH: [u8; 32] = const { - decode_hex("c093bdc1b9749b19ae3f93e3a6d58c901b5d94d09b80690f24e060d1a121a4d7") - .expect("valid hex") -}; -const MOCK_RUST_SRC_HASH: [u8; 32] = const { - decode_hex("c2aa19f097efaa4d789911e3b1b4c1bb8379e4ac4ce66c47d60d0144f0307482") - .expect("valid hex") -}; - -macro_rules! decode_hex_env { - ($key:expr) => { - const { decode_hex(env!($key)).expect("valid hex") } - }; +pub struct SetupArgs { + pub local_archive: Option, } -/// Supported platforms for Anneal dependencies. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Platform { - LinuxX86_64, - LinuxAArch64, - MacosAArch64, - MacosX86_64, -} +pub const CONFIG: exocrate::Config = exocrate::Config { + rel_dir_path: &[".anneal", "toolchain"], + version_slug: env!("ANNEAL_EXOCRATE_VERSION_SLUG"), +}; -/// A specific tool or component within an Anneal dependency. #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum Tool { Charon, + #[allow(dead_code)] CharonDriver, Aeneas, - Lake, - Rustc, - Miri, - RustStd, - RustcDev, - LlvmTools, - RustSrc, } impl Tool { - /// Returns the name of the binary or component for this tool. pub fn name(&self) -> &'static str { match self { Self::Charon => "charon", Self::CharonDriver => "charon-driver", Self::Aeneas => "aeneas", - Self::Lake => "lake", - Self::Rustc => "rustc", - Self::Miri => "miri", - Self::RustStd => "rust-std", - Self::RustcDev => "rustc-dev", - Self::LlvmTools => "llvm-tools", - Self::RustSrc => "rust-src", - } - } -} - -impl Platform { - /// Returns the target triple for this platform. - pub fn triple(&self) -> &'static str { - match self { - Self::LinuxX86_64 => "x86_64-unknown-linux-gnu", - Self::LinuxAArch64 => "aarch64-unknown-linux-gnu", - Self::MacosAArch64 => "aarch64-apple-darwin", - Self::MacosX86_64 => "x86_64-apple-darwin", - } - } - - /// Detects the current host platform. - pub fn detect() -> Result { - let os = std::env::consts::OS; - let arch = std::env::consts::ARCH; - - match (os, arch) { - ("linux", "x86_64") => Ok(Self::LinuxX86_64), - ("linux", "aarch64") => Ok(Self::LinuxAArch64), - ("macos", "aarch64") => Ok(Self::MacosAArch64), - ("macos", "x86_64") => Ok(Self::MacosX86_64), - _ => bail!("Unsupported platform: {}-{}", os, arch), } } - /// Returns the expected SHA-256 checksum for the specified archive on this - /// platform. - /// - /// These hashes are baked into the binary at compile time from values - /// provided by `build.rs` from the project's `Cargo.toml`. This ensures - /// that we always download and verify the exact versions of dependencies - /// that this version of Anneal was built to work with. - pub fn expected_archive_hash(&self) -> [u8; 32] { - use Platform::*; + pub fn path(&self, toolchain: &Toolchain) -> PathBuf { match self { - LinuxX86_64 => decode_hex_env!("ANNEAL_AENEAS_CHECKSUM_LINUX_X86_64"), - LinuxAArch64 => decode_hex_env!("ANNEAL_AENEAS_CHECKSUM_LINUX_AARCH64"), - MacosAArch64 => decode_hex_env!("ANNEAL_AENEAS_CHECKSUM_MACOS_AARCH64"), - MacosX86_64 => decode_hex_env!("ANNEAL_AENEAS_CHECKSUM_MACOS_X86_64"), - } - } - - /// Returns the expected SHA-256 checksum for a specific binary on this - /// platform. - /// - /// This is used for verifying individual binaries within a toolchain, - /// allowing the `setup` command to detect and repair corruption of any - /// of the toolchain components. - pub fn expected_bin_hash(&self, tool: Tool) -> [u8; 32] { - if std::env::var("__ANNEAL_USE_MOCK_RUST_HASHES").is_ok() { - // When testing with mock Rust hashes, we intercept requests for Rust - // components and return the hardcoded mock hashes. For non-Rust - // tools, we fall through to the normal logic that reads hashes from - // environment variables. - // - // This approach is acceptable from a security perspective because: - // 1. The mock hashes are hardcoded in the binary and cannot be - // overridden by an attacker via environment variables. - // 2. The mock archives only contain inert, empty files. Even if an - // attacker forces the use of these mocks, they can only cause - // the tool to fail to run, but cannot inject malicious behavior. - use Tool::*; - match tool { - Rustc => return MOCK_RUSTC_HASH, - RustStd => return MOCK_RUST_STD_HASH, - RustcDev => return MOCK_RUSTC_DEV_HASH, - LlvmTools => return MOCK_LLVM_TOOLS_HASH, - Miri => return MOCK_MIRI_HASH, - RustSrc => return MOCK_RUST_SRC_HASH, - Charon | CharonDriver | Aeneas | Lake => {} - } - } - - use Platform::*; - match (self, tool) { - // Rust components - (LinuxX86_64, Tool::Rustc) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_LINUX_X86_64_RUSTC") - } - (LinuxX86_64, Tool::RustStd) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_LINUX_X86_64_RUST_STD") - } - (LinuxX86_64, Tool::RustcDev) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_LINUX_X86_64_RUSTC_DEV") - } - (LinuxX86_64, Tool::LlvmTools) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_LINUX_X86_64_LLVM_TOOLS_PREVIEW") - } - (LinuxX86_64, Tool::Miri) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_LINUX_X86_64_MIRI_PREVIEW") - } - - (LinuxAArch64, Tool::Rustc) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_LINUX_AARCH64_RUSTC") - } - (LinuxAArch64, Tool::RustStd) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_LINUX_AARCH64_RUST_STD") - } - (LinuxAArch64, Tool::RustcDev) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_LINUX_AARCH64_RUSTC_DEV") - } - (LinuxAArch64, Tool::LlvmTools) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_LINUX_AARCH64_LLVM_TOOLS_PREVIEW") - } - (LinuxAArch64, Tool::Miri) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_LINUX_AARCH64_MIRI_PREVIEW") - } - - (MacosX86_64, Tool::Rustc) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_MACOS_X86_64_RUSTC") - } - (MacosX86_64, Tool::RustStd) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_MACOS_X86_64_RUST_STD") - } - (MacosX86_64, Tool::RustcDev) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_MACOS_X86_64_RUSTC_DEV") - } - (MacosX86_64, Tool::LlvmTools) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_MACOS_X86_64_LLVM_TOOLS_PREVIEW") - } - (MacosX86_64, Tool::Miri) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_MACOS_X86_64_MIRI_PREVIEW") - } - - (MacosAArch64, Tool::Rustc) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_MACOS_AARCH64_RUSTC") - } - (MacosAArch64, Tool::RustStd) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_MACOS_AARCH64_RUST_STD") - } - (MacosAArch64, Tool::RustcDev) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_MACOS_AARCH64_RUSTC_DEV") - } - (MacosAArch64, Tool::LlvmTools) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_MACOS_AARCH64_LLVM_TOOLS_PREVIEW") - } - (MacosAArch64, Tool::Miri) => { - decode_hex_env!("ANNEAL_RUST_CHECKSUM_MACOS_AARCH64_MIRI_PREVIEW") - } - - (_, Tool::RustSrc) => decode_hex_env!("ANNEAL_RUST_CHECKSUM_RUST_SRC"), - - _ => { - unreachable!("unsupported tool combination for individual verification") + Self::Charon | Self::CharonDriver | Self::Aeneas => { + toolchain.aeneas_bin_dir().join(self.name()) } } } } +const AENEAS_DIR: &str = "aeneas"; +const AENEAS_BACKENDS_DIR: &str = "backends"; +const AENEAS_LEAN_DIR: &str = "lean"; +const BIN_DIR: &str = "bin"; +const LIB_DIR: &str = "lib"; +const LEAN_SYSROOT: &str = "lean"; +const RUST_SYSROOT: &str = "rust"; + pub struct Toolchain { - pub root: std::path::PathBuf, - // Holds the shared lock for the lifetime of the Toolchain object. - _lock: Option, + pub root: PathBuf, } impl Toolchain { - /// Resolves the toolchain manager and acquires a shared lock. - pub fn resolve() -> Result { - let home = if let Ok(dir) = std::env::var("ANNEAL_TOOLCHAIN_DIR") { - std::path::PathBuf::from(dir) - } else if std::env::var("__ZEROCOPY_LOCAL_DEV").is_ok() { - let base = std::env::var("CARGO_MANIFEST_DIR") - .map(std::path::PathBuf::from) - // Fall back to current directory if CARGO_MANIFEST_DIR is not set, - // which can happen if the binary is executed directly rather than - // via `cargo run`. - .unwrap_or_else(|_| std::env::current_dir().unwrap()); - base.join("target").join("anneal-home") - } else { - dirs::home_dir().ok_or_else(|| anyhow::anyhow!("Could not find home directory"))? - }; - let platform = Platform::detect()?; - let aeneas_hash = platform.expected_archive_hash(); - - // We produce a unique hash of the toolchain component versions to - // ensure that each combination of versions is installed into its own - // isolated directory. This allows multiple versions of Anneal to - // coexist on the same machine without colliding, and ensures that - // switching branches or updating Anneal will automatically point to - // the correct toolchain version. - // - // We hash the expected archive checksum rather than version tags. - // Checksums provide a stable, data-anchored identity for the toolchain - // components that cannot drift from the underlying binaries. - let mut hasher = Sha256::new(); - hasher.update(aeneas_hash); - // Hash the Rust toolchain tag to ensure that updating the Rust version - // results in a new, isolated toolchain directory. - hasher.update(env!("ANNEAL_RUST_TAG")); - let hash = format!("{:x}", hasher.finalize()); - let short_hash = &hash[..12]; - - // We include the host platform's target triple in the directory name. - // This ensures that toolchains for different architectures remain isolated - // if they are stored in a shared filesystem (e.g., a networked home directory). - let root = home.join(".anneal").join("toolchain").join(format!( - "{}-{}", - platform.triple(), - short_hash - )); - - // Acquire a shared lock to ensure the toolchain isn't modified while - // we use it. If the directory doesn't exist yet, we still acquire the - // lock on the path (which setup will also use). - let lock = DirLock::lock_shared(root.clone()) - .with_context(|| format!("Failed to acquire shared lock on {:?}", root))?; - - Ok(Self { root, _lock: Some(lock) }) + pub fn resolve() -> anyhow::Result { + let root = CONFIG + .resolve_installation_dir(location()) + .context("Toolchain not installed. Please run 'cargo anneal setup' first.")?; + Ok(Self { root }) } - /// Returns the bin directory for this toolchain. - pub fn bin_dir(&self) -> std::path::PathBuf { - self.root.clone() + pub fn bin_dir(&self) -> PathBuf { + self.aeneas_bin_dir() } - /// Returns the cache directory for this toolchain. - pub fn cache_dir(&self) -> std::path::PathBuf { + pub fn cache_dir(&self) -> PathBuf { self.root.join("lake-cache") } - /// Acquires an exclusive lock on the toolchain directory. - pub fn lock_exclusive(&self) -> Result { - DirLock::lock_exclusive(self.root.clone()) + pub fn aeneas_root(&self) -> PathBuf { + self.root.join(AENEAS_DIR) } - /// Returns a Command for the specified tool, prioritizing the managed - /// toolchain. - pub fn command(&self, tool: Tool) -> Command { - let bin_name = tool.name(); - let managed_path = self.bin_dir().join(bin_name); - - // If ANNEAL_USE_PATH_FOR_TOOLS is set, we ignore the managed toolchain - // and look for the tool in the system PATH. This is useful in tests - // to allow mocking tools via PATH shims, which would otherwise be - // bypassed by the managed toolchain's absolute paths. - if std::env::var("ANNEAL_USE_PATH_FOR_TOOLS").is_ok() { - Command::new(bin_name) - } else if tool == Tool::Lake { - // Lake is not part of the managed toolchain; it is assumed to be - // installed on the system (e.g., via elan). - Command::new(bin_name) - } else { - Command::new(managed_path) - } + pub fn aeneas_bin_dir(&self) -> PathBuf { + self.aeneas_root().join(BIN_DIR) } - /// Takes the shared lock from the toolchain, if it exists. - /// - /// This is used when we need to upgrade from a shared lock (held during - /// normal operation) to an exclusive lock (needed during `setup` or - /// repair). Because file locks cannot be atomically upgraded, we must - /// drop the shared lock before acquiring the exclusive one. - pub fn take_lock(&mut self) -> Option { - self._lock.take() + pub fn aeneas_lean_dir(&self) -> PathBuf { + self.aeneas_root().join(AENEAS_BACKENDS_DIR).join(AENEAS_LEAN_DIR) } -} -/// Calculates the SHA-256 hash of a file on disk. -fn calculate_file_hash(path: &Path) -> Result<[u8; 32]> { - let mut file = fs::File::open(path).context("Failed to open file for hashing")?; - let mut hasher = Sha256::new(); - let mut buffer = [0u8; 8192]; - loop { - let n = file.read(&mut buffer).context("Failed to read file for hashing")?; - if n == 0 { - break; - } - hasher.update(&buffer[..n]); + pub fn rust_sysroot(&self) -> PathBuf { + self.root.join(RUST_SYSROOT) } - Ok(hasher.finalize().into()) -} -/// Ensures that the file at the specified path is writable. -/// Some archives (like Nix-built ones) may contain read-only files, -/// which prevents us from repairing or corrupting them in tests. -fn make_writable(path: &Path) -> Result<()> { - if path.exists() { - let mut perms = fs::metadata(path)?.permissions(); - if perms.readonly() { - #[allow(clippy::permissions_set_readonly_false)] - perms.set_readonly(false); - fs::set_permissions(path, perms).context("Failed to set toolchain permissions")?; - } + pub fn rust_bin(&self) -> PathBuf { + self.rust_sysroot().join(BIN_DIR) } - Ok(()) -} -/// Recursively removes write permissions from all files and directories. -fn make_read_only_recursive(path: &Path) -> Result<()> { - if path.exists() { - for entry in WalkDir::new(path) { - let entry = entry.context("Failed to walk directory for read-only setup")?; - let p = entry.path(); - let mut perms = fs::metadata(p)?.permissions(); - perms.set_readonly(true); - fs::set_permissions(p, perms) - .with_context(|| format!("Failed to set read-only permissions on {:?}", p))?; - } + pub fn rust_lib(&self) -> PathBuf { + self.rust_sysroot().join(LIB_DIR) } - Ok(()) -} -/// Recursively restores write permissions for the owner. -fn make_writable_recursive(path: &Path) -> Result<()> { - if path.exists() { - for entry in WalkDir::new(path) { - let entry = entry.context("Failed to walk directory for writable setup")?; - let p = entry.path(); - let mut perms = fs::metadata(p)?.permissions(); - #[allow(clippy::permissions_set_readonly_false)] - perms.set_readonly(false); - fs::set_permissions(p, perms) - .with_context(|| format!("Failed to set writable permissions on {:?}", p))?; - } - } - Ok(()) -} - -/// Decodes a hexadecimal string into its byte representation. -const fn decode_hex(s: &str) -> Option<[u8; 32]> { - let bytes = s.as_bytes(); - if bytes.len() != 64 { - return None; - } - let mut res = [0u8; 32]; - let mut i = 0; - while i < 32 { - let (h, l) = (bytes[i * 2], bytes[i * 2 + 1]); - let h_nib = match decode_nibble(h) { - Some(n) => n, - None => return None, - }; - let l_nib = match decode_nibble(l) { - Some(n) => n, - None => return None, - }; - res[i] = (h_nib << 4) | l_nib; - i += 1; - } - Some(res) -} - -const fn decode_nibble(c: u8) -> Option { - match c { - b'0'..=b'9' => Some(c - b'0'), - b'a'..=b'f' => Some(c - b'a' + 10), - b'A'..=b'F' => Some(c - b'A' + 10), - _ => None, + pub fn lean_sysroot(&self) -> PathBuf { + self.root.join(LEAN_SYSROOT) } -} - -const AENEAS_TOOLS: &[Tool] = &[Tool::Aeneas, Tool::Charon, Tool::CharonDriver]; -const RUST_TOOLS: &[Tool] = - &[Tool::Rustc, Tool::RustStd, Tool::RustcDev, Tool::LlvmTools, Tool::Miri, Tool::RustSrc]; - -/// A generic function to extract a tar.gz archive, using a closure to map -/// paths from the archive to paths on disk. -fn extract_tar_gz(data: &[u8], target_dir: &Path, mut map_path: F) -> Result<()> -where - F: FnMut(&Path) -> Option, -{ - let tar = GzDecoder::new(data); - let mut archive = Archive::new(tar); - fs::create_dir_all(target_dir).context("Failed to create target directory")?; - - for entry in archive.entries().context("Failed to read archive entries")? { - let mut entry = entry.context("Failed to get archive entry")?; - let path = entry.path().context("Failed to get entry path")?; - - if let Some(target) = map_path(&path) { - if let Some(parent) = target.parent() { - fs::create_dir_all(parent).context("Failed to create parent directory")?; - } - entry.unpack(&target).context("Failed to unpack archive entry")?; - make_writable(&target)?; - } + pub fn lean_bin(&self) -> PathBuf { + self.lean_sysroot().join(BIN_DIR) } - Ok(()) -} - -/// Extracts a tar.gz archive to the target directory. -fn extract_artifact(data: &[u8], target_dir: &Path) -> Result<()> { - log::info!("Extracting to {:?}...", target_dir); - extract_tar_gz(data, target_dir, |path| Some(target_dir.join(path))) -} - -/// Performs a strict string replacement in a file. -/// -/// This function reads the file at the specified path, ensures that the target -/// string appears exactly once in the file, and replaces it with the -/// replacement string. -/// -/// We are strict about expecting exactly one occurrence to prevent accidental -/// mis-replacements or corrupted states when modifying files that we do not -/// fully parse (like Lean source files acting as configuration). -/// -/// # Errors -/// -/// Bails with an error if the target string is not found, or if it is found -/// more than once. -fn strict_replace_file_content(path: &Path, target: &str, replacement: &str) -> Result<()> { - let content = fs::read_to_string(path).context("Failed to read file for rewriting")?; - let count = content.matches(target).count(); - if count == 0 { - bail!("Target string not found in {:?}", path); - } - if count > 1 { - bail!("Multiple instances of target string found in {:?}", path); - } - let new_content = content.replace(target, replacement); - fs::write(path, new_content).context("Failed to write rewritten file")?; - Ok(()) -} - -/// Reads a Lake manifest file and extracts resolved package commits. -/// -/// This function parses the JSON manifest generated by Lake and returns a map -/// from package names to their resolved Git commit hashes. This allows us to -/// know the exact versions of dependencies resolved by Lake, even if we -/// subsequently override the repository URLs to be local. -fn read_manifest_revs(manifest_path: &Path) -> Result> { - let content = fs::read_to_string(manifest_path).context("Failed to read manifest")?; - let json: serde_json::Value = - serde_json::from_str(&content).context("Failed to parse manifest JSON")?; - let mut map = std::collections::HashMap::new(); - - if let Some(packages) = json.get("packages").and_then(|p| p.as_array()) { - for pkg in packages { - if let (Some(name), Some(rev)) = - (pkg.get("name").and_then(|n| n.as_str()), pkg.get("rev").and_then(|r| r.as_str())) - { - map.insert(name.to_string(), rev.to_string()); - } - } - } - Ok(map) -} - -/// Updates package URLs and requested revisions in a Lake manifest file. -/// -/// This function reads the generated manifest, iterates through all resolved -/// packages, and updates their URLs to point to the local `packages/` -/// directory using `file://` URLs based on the provided `base_path`. -/// -/// We update the manifest in addition to the `lakefile`s to prevent Lake from -/// detecting that the manifest is out of date and falling back to cloning the -/// dependencies from GitHub again. -/// -/// It also updates the `inputRev` field to match the resolved `rev` (commit -/// hash) to suppress warnings from Lake about the requested revision changing. -fn update_manifest_urls(manifest_path: &Path, base_path: &Path) -> Result<()> { - let content = fs::read_to_string(manifest_path).context("Failed to read manifest")?; - let mut json: serde_json::Value = - serde_json::from_str(&content).context("Failed to parse manifest JSON")?; - - if let Some(packages) = json.get_mut("packages").and_then(|p| p.as_array_mut()) { - for pkg in packages { - if let Some(name) = pkg.get("name").and_then(|n| n.as_str()) { - let local_url = format!("file://{}/packages/{}", base_path.display(), name); - pkg["url"] = serde_json::Value::String(local_url); - - // Also update inputRev to match the resolved rev to avoid warnings - if let Some(rev) = pkg.get("rev").cloned() { - pkg["inputRev"] = rev; - } - } - } - } - - let new_content = - serde_json::to_string_pretty(&json).context("Failed to serialize manifest")?; - fs::write(manifest_path, new_content).context("Failed to write manifest")?; - Ok(()) -} - -fn extract_rust_component(data: &[u8], target_dir: &Path, component_name: &str) -> Result<()> { - log::info!("Extracting component {} to {:?}...", component_name, target_dir); - extract_tar_gz(data, target_dir, |path| { - let mut components = path.components(); - components.next(); // skip top level (e.g. rustc-nightly-x86_64-unknown-linux-gnu) - components.next(); // skip component name (e.g. rustc) - - let rest = components.as_path(); - if rest.as_os_str().is_empty() { None } else { Some(target_dir.join(rest)) } - }) -} - -fn setup_rust_toolchain(toolchain: &Toolchain, platform: Platform, tmp_root: &Path) -> Result<()> { - let sysroot = tmp_root.join("rust"); - println!("Setting up Rust toolchain at {:?}...", sysroot); - - let base_url = std::env::var("ANNEAL_SETUP_RUST_BASE_URL").unwrap_or_else(|_| { - format!("https://static.rust-lang.org/dist/{}", env!("ANNEAL_RUST_DATE")) - }); - - let components = [ - ("rustc", Tool::Rustc), - ("rust-std", Tool::RustStd), - ("rustc-dev", Tool::RustcDev), - ("llvm-tools", Tool::LlvmTools), - ("miri", Tool::Miri), - ]; - - for (name, tool) in components { - let url = format!("{}/{}-nightly-{}.tar.gz", base_url, name, platform.triple()); - let expected_hash = platform.expected_bin_hash(tool); - - println!("Downloading and extracting {}...", name); - let data = download_artifact(&url, &expected_hash)?; - extract_rust_component(&data, &sysroot, name)?; - } - - // Handle rust-src separately as it is target-independent - let url = format!("{}/rust-src-nightly.tar.gz", base_url); - let expected_hash = platform.expected_bin_hash(Tool::RustSrc); - println!("Downloading and extracting rust-src..."); - let data = download_artifact(&url, &expected_hash)?; - extract_rust_component(&data, &sysroot, "rust-src")?; - - Ok(()) -} - -/// Ensures that `elan` (the Lean toolchain manager) is installed on the -/// system. If it is not found in the system `PATH`, it downloads the latest -/// release from GitHub and runs `elan-init` to install it for the current -/// user. It also attempts to add the `elan` bin directory to the current -/// process's `PATH` to ensure subsequent commands can find it immediately. -fn ensure_elan_installed() -> Result<()> { - println!("Checking for elan..."); - let status = Command::new("elan") - .arg("--version") - .stdout(std::process::Stdio::null()) - .stderr(std::process::Stdio::null()) - .status(); - - if status.is_ok() && status.unwrap().success() { - println!("elan is already installed."); - return Ok(()); - } - - println!("elan not found. Installing elan..."); - let platform = Platform::detect()?; - let arch = platform.triple(); - - let url = - format!("https://github.com/leanprover/elan/releases/latest/download/elan-{}.tar.gz", arch); - - println!("Downloading elan from {}...", url); - let response = reqwest::blocking::get(&url).context("Failed to download elan")?; - if !response.status().is_success() { - bail!("Failed to download elan: HTTP {}", response.status()); - } - let data = response.bytes().context("Failed to read elan response")?; - - let temp_dir = std::env::temp_dir(); - let elan_extract_dir = temp_dir.join("elan-extract-anneal"); - fs::create_dir_all(&elan_extract_dir).context("Failed to create elan extract dir")?; - - extract_artifact(&data, &elan_extract_dir)?; - - let elan_init_path = elan_extract_dir.join("elan-init"); - - let status = Command::new(&elan_init_path) - .args(["-y", "--default-toolchain", "none"]) - .status() - .context("Failed to run elan-init")?; - - let _ = fs::remove_dir_all(&elan_extract_dir); - - if !status.success() { - bail!("elan-init failed"); - } - - // Add elan to PATH for current process - let home = dirs::home_dir().ok_or_else(|| anyhow::anyhow!("Could not find home directory"))?; - let elan_bin = home.join(".elan").join("bin"); - if elan_bin.exists() { - let path = std::env::var_os("PATH").unwrap_or_default(); - let mut paths = std::env::split_paths(&path).collect::>(); - if !paths.contains(&elan_bin) { - paths.insert(0, elan_bin); - let new_path = std::env::join_paths(paths)?; - // SAFETY: This is a single-threaded setup context. - unsafe { - std::env::set_var("PATH", new_path); - } + pub fn command(&self, tool: Tool) -> Command { + if std::env::var("ANNEAL_USE_PATH_FOR_TOOLS").is_ok() { + Command::new(tool.name()) + } else { + Command::new(tool.path(self)) } } - - println!("elan installed successfully."); - Ok(()) } -/// Installs the pinned Lean toolchain required by Anneal using `elan`. -/// It checks the environment variable `ANNEAL_LEAN_TOOLCHAIN` to determine -/// which version to install. If the version is already listed in `elan -/// toolchain list`, it skips installation to save time. -fn install_lean_toolchain() -> Result<()> { - let version = env!("ANNEAL_LEAN_TOOLCHAIN"); - println!("Installing Lean toolchain {}...", version); - - // Check if already installed - let output = Command::new("elan") - .args(["toolchain", "list"]) - .output() - .context("Failed to run elan toolchain list")?; - - if output.status.success() { - let stdout = String::from_utf8_lossy(&output.stdout); - if stdout.lines().any(|line| line.contains(version)) { - println!("Lean toolchain {} is already installed.", version); - return Ok(()); - } - } - - let status = Command::new("elan") - .args(["toolchain", "install", version]) - .status() - .context("Failed to run elan toolchain install")?; - - if !status.success() { - bail!("Failed to install Lean toolchain"); - } +pub fn run_setup(args: SetupArgs) -> anyhow::Result<()> { + let local_archive = args + .local_archive + .or_else(|| std::env::var_os("ANNEAL_SETUP_LOCAL_ARCHIVE").map(PathBuf::from)); + let source = match local_archive { + Some(local_archive) => exocrate::Source::Local(local_archive), + None => exocrate::Source::Remote(remote_archive()), + }; - println!("Lean toolchain {} installed successfully.", version); + let installation_dir = CONFIG + .resolve_installation_dir_or_install(location(), source) + .context("failed to resolve-or-install dependencies")?; + log::info!("anneal toolchain is installed at {:?}", installation_dir); Ok(()) } -/// Pre-builds the Aeneas Lean library in the extracted toolchain directory. -/// -/// This prevents compiling the library from source when users verify their -/// projects, which is slow and disk-heavy. It first attempts to fetch -/// pre-compiled Mathlib artifacts using `lake exe cache get` to avoid -/// compiling Mathlib from source, and then runs `lake build`. -fn prebuild_aeneas_lean_library(lean_dir: &Path, cache_dir: &Path) -> Result<()> { - println!("Pre-building Aeneas Lean library at {:?}...", lean_dir); - - // Fetch Mathlib cache - println!("Fetching Mathlib cache..."); - let status = Command::new("lake") - .args(["exe", "cache", "get"]) - .env("LAKE_CACHE_DIR", cache_dir) - .env("LAKE_ARTIFACT_CACHE", "1") - .current_dir(lean_dir) - .status() - .context("Failed to run `lake exe cache get`")?; - - if !status.success() { - bail!("Failed to fetch Mathlib cache; refusing to build from scratch"); - } - - // Build the library - println!("Building Aeneas Lean library..."); - let status = Command::new("lake") - .arg("build") - .env("LAKE_CACHE_DIR", cache_dir) - .env("LAKE_ARTIFACT_CACHE", "1") - .current_dir(lean_dir) - .status() - .context("Failed to run `lake build`")?; - - if !status.success() { - bail!("Failed to build Aeneas Lean library"); +fn location() -> exocrate::Location { + if let Some(dir) = std::env::var_os("ANNEAL_TOOLCHAIN_DIR") { + exocrate::Location::Custom(PathBuf::from(dir)) + } else if std::env::var("__ZEROCOPY_LOCAL_DEV").is_ok() + || std::env::var("__ANNEAL_LOCAL_DEV").is_ok() + { + exocrate::Location::LocalDev + } else { + exocrate::Location::UserGlobal } - - println!("Successfully pre-built Aeneas Lean library."); - Ok(()) } -/// Checks whether the specified tools are installed and have valid hashes. -/// Returns `true` if all are valid, or `false` if any are missing or corrupt. - -/// Sets up the Anneal toolchain by downloading and extracting dependencies. -pub fn run_setup() -> Result<()> { - ensure_elan_installed()?; - install_lean_toolchain()?; - - let mut toolchain = Toolchain::resolve()?; - // Drop the shared lock acquired by resolve() so we can acquire an - // exclusive one. - drop(toolchain.take_lock()); - - // Acquire global lock to prevent concurrent installations or repairs. - // This ensures that two instances of Anneal don't try to download or - // modify the toolchain at the same time. - let _lock = toolchain.lock_exclusive()?; - let platform = Platform::detect()?; - - let parent_dir = toolchain.root.parent().unwrap(); - fs::create_dir_all(parent_dir).context("Failed to create toolchain parent directory")?; - // To ensure atomic installation, we perform all extraction and setup steps - // in a temporary directory within the same parent folder. This prevents - // leaving the toolchain in a partially-installed state if the process is - // interrupted. - let temp_dir = tempfile::Builder::new() - .prefix("anneal-toolchain-tmp-") - .tempdir_in(parent_dir) - .context("Failed to create temporary directory for setup")?; - let tmp_root = temp_dir.path(); - - setup_rust_toolchain(&toolchain, platform, tmp_root)?; - - let tag = env!("ANNEAL_AENEAS_TAG"); - - // Perform installation. Note that, because we validate SHA-256 - // checksums against values baked into the binary, allowing the user to - // override the download URL does not represent a security risk. - let base_url = std::env::var("ANNEAL_SETUP_AENEAS_BASE_URL") - .unwrap_or_else(|_| "https://github.com/AeneasVerif/aeneas/releases/download".to_string()); - - let url = format!( - "{}/{}/aeneas-{}.tar.gz", - base_url, - tag, - match platform { - Platform::LinuxX86_64 => "linux-x86_64", - Platform::LinuxAArch64 => "linux-aarch64", - Platform::MacosAArch64 => "macos-aarch64", - Platform::MacosX86_64 => "macos-x86_64", - } - ); - - let expected_archive_hash = platform.expected_archive_hash(); - - let data = download_artifact(&url, &expected_archive_hash)?; - - extract_artifact(&data, &tmp_root)?; - - let lean_dir = tmp_root.join("backends").join("lean"); - - // Initialize git repo in the extracted Lean directory - println!("Initializing git repository in {:?}...", lean_dir); - let status = Command::new("git") - .args(["init", "-b", "main", "-q"]) - .current_dir(&lean_dir) - .status() - .context("Failed to run `git init -b main`")?; - if !status.success() { - bail!("`git init -b main` failed"); - } - - let status = Command::new("git") - .args(["add", "."]) - .current_dir(&lean_dir) - .status() - .context("Failed to run `git add`")?; - if !status.success() { - bail!("`git add` failed"); - } - - let status = Command::new("git") - .args(["commit", "-m", "Initial commit from Anneal setup", "-q"]) - .env("GIT_AUTHOR_NAME", "Anneal") - .env("GIT_AUTHOR_EMAIL", "anneal@example.com") - .env("GIT_COMMITTER_NAME", "Anneal") - .env("GIT_COMMITTER_EMAIL", "anneal@example.com") - .current_dir(&lean_dir) - .status() - .context("Failed to run `git commit`")?; - if !status.success() { - bail!("`git commit` failed"); - } - - // Read the newly created HEAD commit hash and write it to a static - // file `aeneas-commit.txt` inside the package directory. - // - // This allows us to read the hash directly at runtime during - // `cargo-anneal verify` instead of executing `git rev-parse HEAD`. - // Spawning Git at runtime would fail inside Docker containers due to - // Git's "dubious ownership" security checks (caused by UID mapping - // mismatches between the build runner and the test runner). - let output = Command::new("git") - .args(["rev-parse", "HEAD"]) - .current_dir(&lean_dir) - .output() - .context("Failed to run `git rev-parse HEAD` during setup")?; - if !output.status.success() { - bail!("`git rev-parse HEAD` failed during setup"); - } - let commit_hash = - String::from_utf8(output.stdout).context("Failed to parse git output")?.trim().to_string(); - fs::write(lean_dir.join("aeneas-commit.txt"), commit_hash) - .context("Failed to write aeneas-commit.txt")?; - - // Run `lake update` to resolve dependencies and generate the manifest. - // We do this initially with remote URLs to let Lake resolve conflicts and - // record the specific commit hashes in `lake-manifest.json`. This also - // fetches the sources into `.lake/packages`. - println!("Resolving dependencies with `lake update` in {:?}...", lean_dir); - let status = Command::new("lake") - .arg("update") - .current_dir(&lean_dir) - .status() - .context("Failed to run `lake update`")?; - if !status.success() { - bail!("`lake update` failed"); - } - - // Move the resolved dependency directories to a centralized `packages` - // folder in the toolchain root. This acts as our local registry and - // ensures that they are preserved across builds and not treated as - // transient build artifacts by Lake in `backends/lean`. - let packages_dir = tmp_root.join("packages"); - fs::create_dir_all(&packages_dir).context("Failed to create packages directory")?; - - let lake_packages_dir = lean_dir.join(".lake").join("packages"); - if lake_packages_dir.exists() { - for entry in fs::read_dir(&lake_packages_dir).context("Failed to read .lake/packages")? { - let entry = entry.context("Failed to read directory entry")?; - let path = entry.path(); - if path.is_dir() { - let name = path.file_name().unwrap(); - let dest = packages_dir.join(name); - fs::rename(&path, &dest).context("Failed to move package")?; - } - } - } - - // We now perform the core rewriting of dependency configurations to point - // to the filesystem-local paths we just created using relative path dependencies. - let manifest_path = lean_dir.join("lake-manifest.json"); - - // Rewrite URLs in Aeneas lakefile.lean to use path dependency - let aeneas_lakefile = lean_dir.join("lakefile.lean"); - let target = "require mathlib from git\n \"https://github.com/leanprover-community/mathlib4.git\" @ \"v4.28.0-rc1\""; - let replacement = "require mathlib from \"../../packages/mathlib\""; - strict_replace_file_content(&aeneas_lakefile, target, replacement)?; - - // Rewrite URLs in Mathlib lakefile.lean to use relative path dependencies - let mathlib_lakefile = packages_dir.join("mathlib").join("lakefile.lean"); - let mathlib_replacements = [ - ( - "require \"leanprover-community\" / \"batteries\" @ git \"main\"", - "require batteries from \"../batteries\"", - ), - ("require \"leanprover-community\" / \"Qq\" @ git \"master\"", "require Qq from \"../Qq\""), - ( - "require \"leanprover-community\" / \"aesop\" @ git \"master\"", - "require aesop from \"../aesop\"", +fn remote_archive() -> exocrate::RemoteArchive { + match (std::env::consts::OS, std::env::consts::ARCH) { + ("linux", "x86_64") => remote_archive_for( + env!("ANNEAL_EXOCRATE_LINUX_X86_64_URL"), + env!("ANNEAL_EXOCRATE_LINUX_X86_64_SHA256"), ), - ( - "require \"leanprover-community\" / \"proofwidgets\" @ git \"v0.0.86\"", - "require proofwidgets from \"../proofwidgets\"", + ("macos", "x86_64") => remote_archive_for( + env!("ANNEAL_EXOCRATE_MACOS_X86_64_URL"), + env!("ANNEAL_EXOCRATE_MACOS_X86_64_SHA256"), ), - ( - "require \"leanprover-community\" / \"importGraph\" @ git \"main\"", - "require importGraph from \"../importGraph\"", + ("linux", "aarch64") => remote_archive_for( + env!("ANNEAL_EXOCRATE_LINUX_AARCH64_URL"), + env!("ANNEAL_EXOCRATE_LINUX_AARCH64_SHA256"), ), - ( - "require \"leanprover-community\" / \"LeanSearchClient\" @ git \"main\"", - "require LeanSearchClient from \"../LeanSearchClient\"", + ("macos", "aarch64") => remote_archive_for( + env!("ANNEAL_EXOCRATE_MACOS_AARCH64_URL"), + env!("ANNEAL_EXOCRATE_MACOS_AARCH64_SHA256"), ), - ( - "require \"leanprover-community\" / \"plausible\" @ git \"main\"", - "require plausible from \"../plausible\"", - ), - ]; - - for (target, replacement) in &mathlib_replacements { - strict_replace_file_content(&mathlib_lakefile, target, replacement)?; - } - - // Rewrite URLs in Aesop lakefile.toml to use relative path dependency - let aesop_lakefile = packages_dir.join("aesop").join("lakefile.toml"); - let target = "[[require]]\nname = \"batteries\"\ngit = \"https://github.com/leanprover-community/batteries\"\nrev = \"v4.28.0-rc1\""; - let replacement = "[[require]]\nname = \"batteries\"\npath = \"../batteries\""; - strict_replace_file_content(&aesop_lakefile, target, replacement)?; - - // Rewrite URLs in ImportGraph lakefile.toml to use relative path dependency - let import_graph_lakefile = packages_dir.join("importGraph").join("lakefile.toml"); - let target = "[[require]]\nname = \"Cli\"\nscope = \"leanprover\"\nrev = \"v4.28.0-rc1\""; - let replacement = "[[require]]\nname = \"Cli\"\npath = \"../Cli\""; - strict_replace_file_content(&import_graph_lakefile, target, replacement)?; - - // Delete the manifest lockfile (`lake-manifest.json`). This is - // critical because Aeneas is resolved as a local dependency package - // in user projects. If Aeneas preserves its own lockfile, Lake will - // read it at runtime and attempt to resolve nested dependencies - // (like `mathlib`) via Git, bypassing our local path overrides. - if manifest_path.exists() { - fs::remove_file(&manifest_path).context("Failed to delete manifest")?; - } - - prebuild_aeneas_lean_library(&lean_dir, &tmp_root.join("lake-cache"))?; - - // Pre-compile the `graph` tool in the `importGraph` dependency. This - // is required because the Aeneas library itself does not import - // `importGraph`, so a standard `lake build` skips it. - // - // We must pre-compile it during setup so that the `lake exe graph` - // tool is pre-built and available in the final read-only toolchain. - println!("Pre-compiling importGraph graph tool inside toolchain..."); - let status = Command::new("lake") - .args(["build", "importGraph/graph"]) - .current_dir(&lean_dir) - .status() - .context("Failed to build importGraph/graph in toolchain")?; - if !status.success() { - bail!("Failed to build importGraph/graph in toolchain"); - } - - // Delete manifest files from dependencies AFTER pre-building. This is - // critical because mathlib's cache fetching tool (run during - // prebuild) requires its own manifest to function. However, once the - // toolchain is installed, we must not have any manifest files in the - // dependencies, otherwise Lake will read them during user project - // verification and attempt to resolve nested dependencies via Git, - // bypassing our path overrides. - if packages_dir.exists() { - for entry in fs::read_dir(&packages_dir).context("Failed to read packages directory")? { - let entry = entry.context("Failed to read directory entry")?; - let path = entry.path(); - if path.is_dir() { - let dep_manifest = path.join("lake-manifest.json"); - if dep_manifest.exists() { - fs::remove_file(&dep_manifest) - .context("Failed to delete dependency manifest")?; - } - } - } - } - - // Lake records absolute paths in its `.trace` files (e.g., in the - // compiler command lines). Since we built the project in a temporary - // directory, these traces contain paths to that directory. - // - // To prevent Lake from invalidating these traces and rebuilding everything - // when the toolchain is used from its final location, we scan all - // `.trace` files in Aeneas and its dependencies, and replace the - // temporary path with the final installation path. - println!("Post-processing trace files to fix absolute paths..."); - let tmp_path_str = temp_dir.path().to_str().unwrap(); - let final_path_str = toolchain.root.to_str().unwrap(); - - // Process Aeneas build dir - crate::util::patch_trace_files( - &lean_dir.join(".lake").join("build"), - &[(tmp_path_str, final_path_str)], - )?; - - // Process dependencies build dirs - if packages_dir.exists() { - for entry in fs::read_dir(&packages_dir).context("Failed to read packages directory")? { - let entry = entry.context("Failed to read directory entry")?; - let path = entry.path(); - if path.is_dir() { - crate::util::patch_trace_files( - &path.join(".lake").join("build"), - &[(tmp_path_str, final_path_str)], - )?; - } - } + (os, arch) => panic!("unsupported platform: {os}-{arch}"), } +} - println!("Successfully installed toolchain v{tag}"); - - // Once installation is successful, we atomically swap the temporary - // directory into the final target location. If the target directory - // already exists (e.g., a re-installation attempt), we delete it first to - // allow the rename to succeed on Unix systems. - let tmp_path = temp_dir.into_path(); - if toolchain.root.exists() { - make_writable_recursive(&toolchain.root)?; - fs::remove_dir_all(&toolchain.root).context("Failed to remove old toolchain directory")?; +fn remote_archive_for(url: &'static str, sha256: &'static str) -> exocrate::RemoteArchive { + exocrate::RemoteArchive { + url, + sha256: decode_hex(sha256).expect("package.metadata.exocrate sha256 must be valid hex"), } - fs::rename(&tmp_path, &toolchain.root) - .context("Failed to rename temporary toolchain directory to target")?; - - // Create an empty .lock file during the setup phase while the - // toolchain directory is still writable. This ensures that future - // verify runs (which operate in read-only mode) can open the existing - // lock file to acquire shared file locks. - let lock_path = toolchain.root.join(".lock"); - fs::File::create(&lock_path).context("Failed to create lock file in setup")?; - - make_read_only_recursive(&toolchain.root)?; - - Ok(()) } -/// Downloads an artifact from the specified URL and verifies its SHA-256 hash. -fn download_artifact(url: &str, expected_hash: &[u8; 32]) -> Result> { - println!("Downloading: {}", url); - let mut response = reqwest::blocking::get(url).context("Failed to download artifact")?; - if !response.status().is_success() { - bail!("Failed to download artifact: HTTP {}", response.status()); +fn decode_hex(s: &str) -> Option<[u8; 32]> { + let bytes = s.as_bytes(); + if bytes.len() != 64 { + return None; } - - let mut data = Vec::new(); - response.read_to_end(&mut data).context("Failed to read artifact data")?; - - let mut hasher = Sha256::new(); - hasher.update(&data); - let actual_hash: [u8; 32] = hasher.finalize().into(); - - if actual_hash != *expected_hash { - bail!( - "Checksum mismatch for artifact! Expected {}, got {}", - format_hex(expected_hash), - format_hex(&actual_hash) - ); + let mut res = [0u8; 32]; + for i in 0..32 { + let h_nib = decode_nibble(bytes[i * 2])?; + let l_nib = decode_nibble(bytes[i * 2 + 1])?; + res[i] = (h_nib << 4) | l_nib; } - - Ok(data) + Some(res) } -fn format_hex(bytes: &[u8]) -> String { - let mut s = String::with_capacity(bytes.len() * 2); - for &b in bytes { - use std::fmt::Write; - write!(&mut s, "{:02x}", b).unwrap(); +fn decode_nibble(c: u8) -> Option { + match c { + b'0'..=b'9' => Some(c - b'0'), + b'a'..=b'f' => Some(c - b'a' + 10), + b'A'..=b'F' => Some(c - b'A' + 10), + _ => None, } - s } #[cfg(test)] @@ -1109,156 +193,21 @@ mod tests { use super::*; #[test] - fn test_platform_detection() { - let platform = Platform::detect().expect("Should detect current platform"); - // Verify that the detected platform triple matches the Rust target triple - // used to compile this test (roughly). - let triple = platform.triple(); - if cfg!(target_os = "linux") { - assert!(triple.contains("linux")); - } else if cfg!(target_os = "macos") { - assert!(triple.contains("apple-darwin")); - } - } - - #[test] - fn test_toolchain_resolve() { - let temp_dir = tempfile::tempdir().unwrap(); - // We must use an unsafe block because `set_var` is unsafe in recent Rust - // versions due to potential data races. We use it here to point the - // toolchain directory to our temporary directory, preventing the test - // from mutating the user's real home directory. - unsafe { - std::env::set_var("ANNEAL_TOOLCHAIN_DIR", temp_dir.path()); - } + fn tool_paths_use_omnibus_layout() { + let toolchain = Toolchain { root: PathBuf::from("/tmp/toolchain") }; - let toolchain = Toolchain::resolve().expect("Should resolve toolchain"); - - // Verify that the resolved toolchain root is located within the - // isolated temporary directory we specified. - assert!(toolchain.root.starts_with(temp_dir.path())); - - // Verify that the resolved path includes the platform target triple, - // ensuring platform-specific isolation. - let path_str = toolchain.root.to_str().unwrap(); - let platform = Platform::detect().unwrap(); - assert!(path_str.contains(platform.triple())); - } - - #[test] - fn test_locking() { - let temp = tempfile::tempdir().unwrap(); - let lock_path = temp.path().join(".lock"); - - // First lock - let lock1 = - DirLock::lock_exclusive(temp.path().to_path_buf()).expect("First lock should succeed"); - - // Try second lock in another thread (should block/fail if we used try_lock, but DirLock::lock blocks) - // To test non-blocking, we'd need another helper, but we can verify that the second lock - // succeeds after the first one is dropped. - let lock_path_clone = lock_path.clone(); - let handle = std::thread::spawn(move || { - let _lock2 = DirLock::lock_exclusive(lock_path_clone.parent().unwrap().to_path_buf()) - .expect("Second lock should succeed after first is dropped"); - }); - - std::thread::sleep(std::time::Duration::from_millis(100)); - drop(lock1); - handle.join().expect("Thread should finish"); - } - - #[test] - fn test_extraction() { - let temp = tempfile::tempdir().unwrap(); - let target = temp.path().join("extracted"); - - // Create a dummy tar.gz in memory - let mut enc = flate2::write::GzEncoder::new(Vec::new(), flate2::Compression::default()); - { - let mut tar = tar::Builder::new(&mut enc); - let mut header = tar::Header::new_gnu(); - header.set_path("hello.txt").unwrap(); - header.set_size(5); - #[cfg(unix)] - { - header.set_mode(0o755); - } - header.set_cksum(); - tar.append(&header, b"world" as &[u8]).unwrap(); - tar.finish().unwrap(); - } - let data = enc.finish().unwrap(); - - // Test normal extraction - extract_artifact(&data, &target).expect("Extraction should succeed"); - - let hello_path = target.join("hello.txt"); - assert!(hello_path.exists()); - assert_eq!(fs::read_to_string(&hello_path).unwrap(), "world"); - - // Test aeneas extraction (should extract everything) - let aeneas_target = temp.path().join("aeneas_extracted"); - let mut enc = flate2::write::GzEncoder::new(Vec::new(), flate2::Compression::default()); - { - let mut tar = tar::Builder::new(&mut enc); - - // Add aeneas binary - let mut header = tar::Header::new_gnu(); - header.set_path("aeneas").unwrap(); - header.set_size(6); - header.set_cksum(); - tar.append(&header, b"binary" as &[u8]).unwrap(); - - // Add backends directory - let mut header = tar::Header::new_gnu(); - header.set_path("backends/lean/test.lean").unwrap(); - header.set_size(4); - header.set_cksum(); - tar.append(&header, b"lean" as &[u8]).unwrap(); - - tar.finish().unwrap(); - } - let aeneas_data = enc.finish().unwrap(); - extract_artifact(&aeneas_data, &aeneas_target).expect("Aeneas extraction should succeed"); - - assert!(aeneas_target.join("aeneas").exists()); - assert!(aeneas_target.join("backends/lean/test.lean").exists()); - - #[cfg(unix)] - { - use std::os::unix::fs::PermissionsExt; - let metadata = fs::metadata(&hello_path).unwrap(); - assert!(metadata.permissions().mode() & 0o111 != 0, "Executable bit should be set"); - } - } - - #[test] - fn test_download() { - use std::{ - io::{Read, Write}, - net::TcpListener, - }; - - // Start a minimal mock HTTP server - let listener = TcpListener::bind("127.0.0.1:0").unwrap(); - let port = listener.local_addr().unwrap().port(); - let url = format!("http://127.0.0.1:{}", port); - - let handle = std::thread::spawn(move || { - let (mut stream, _) = listener.accept().unwrap(); - let mut buffer = [0; 1024]; - let _ = stream.read(&mut buffer).unwrap(); - - let response = "HTTP/1.1 200 OK\r\nContent-Length: 13\r\n\r\nMock Artifact"; - stream.write_all(response.as_bytes()).unwrap(); - }); - - let expected_hash_hex = "5fed9305f5a694b6b33ee9f783596ecf08ed89ea00c2960699ba8285e0d67c71"; // sha256 of "Mock Artifact" - let expected_hash = decode_hex(expected_hash_hex).expect("Mock hex should be valid"); - - let data = download_artifact(&url, &expected_hash).expect("Download should succeed"); - assert_eq!(data, b"Mock Artifact"); - handle.join().unwrap(); + assert_eq!(toolchain.bin_dir(), PathBuf::from("/tmp/toolchain/aeneas/bin")); + assert_eq!( + toolchain.aeneas_lean_dir(), + PathBuf::from("/tmp/toolchain/aeneas/backends/lean") + ); + assert_eq!( + Tool::Charon.path(&toolchain), + PathBuf::from("/tmp/toolchain/aeneas/bin/charon") + ); + assert_eq!( + Tool::Aeneas.path(&toolchain), + PathBuf::from("/tmp/toolchain/aeneas/bin/aeneas") + ); } } diff --git a/anneal/src/util.rs b/anneal/src/util.rs index 4d1dcefa8c..fe085b37dc 100644 --- a/anneal/src/util.rs +++ b/anneal/src/util.rs @@ -1,8 +1,7 @@ -use std::path::{Path, PathBuf}; +use std::path::PathBuf; use anyhow::{Context, Result}; use fs2::FileExt; -use walkdir::WalkDir; /// Represents an active, exclusive lock on a directory. /// @@ -30,17 +29,6 @@ impl DirLock { Ok(Self { path, _file: file }) } - /// Acquires a shared lock on the specified directory. - /// - /// Multiple processes can hold shared locks simultaneously, but an - /// exclusive lock will block until all shared locks are released. - pub fn lock_shared(path: PathBuf) -> Result { - let file = Self::open_lock_file(&path)?; - file.lock_shared() - .with_context(|| format!("Failed to acquire shared lock on {:?}", path))?; - Ok(Self { path, _file: file }) - } - fn open_lock_file(path: &std::path::Path) -> Result { let lock_path = path.join(".lock"); @@ -69,28 +57,3 @@ impl DirLock { } } } - -/// Walks a directory recursively and replaces string patterns inside `.trace` -/// files. This is used to patch non-portable paths generated by Lake. -pub fn patch_trace_files(dir: &Path, replacements: &[(&str, &str)]) -> Result<()> { - if dir.exists() { - let walker = WalkDir::new(dir).into_iter(); - for entry in walker { - let entry = entry.context("Failed to walk directory for trace patching")?; - let path = entry.path(); - if path.is_file() && path.extension().map_or(false, |ext| ext == "trace") { - let content = std::fs::read_to_string(path) - .with_context(|| format!("Failed to read trace file {:?}", path))?; - let mut new_content = content.clone(); - for (from, to) in replacements { - new_content = new_content.replace(from, to); - } - if new_content != content { - std::fs::write(path, new_content) - .with_context(|| format!("Failed to write trace file {:?}", path))?; - } - } - } - } - Ok(()) -} diff --git a/anneal/tests/fixtures/allow_sorry_fallbacks/expected.stderr b/anneal/tests/fixtures/allow_sorry_fallbacks/expected.stderr index 6daf6e5407..0d72958f2c 100644 --- a/anneal/tests/fixtures/allow_sorry_fallbacks/expected.stderr +++ b/anneal/tests/fixtures/allow_sorry_fallbacks/expected.stderr @@ -40,19 +40,15 @@ 43 │ /// proof: ╰──── - × invalid {...} notation, structure type expected - │ Post ret - ╭─[[PROJECT_ROOT]/src/lib.rs:44:7] - 43 │ /// proof: - 44 │ ╭─▶ /// -- A deliberately broken explicit proof should NOT emit "declaration uses sorry" - 45 │ │ /// -- but instead natively fail on the syntax error "unknown tactic". - 46 │ │ /// exact { - 47 │ │ /// invalid_tactic - 48 │ ├─▶ /// } - · ╰──── here - 49 │ /// ``` - ╰──── +[External Error] generated/NamedBoundsValidationFailuresNamedBoundsValidationFailures22b4e0ecfe54227c/NamedBoundsValidationFailuresNamedBoundsValidationFailures22b4e0ecfe54227c.lean: Function expected at + Post +but this term has type + ?m.1 + +Note: Expected a function because this term is being applied to the argument + ret_ +Hint: The identifier `Post` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement. × Tactic `rfl` failed: The left-hand side │ true == false │ is not definitionally equal to the right-hand side diff --git a/anneal/tests/fixtures/cfg_blind_spot/expected.stderr b/anneal/tests/fixtures/cfg_blind_spot/expected.stderr index 9eef0ffa38..bedc7cba44 100644 --- a/anneal/tests/fixtures/cfg_blind_spot/expected.stderr +++ b/anneal/tests/fixtures/cfg_blind_spot/expected.stderr @@ -1,9 +1,9 @@ Compiling cfg_blind_spot v0.1.0 ([PROJECT_ROOT]) -warning: when processing starting pattern `crate::ghost::hidden`: path `crate::ghost` does not correspond to any item +warning: failed to resolve item path `crate::ghost::hidden`: path `crate::ghost` does not correspond to any item -thread 'rustc' () panicked at src/errors.rs:278:13: -when processing starting pattern `crate::ghost::hidden`: path `crate::ghost` does not correspond to any item +thread 'rustc' () panicked at src/errors.rs:261:13: +failed to resolve item path `crate::ghost::hidden`: path `crate::ghost` does not correspond to any item note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace ERROR Compilation panicked error: could not compile `cfg_blind_spot` (lib) diff --git a/anneal/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/expected.stderr b/anneal/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/expected.stderr index 54e5b506eb..2005837595 100644 --- a/anneal/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/expected.stderr +++ b/anneal/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/expected.stderr @@ -1,9 +1,9 @@ Compiling test_7_1_phantom_fn v0.1.0 ([PROJECT_ROOT]) -warning: when processing starting pattern `crate::windows_only`: path `crate::windows_only` does not correspond to any item +warning: failed to resolve item path `crate::windows_only`: path `crate::windows_only` does not correspond to any item -thread 'rustc' () panicked at src/errors.rs:278:13: -when processing starting pattern `crate::windows_only`: path `crate::windows_only` does not correspond to any item +thread 'rustc' () panicked at src/errors.rs:261:13: +failed to resolve item path `crate::windows_only`: path `crate::windows_only` does not correspond to any item note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace ERROR Compilation panicked error: could not compile `test_7_1_phantom_fn` (lib) diff --git a/anneal/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/expected.stderr b/anneal/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/expected.stderr index 35f4324220..c31f163856 100644 --- a/anneal/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/expected.stderr +++ b/anneal/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/expected.stderr @@ -1,13 +1,13 @@ Compiling test_7_3_ghost_spec v0.1.0 ([PROJECT_ROOT]) -warning: when processing starting pattern `crate::windows_only`: path `crate::windows_only` does not correspond to any item +warning: failed to resolve item path `crate::windows_only`: path `crate::windows_only` does not correspond to any item --> src/lib.rs:18:36 | 18 | pub fn linux_only() -> u32 { 100 } | ^ -thread 'rustc' () panicked at src/errors.rs:278:13: -when processing starting pattern `crate::windows_only`: path `crate::windows_only` does not correspond to any item +thread 'rustc' () panicked at src/errors.rs:261:13: +failed to resolve item path `crate::windows_only`: path `crate::windows_only` does not correspond to any item note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace ERROR Compilation panicked error: could not compile `test_7_3_ghost_spec` (lib) diff --git a/anneal/tests/fixtures/edge_cases_charon/test_8_2_unions/expected.stderr b/anneal/tests/fixtures/edge_cases_charon/test_8_2_unions/expected.stderr index 74161b7df2..2a2b6ed630 100644 --- a/anneal/tests/fixtures/edge_cases_charon/test_8_2_unions/expected.stderr +++ b/anneal/tests/fixtures/edge_cases_charon/test_8_2_unions/expected.stderr @@ -5,17 +5,17 @@ Uncaught exception: (Failure "unions are not supported\ \nSource: 'src/lib.rs', lines 2:0-5:1\ - \nCompiler source: llbc/TypesAnalysis.ml, line 503") + \nCompiler source: llbc/TypesAnalysis.ml, line 514") Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 120, characters 4-23 Called from Aeneas__Errors.craise in file "Errors.ml" (inlined), line 126, characters 2-43 -Called from Aeneas__TypesAnalysis.analyze_type_decl in file "llbc/TypesAnalysis.ml", line 503, characters 19-74 +Called from Aeneas__TypesAnalysis.analyze_type_decl in file "llbc/TypesAnalysis.ml", line 514, characters 19-74 Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 -Called from Aeneas__TypesAnalysis.analyze_type_declaration_group.analyze in file "llbc/TypesAnalysis.ml", lines 554-556, characters 6-23 +Called from Aeneas__TypesAnalysis.analyze_type_declaration_group.analyze in file "llbc/TypesAnalysis.ml", lines 565-567, characters 6-23 Called from Aeneas__Interp.analyze_type_declarations.(fun) in file "interp/Interp.ml", line 31, characters 10-62 Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 -Called from Aeneas__Interp.compute_contexts in file "interp/Interp.ml", line 153, characters 19-66 -Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 290, characters 18-40 -Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 2100, characters 31-71 -Called from Dune__exe__Main in file "Main.ml", lines 726-727, characters 8-37 +Called from Aeneas__Interp.compute_contexts in file "interp/Interp.ml", line 149, characters 19-66 +Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 313, characters 18-40 +Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 2131, characters 31-71 +Called from Dune__exe__Main in file "Main.ml", lines 738-739, characters 8-37 diff --git a/anneal/tests/fixtures/expand_output/expected-aeneas.stdout b/anneal/tests/fixtures/expand_output/expected-aeneas.stdout index ce8ea8ce62..35f4c97f22 100644 --- a/anneal/tests/fixtures/expand_output/expected-aeneas.stdout +++ b/anneal/tests/fixtures/expand_output/expected-aeneas.stdout @@ -1,3 +1,4 @@ +Materializing packages by copying from toolchain... === Lean expansion for: expand_output === --- Aeneas --- -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS @@ -11,6 +12,9 @@ set_option linter.unusedVariables false /- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ set_option maxHeartbeats 1000000 +/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/ +set_option maxRecDepth 2048 + namespace expand_output end expand_output @@ -29,6 +33,9 @@ set_option linter.unusedVariables false /- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ set_option maxHeartbeats 1000000 +/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/ +set_option maxRecDepth 2048 + namespace expand_output /-- [expand_output::foo]: diff --git a/anneal/tests/fixtures/expand_output/expected-all.stdout b/anneal/tests/fixtures/expand_output/expected-all.stdout index 257ce4c9f2..6610b1a7cb 100644 --- a/anneal/tests/fixtures/expand_output/expected-all.stdout +++ b/anneal/tests/fixtures/expand_output/expected-all.stdout @@ -1,3 +1,4 @@ +Materializing packages by copying from toolchain... === Lean expansion for: expand_output === --- Aeneas --- -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS @@ -11,6 +12,9 @@ set_option linter.unusedVariables false /- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ set_option maxHeartbeats 1000000 +/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/ +set_option maxRecDepth 2048 + namespace expand_output end expand_output @@ -29,6 +33,9 @@ set_option linter.unusedVariables false /- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ set_option maxHeartbeats 1000000 +/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/ +set_option maxRecDepth 2048 + namespace expand_output /-- [expand_output::foo]: diff --git a/anneal/tests/fixtures/expand_output/expected-anneal.stdout b/anneal/tests/fixtures/expand_output/expected-anneal.stdout index 459890bdeb..25391c9fa2 100644 --- a/anneal/tests/fixtures/expand_output/expected-anneal.stdout +++ b/anneal/tests/fixtures/expand_output/expected-anneal.stdout @@ -1,3 +1,4 @@ +Materializing packages by copying from toolchain... === Lean expansion for: expand_output === --- Anneal --- -- This file is automatically generated by Anneal. diff --git a/anneal/tests/fixtures/extern_never_verified/out.txt b/anneal/tests/fixtures/extern_never_verified/out.txt index 534f1fb8c0..af40cb8a87 100644 --- a/anneal/tests/fixtures/extern_never_verified/out.txt +++ b/anneal/tests/fixtures/extern_never_verified/out.txt @@ -1,3 +1,4 @@ +Materializing packages by copying from toolchain... === Lean expansion for: extern_never_verified === --- Aeneas --- -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS @@ -11,6 +12,9 @@ set_option linter.unusedVariables false /- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ set_option maxHeartbeats 1000000 +/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/ +set_option maxRecDepth 2048 + namespace extern_never_verified /-- [extern_never_verified::S] @@ -42,6 +46,9 @@ set_option linter.unusedVariables false /- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ set_option maxHeartbeats 1000000 +/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/ +set_option maxRecDepth 2048 + /- You can remove the following line by using the CLI option `-all-computable`: -/ noncomputable section @@ -91,6 +98,9 @@ set_option linter.unusedVariables false /- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ set_option maxHeartbeats 1000000 + +/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/ +set_option maxRecDepth 2048 open extern_never_verified /-- [extern_never_verified::a::b::foo]: diff --git a/anneal/tests/fixtures/external_path_dependency/anneal.toml b/anneal/tests/fixtures/external_path_dependency/anneal.toml new file mode 100644 index 0000000000..6178ceddef --- /dev/null +++ b/anneal/tests/fixtures/external_path_dependency/anneal.toml @@ -0,0 +1,11 @@ +description = """ +Purpose: Allows build-only local path dependencies outside the selected workspace root. +Behavior: Runs from a nested workspace whose selected package depends on a sibling crate +outside that workspace. The sibling crate should not be rejected merely because Cargo +metadata includes it; Anneal only scans the selected package. +""" + +[test] +args = ["verify"] +cwd = "workspace" +expected_status = "success" diff --git a/anneal/tests/fixtures/external_path_dependency/source/external_dep/Cargo.toml b/anneal/tests/fixtures/external_path_dependency/source/external_dep/Cargo.toml new file mode 100644 index 0000000000..886f5f973f --- /dev/null +++ b/anneal/tests/fixtures/external_path_dependency/source/external_dep/Cargo.toml @@ -0,0 +1,4 @@ +[package] +name = "external_dep" +version = "0.1.0" +edition = "2021" diff --git a/anneal/tests/fixtures/external_path_dependency/source/external_dep/src/lib.rs b/anneal/tests/fixtures/external_path_dependency/source/external_dep/src/lib.rs new file mode 100644 index 0000000000..1e312bbd2a --- /dev/null +++ b/anneal/tests/fixtures/external_path_dependency/source/external_dep/src/lib.rs @@ -0,0 +1,3 @@ +pub fn value() -> u32 { + 7 +} diff --git a/anneal/tests/fixtures/external_path_dependency/source/workspace/Cargo.toml b/anneal/tests/fixtures/external_path_dependency/source/workspace/Cargo.toml new file mode 100644 index 0000000000..9d2182e90f --- /dev/null +++ b/anneal/tests/fixtures/external_path_dependency/source/workspace/Cargo.toml @@ -0,0 +1,3 @@ +[workspace] +members = ["app"] +resolver = "2" diff --git a/anneal/tests/fixtures/external_path_dependency/source/workspace/app/Cargo.toml b/anneal/tests/fixtures/external_path_dependency/source/workspace/app/Cargo.toml new file mode 100644 index 0000000000..d5d7932518 --- /dev/null +++ b/anneal/tests/fixtures/external_path_dependency/source/workspace/app/Cargo.toml @@ -0,0 +1,7 @@ +[package] +name = "app" +version = "0.1.0" +edition = "2021" + +[dependencies] +external_dep = { path = "../../external_dep" } diff --git a/anneal/tests/fixtures/external_path_dependency/source/workspace/app/src/lib.rs b/anneal/tests/fixtures/external_path_dependency/source/workspace/app/src/lib.rs new file mode 100644 index 0000000000..82fb3c946e --- /dev/null +++ b/anneal/tests/fixtures/external_path_dependency/source/workspace/app/src/lib.rs @@ -0,0 +1,3 @@ +pub fn app_value() -> u32 { + external_dep::value() +} diff --git a/anneal/tests/fixtures/generate_output/expected-generate.stdout b/anneal/tests/fixtures/generate_output/expected-generate.stdout index 974497f52c..3cba225c7f 100644 --- a/anneal/tests/fixtures/generate_output/expected-generate.stdout +++ b/anneal/tests/fixtures/generate_output/expected-generate.stdout @@ -1,8 +1,6 @@ -Writing modified manifest to generated workspace... Materializing packages by copying from toolchain... -Post-processing traces in the clone... Lean workspace generated at: [PROJECT_ROOT]/target/anneal/anneal_test_target/lean To manually build and experiment: 1. cd [PROJECT_ROOT]/target/anneal/anneal_test_target/lean - 2. LAKE_CACHE_DIR=[CACHE_ROOT]/lake-cache lake build + 2. LAKE_CACHE_DIR=[CACHE_ROOT]/lake-cache [CACHE_ROOT]/lean/bin/lake --keep-toolchain build diff --git a/anneal/tests/fixtures/named_bounds_lean_failures/expected.stderr b/anneal/tests/fixtures/named_bounds_lean_failures/expected.stderr index 80199cf84d..176c101252 100644 --- a/anneal/tests/fixtures/named_bounds_lean_failures/expected.stderr +++ b/anneal/tests/fixtures/named_bounds_lean_failures/expected.stderr @@ -1,129 +1,19 @@ - ⚠ unused variable: `x` - ╭─[[PROJECT_ROOT]/src/lib.rs:14:35] - 13 │ /// ``` - 14 │ fn fail_anon_ensures_verification(x: u32) -> u32 { - · ┬ - · ╰── - 15 │ 1 - ╰──── - help: if this is intentional, prefix it with an underscore - - ⚠ unused variable: `x` - ╭─[[PROJECT_ROOT]/src/lib.rs:35:31] - 34 │ /// ``` - 35 │ fn fail_is_valid_verification(x: Positive) -> Positive { - · ┬ - · ╰── - 36 │ Positive { val: 0 } - ╰──── - help: if this is intentional, prefix it with an underscore - - ⚠ unused variable: `ret` - ╭─[[PROJECT_ROOT]/src/lib.rs:90:28] - 89 │ /// ``` - 90 │ fn fail_argument_named_ret(ret: u32) -> u32 { - · ─┬─ - · ╰── - 91 │ 0 - ╰──── - help: if this is intentional, prefix it with an underscore - - ⚠ function `fail_anon_ensures_verification` is never used - ╭─[[PROJECT_ROOT]/src/lib.rs:14:4] - 13 │ /// ``` - 14 │ fn fail_anon_ensures_verification(x: u32) -> u32 { - · ───────────────┬────────────── - · ╰── - 15 │ 1 - ╰──── - - ⚠ function `fail_is_valid_verification` is never used - ╭─[[PROJECT_ROOT]/src/lib.rs:35:4] - 34 │ /// ``` - 35 │ fn fail_is_valid_verification(x: Positive) -> Positive { - · ─────────────┬──────────── - · ╰── - 36 │ Positive { val: 0 } - ╰──── - - ⚠ function `fail_proof_context_tactic_failure` is never used - ╭─[[PROJECT_ROOT]/src/lib.rs:51:4] - 50 │ /// ``` - 51 │ fn fail_proof_context_tactic_failure(x: u32) -> u32 { - · ────────────────┬──────────────── - · ╰── - 52 │ x - ╰──── - - ⚠ function `fail_lean_keyword_proof` is never used - ╭─[[PROJECT_ROOT]/src/lib.rs:65:4] - 64 │ /// ``` - 65 │ fn fail_lean_keyword_proof(x: u32) -> u32 { - · ───────────┬─────────── - · ╰── - 66 │ x - ╰──── - - ⚠ function `fail_ret_in_requires` is never used - ╭─[[PROJECT_ROOT]/src/lib.rs:76:11] - 75 │ /// ``` - 76 │ unsafe fn fail_ret_in_requires(x: u32) -> u32 { - · ──────────┬───────── - · ╰── - 77 │ x - ╰──── - - ⚠ function `fail_argument_named_ret` is never used - ╭─[[PROJECT_ROOT]/src/lib.rs:90:4] - 89 │ /// ``` - 90 │ fn fail_argument_named_ret(ret: u32) -> u32 { - · ───────────┬─────────── - · ╰── - 91 │ 0 - ╰──── - - ⚠ function `fail_unknown_variable_in_requires` is never used - ╭─[[PROJECT_ROOT]/src/lib.rs:99:11] - 98 │ /// ``` - 99 │ unsafe fn fail_unknown_variable_in_requires(x: u32) -> u32 { - · ────────────────┬──────────────── - · ╰── - 100 │ x - ╰──── - - ⚠ function `fail_missing_named_proof` is never used - ╭─[[PROJECT_ROOT]/src/lib.rs:112:4] - 111 │ /// ``` - 112 │ fn fail_missing_named_proof(x: u32) -> u32 { - · ────────────┬─────────── - · ╰── - 113 │ x - ╰──── - - ⚠ function `main` is never used - ╭─[[PROJECT_ROOT]/src/lib.rs:116:4] - 115 │ - 116 │ fn main() {} - · ──┬─ - · ╰── - ╰──── - × simp_all made no progress - ╭─[[PROJECT_ROOT]/src/lib.rs:12:7] - 11 │ /// proof: - 12 │ /// simp_all + ╭─[[PROJECT_ROOT]/src/lib.rs:14:7] + 13 │ /// proof: + 14 │ /// simp_all · ────┬─── · ╰── here - 13 │ /// ``` + 15 │ /// ``` ╰──── ⚠ declaration uses `sorry` - ╭─[[PROJECT_ROOT]/src/lib.rs:35:4] - 34 │ /// ``` - 35 │ fn fail_is_valid_verification(x: Positive) -> Positive { + ╭─[[PROJECT_ROOT]/src/lib.rs:37:4] + 36 │ /// ``` + 37 │ fn fail_is_valid_verification(x: Positive) -> Positive { · ──┬─ · ╰── here - 36 │ Positive { val: 0 } + 38 │ Positive { val: 0 } ╰──── × unsolved goals @@ -131,21 +21,21 @@ │ h_returns : fail_proof_context_tactic_failure x = ok ret │ h_x_is_valid : Anneal.IsValid.isValid x │ ⊢ False - ╭─[[PROJECT_ROOT]/src/lib.rs:46:24] - 45 │ /// proof context: - 46 │ /// have h: false := by simp + ╭─[[PROJECT_ROOT]/src/lib.rs:48:24] + 47 │ /// proof context: + 48 │ /// have h: false := by simp · ───┬─── · ╰── here - 47 │ /// proof context: + 49 │ /// proof context: ╰──── × simp_all made no progress - ╭─[[PROJECT_ROOT]/src/lib.rs:88:7] - 87 │ /// proof (ens): - 88 │ /// simp_all + ╭─[[PROJECT_ROOT]/src/lib.rs:90:7] + 89 │ /// proof (ens): + 90 │ /// simp_all · ────┬─── · ╰── here - 89 │ /// ``` + 91 │ /// ``` ╰──── Error: Lean verification failed. Consider running `cargo anneal generate`, iterating on generated `.lean` files, and copying results back to `.rs` files. diff --git a/anneal/tests/fixtures/named_bounds_lean_failures/source/src/lib.rs b/anneal/tests/fixtures/named_bounds_lean_failures/source/src/lib.rs index b6a55f5bef..7e5bd81ad4 100644 --- a/anneal/tests/fixtures/named_bounds_lean_failures/source/src/lib.rs +++ b/anneal/tests/fixtures/named_bounds_lean_failures/source/src/lib.rs @@ -1,3 +1,5 @@ +#![allow(dead_code, unused_variables)] + /// This file contains failure cases for the Anneal named bounds feature. /// We test both validation errors (rust-level parsing and validation) /// and verification errors (Lean-level theorem failures). diff --git a/anneal/tests/fixtures/size_of_align_of/source/src/lib.rs b/anneal/tests/fixtures/size_of_align_of/source/src/lib.rs index b1bdda17a4..1d79ff1be7 100644 --- a/anneal/tests/fixtures/size_of_align_of/source/src/lib.rs +++ b/anneal/tests/fixtures/size_of_align_of/source/src/lib.rs @@ -12,7 +12,7 @@ /// unfold get_size_of_empty_tuple at h_returns /// simp_all /// subst h_returns -/// simp_all +/// simp [Anneal.HasStaticLayout.layout, Anneal.HasStaticSpecLayout.layout] /// proof (h_valid): /// unfold get_size_of_empty_tuple at h_returns /// simp_all @@ -37,7 +37,7 @@ pub fn get_size_of_empty_tuple() -> usize { /// unfold get_align_of_empty_tuple at h_returns /// simp_all /// subst h_returns -/// simp_all +/// simp [Anneal.HasStaticLayout.layout, Anneal.HasStaticSpecLayout.layout] /// proof (h_valid): /// unfold get_align_of_empty_tuple at h_returns /// simp_all diff --git a/anneal/tests/fixtures/split_artifact/expected.stderr b/anneal/tests/fixtures/split_artifact/expected.stderr index 34a3be411c..eef1af957a 100644 --- a/anneal/tests/fixtures/split_artifact/expected.stderr +++ b/anneal/tests/fixtures/split_artifact/expected.stderr @@ -7,11 +7,11 @@ ╰──── Compiling split v0.1.0 ([PROJECT_ROOT]) -warning: when processing starting pattern `crate::main`: path `crate::main` does not correspond to any item +warning: failed to resolve item path `crate::main`: path `crate::main` does not correspond to any item -thread 'rustc' () panicked at src/errors.rs:278:13: -when processing starting pattern `crate::main`: path `crate::main` does not correspond to any item +thread 'rustc' () panicked at src/errors.rs:261:13: +failed to resolve item path `crate::main`: path `crate::main` does not correspond to any item note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace ERROR Compilation panicked error: could not compile `split` (lib) diff --git a/anneal/tests/fixtures/target_selection/expected.stderr b/anneal/tests/fixtures/target_selection/expected.stderr index c1b216c8a4..a39640c126 100644 --- a/anneal/tests/fixtures/target_selection/expected.stderr +++ b/anneal/tests/fixtures/target_selection/expected.stderr @@ -1,9 +1,9 @@ Compiling selector v0.1.0 ([PROJECT_ROOT]) -warning: when processing starting pattern `crate::_anneal_dummy`: path `crate::_anneal_dummy` does not correspond to any item +warning: failed to resolve item path `crate::_anneal_dummy`: path `crate::_anneal_dummy` does not correspond to any item -thread 'rustc' () panicked at src/errors.rs:278:13: -when processing starting pattern `crate::_anneal_dummy`: path `crate::_anneal_dummy` does not correspond to any item +thread 'rustc' () panicked at src/errors.rs:261:13: +failed to resolve item path `crate::_anneal_dummy`: path `crate::_anneal_dummy` does not correspond to any item note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace ERROR Compilation panicked error: could not compile `selector` (lib) diff --git a/anneal/tests/fixtures/unions/expected.stderr b/anneal/tests/fixtures/unions/expected.stderr index 61a0167d8e..cd365777ec 100644 --- a/anneal/tests/fixtures/unions/expected.stderr +++ b/anneal/tests/fixtures/unions/expected.stderr @@ -5,17 +5,17 @@ Uncaught exception: (Failure "unions are not supported\ \nSource: 'src/lib.rs', lines 2:0-5:1\ - \nCompiler source: llbc/TypesAnalysis.ml, line 503") + \nCompiler source: llbc/TypesAnalysis.ml, line 514") Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 120, characters 4-23 Called from Aeneas__Errors.craise in file "Errors.ml" (inlined), line 126, characters 2-43 -Called from Aeneas__TypesAnalysis.analyze_type_decl in file "llbc/TypesAnalysis.ml", line 503, characters 19-74 +Called from Aeneas__TypesAnalysis.analyze_type_decl in file "llbc/TypesAnalysis.ml", line 514, characters 19-74 Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 -Called from Aeneas__TypesAnalysis.analyze_type_declaration_group.analyze in file "llbc/TypesAnalysis.ml", lines 554-556, characters 6-23 +Called from Aeneas__TypesAnalysis.analyze_type_declaration_group.analyze in file "llbc/TypesAnalysis.ml", lines 565-567, characters 6-23 Called from Aeneas__Interp.analyze_type_declarations.(fun) in file "interp/Interp.ml", line 31, characters 10-62 Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 -Called from Aeneas__Interp.compute_contexts in file "interp/Interp.ml", line 153, characters 19-66 -Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 290, characters 18-40 -Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 2100, characters 31-71 -Called from Dune__exe__Main in file "Main.ml", lines 726-727, characters 8-37 +Called from Aeneas__Interp.compute_contexts in file "interp/Interp.ml", line 149, characters 19-66 +Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 313, characters 18-40 +Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 2131, characters 31-71 +Called from Dune__exe__Main in file "Main.ml", lines 738-739, characters 8-37 diff --git a/anneal/tests/fixtures/weird_functions/expected.stderr b/anneal/tests/fixtures/weird_functions/expected.stderr index 9c25ba9cda..4e22d5c3b6 100644 --- a/anneal/tests/fixtures/weird_functions/expected.stderr +++ b/anneal/tests/fixtures/weird_functions/expected.stderr @@ -6,7 +6,7 @@ warning: Coroutine types are not supported yet | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -thread 'rustc' () panicked at src/errors.rs:278:13: +thread 'rustc' () panicked at src/errors.rs:261:13: Coroutine types are not supported yet note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace warning: Thread panicked when extracting item `weird::async_foo`. @@ -16,7 +16,7 @@ warning: Thread panicked when extracting item `weird::async_foo`. | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -thread 'rustc' () panicked at src/errors.rs:278:13: +thread 'rustc' () panicked at src/errors.rs:261:13: Thread panicked when extracting item `weird::async_foo`. ERROR Compilation panicked error: could not compile `weird` (lib) diff --git a/anneal/tests/integration.rs b/anneal/tests/integration.rs index 9fa2598e6b..036d50f4ea 100644 --- a/anneal/tests/integration.rs +++ b/anneal/tests/integration.rs @@ -1,16 +1,18 @@ use std::{ - cmp, fs, io, + fs, io, + io::Write as _, os::unix::fs::PermissionsExt, path::{Path, PathBuf}, - process::Command, - sync::OnceLock, + process::{self, Stdio}, + sync::{Arc, Condvar, Mutex, OnceLock}, thread, - time::Duration, + time::{Duration, Instant}, }; -use fs2::FileExt; +use assert_cmd::assert::Assert; +use fs2::FileExt as _; use serde::Deserialize; -use sha2::Digest; +use serde_json::json; use walkdir::WalkDir; fn new_sorted_walkdir(path: impl AsRef) -> WalkDir { @@ -39,7 +41,7 @@ enum ExpectedStatus { // A note on our "no implicit files" philosophy: We prefer explicit // configuration to implicit conventions. Thus, unless explicitly specified in -// `anneal.toml` (e.g., via `stderr_file` or `matches_expected_directory`), the +// `anneal.toml` (e.g., via `stderr_file` or `matches_expected_dir`), the // test runner will completely ignore all other files in // `tests/fixtures/`. It will not implicitly search for "implicit // files" (like `expected.stderr`) if they are not named in the TOML @@ -62,9 +64,6 @@ struct TestConfig { #[serde(default)] command: Vec, mock: Option, - - #[serde(default)] - env: std::collections::HashMap, #[serde(default)] phases: Vec, } @@ -104,8 +103,6 @@ struct ArtifactExpectation { #[serde(default)] content_contains: Vec, #[serde(default)] - content_lacks: Vec, - #[serde(default)] matches_expected_dir: Option, } @@ -113,12 +110,127 @@ struct ArtifactExpectation { #[serde(deny_unknown_fields)] struct CommandExpectation { args: Vec, - #[serde(default)] - should_not_exist: bool, } static TARGET_DIR: OnceLock = OnceLock::new(); -static TOOLCHAIN_PATH: OnceLock = OnceLock::new(); +static TOOLCHAIN_BASE_DIR: OnceLock = OnceLock::new(); +static TOOLCHAIN_INSTALL_DIR: OnceLock = OnceLock::new(); +static TOOLCHAIN_RUN_JOBS: OnceLock = OnceLock::new(); +static PROFILE_LOG: OnceLock> = OnceLock::new(); +static PROFILE_SAMPLE_MS: OnceLock = OnceLock::new(); +static PROFILE_EMIT_SAMPLES: OnceLock = OnceLock::new(); + +struct ProfileLog { + file: Mutex, + start: Instant, +} + +struct ProfileScope { + test: String, + phase: Option, + name: &'static str, + start: Instant, +} + +impl ProfileScope { + fn new(test: &str, phase: Option<&str>, name: &'static str) -> Self { + Self { + test: test.to_string(), + phase: phase.map(str::to_string), + name, + start: Instant::now(), + } + } +} + +impl Drop for ProfileScope { + fn drop(&mut self) { + emit_profile_event(json!({ + "event": "duration", + "test": self.test, + "phase": self.phase, + "name": self.name, + "start_ms": profile_elapsed_ms(self.start), + "duration_ms": self.start.elapsed().as_millis(), + })); + } +} + +#[derive(Clone, Default)] +struct ProcessMetrics { + samples: usize, + max_processes: usize, + max_threads: u64, + max_open_fds: u64, + max_rss_kb: u64, + max_read_bytes: u64, + max_write_bytes: u64, +} + +struct CommandRun { + assert: Assert, +} + +fn profile_step( + test: &str, + phase: Option<&str>, + name: &'static str, + f: impl FnOnce() -> T, +) -> T { + let _scope = ProfileScope::new(test, phase, name); + f() +} + +fn profile_log() -> Option<&'static ProfileLog> { + PROFILE_LOG + .get_or_init(|| { + let path = std::env::var_os("ANNEAL_INTEGRATION_PROFILE")?; + let path = PathBuf::from(path); + if let Some(parent) = path.parent() + && !parent.as_os_str().is_empty() + { + fs::create_dir_all(parent).unwrap_or_else(|e| { + panic!("failed to create profile directory {}: {e}", parent.display()) + }); + } + + let file = + fs::OpenOptions::new().create(true).append(true).open(&path).unwrap_or_else(|e| { + panic!("failed to open profile log {}: {e}", path.display()) + }); + Some(ProfileLog { file: Mutex::new(file), start: Instant::now() }) + }) + .as_ref() +} + +fn profile_elapsed_ms(instant: Instant) -> u128 { + profile_log().map(|log| instant.saturating_duration_since(log.start).as_millis()).unwrap_or(0) +} + +fn emit_profile_event(mut event: serde_json::Value) { + let Some(log) = profile_log() else { return }; + if let Some(obj) = event.as_object_mut() { + obj.insert("pid".to_string(), json!(process::id())); + obj.insert("thread".to_string(), json!(format!("{:?}", thread::current().id()))); + } + let mut file = log.file.lock().expect("profile log mutex poisoned"); + writeln!(file, "{event}").expect("failed to write profile event"); +} + +fn profile_sample_ms() -> u64 { + *PROFILE_SAMPLE_MS.get_or_init(|| { + std::env::var("ANNEAL_INTEGRATION_PROFILE_SAMPLE_MS") + .ok() + .and_then(|s| s.parse().ok()) + .unwrap_or(500) + }) +} + +fn profile_emit_samples() -> bool { + *PROFILE_EMIT_SAMPLES.get_or_init(|| { + std::env::var("ANNEAL_INTEGRATION_PROFILE_EMIT_SAMPLES").as_deref() == Ok("1") + }) +} fn get_target_dir() -> PathBuf { TARGET_DIR @@ -133,35 +245,346 @@ fn get_target_dir() -> PathBuf { .clone() } -fn get_toolchain_path() -> PathBuf { - TOOLCHAIN_PATH +fn get_toolchain_base_dir() -> PathBuf { + TOOLCHAIN_BASE_DIR .get_or_init(|| { - let cargo_bin = env!("CARGO_BIN_EXE_cargo-anneal"); - let output = Command::new(cargo_bin) - .arg("toolchain-path") - .output() - .expect("Failed to execute cargo-anneal toolchain-path"); + std::env::var_os("ANNEAL_TOOLCHAIN_DIR").map(PathBuf::from).expect( + "Anneal integration tests require ANNEAL_TOOLCHAIN_DIR to point at a \ + directory where `cargo run setup --local-archive ...` has already run.", + ) + }) + .clone() +} - if !output.status.success() { +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!( - "cargo-anneal toolchain-path failed: {:?}", - String::from_utf8_lossy(&output.stderr) + "Anneal toolchain is not installed at {}. Run `cargo run setup \ + --local-archive ...` once before running integration tests.", + dir.display() ); } - let path_str = String::from_utf8(output.stdout).unwrap(); - let toolchain_path = PathBuf::from(path_str.trim()); + for path in [ + dir.join("aeneas/bin/charon"), + dir.join("aeneas/bin/aeneas"), + dir.join("lean/bin/lake"), + ] { + if !path.exists() { + panic!( + "Anneal toolchain installation is missing {}. Re-run `cargo run setup \ + --local-archive ...` before running integration tests.", + path.display() + ); + } + } + + dir + }) + .clone() +} - if !toolchain_path.exists() { - panic!( - "Resolved toolchain path does not exist: {:?}. Please run `cargo run setup` first.", - toolchain_path +fn get_toolchain_bin_dir() -> PathBuf { + get_toolchain_install_dir().join("aeneas").join("bin") +} + +fn toolchain_run_jobs() -> usize { + *TOOLCHAIN_RUN_JOBS.get_or_init(|| { + std::env::var("ANNEAL_INTEGRATION_REAL_JOBS") + .ok() + .and_then(|s| s.parse().ok()) + .filter(|jobs| *jobs > 0) + .unwrap_or(1) + }) +} + +struct ToolchainRunPermit { + _lock: fs::File, + slot: usize, + jobs: usize, + wait: Duration, + acquired_at: Instant, +} + +impl ToolchainRunPermit { + fn hold_duration(&self) -> Duration { + self.acquired_at.elapsed() + } +} + +fn acquire_toolchain_run_slot() -> ToolchainRunPermit { + let started = Instant::now(); + let jobs = toolchain_run_jobs(); + let target_dir = get_target_dir(); + fs::create_dir_all(&target_dir).expect("failed to create integration target directory"); + + loop { + for slot in 0..jobs { + let lock_path = target_dir.join(format!("anneal-toolchain-run-{slot}.lock")); + let lock = + fs::OpenOptions::new().create(true).write(true).open(&lock_path).unwrap_or_else( + |e| panic!("failed to open integration lock {}: {e}", lock_path.display()), ); + match lock.try_lock_exclusive() { + Ok(()) => { + return ToolchainRunPermit { + _lock: lock, + slot, + jobs, + wait: started.elapsed(), + acquired_at: Instant::now(), + }; + } + Err(e) if e.kind() == io::ErrorKind::WouldBlock => continue, + Err(e) => panic!("failed to lock {}: {e}", lock_path.display()), } + } - toolchain_path + thread::sleep(Duration::from_millis(25)); + } +} + +fn run_command_with_profile( + test: &str, + phase: Option<&str>, + mut cmd: process::Command, +) -> io::Result { + let argv: Vec<_> = std::iter::once(cmd.get_program().to_string_lossy().to_string()) + .chain(cmd.get_args().map(|arg| arg.to_string_lossy().to_string())) + .collect(); + let cwd = cmd.get_current_dir().map(|dir| dir.display().to_string()); + let started = Instant::now(); + + cmd.stdin(Stdio::null()).stdout(Stdio::piped()).stderr(Stdio::piped()); + let child = cmd.spawn()?; + let child_pid = child.id(); + let sampler = ProcessSampler::start(test, phase, child_pid); + let output = child.wait_with_output()?; + let metrics = sampler.map(ProcessSampler::finish); + + let metrics_json = metrics.as_ref().map(|metrics| { + json!({ + "samples": metrics.samples, + "max_processes": metrics.max_processes, + "max_threads": metrics.max_threads, + "max_open_fds": metrics.max_open_fds, + "max_rss_kb": metrics.max_rss_kb, + "max_read_bytes": metrics.max_read_bytes, + "max_write_bytes": metrics.max_write_bytes, }) - .clone() + }); + + emit_profile_event(json!({ + "event": "command", + "test": test, + "phase": phase, + "argv": argv, + "cwd": cwd, + "status_code": output.status.code(), + "success": output.status.success(), + "start_ms": profile_elapsed_ms(started), + "duration_ms": started.elapsed().as_millis(), + "stdout_bytes": output.stdout.len(), + "stderr_bytes": output.stderr.len(), + "process_metrics": metrics_json, + })); + + Ok(CommandRun { assert: Assert::new(output) }) +} + +struct ProcessSampler { + stop: Arc<(Mutex, Condvar)>, + handle: thread::JoinHandle, +} + +impl ProcessSampler { + fn start(test: &str, phase: Option<&str>, root_pid: u32) -> Option { + profile_log()?; + let sample_ms = profile_sample_ms(); + if sample_ms == 0 { + return None; + } + + let stop = Arc::new((Mutex::new(false), Condvar::new())); + let thread_stop = Arc::clone(&stop); + let test = test.to_string(); + let phase = phase.map(str::to_string); + let handle = thread::spawn(move || { + let started = Instant::now(); + let mut metrics = ProcessMetrics::default(); + loop { + if *thread_stop.0.lock().expect("process sampler mutex poisoned") { + break; + } + + if let Some(sample) = collect_process_sample(root_pid) { + metrics.samples += 1; + metrics.max_processes = metrics.max_processes.max(sample.processes); + metrics.max_threads = metrics.max_threads.max(sample.threads); + metrics.max_open_fds = metrics.max_open_fds.max(sample.open_fds); + metrics.max_rss_kb = metrics.max_rss_kb.max(sample.rss_kb); + metrics.max_read_bytes = metrics.max_read_bytes.max(sample.read_bytes); + metrics.max_write_bytes = metrics.max_write_bytes.max(sample.write_bytes); + + if profile_emit_samples() { + emit_profile_event(json!({ + "event": "process_sample", + "test": test, + "phase": phase, + "root_pid": root_pid, + "sample_elapsed_ms": started.elapsed().as_millis(), + "processes": sample.processes, + "threads": sample.threads, + "open_fds": sample.open_fds, + "rss_kb": sample.rss_kb, + "read_bytes": sample.read_bytes, + "write_bytes": sample.write_bytes, + })); + } + } + + let stop = thread_stop.0.lock().expect("process sampler mutex poisoned"); + let (stop, _) = thread_stop + .1 + .wait_timeout_while(stop, Duration::from_millis(sample_ms), |stop| !*stop) + .expect("process sampler condvar poisoned"); + if *stop { + break; + } + } + metrics + }); + + Some(Self { stop, handle }) + } + + fn finish(self) -> ProcessMetrics { + *self.stop.0.lock().expect("process sampler mutex poisoned") = true; + self.stop.1.notify_one(); + self.handle.join().expect("process sampler panicked") + } +} + +#[derive(Default)] +struct ProcessSample { + processes: usize, + threads: u64, + open_fds: u64, + rss_kb: u64, + read_bytes: u64, + write_bytes: u64, +} + +#[cfg(target_os = "linux")] +fn collect_process_sample(root_pid: u32) -> Option { + let mut parents = std::collections::HashMap::new(); + for entry in fs::read_dir("/proc").ok()? { + let Ok(entry) = entry else { continue }; + let Some(pid) = entry.file_name().to_str().and_then(|name| name.parse::().ok()) else { + continue; + }; + if let Some(ppid) = read_proc_ppid(pid) { + parents.insert(pid, ppid); + } + } + + if !parents.contains_key(&root_pid) { + return None; + } + + let mut sample = ProcessSample::default(); + for &pid in parents.keys() { + if !is_descendant(pid, root_pid, &parents) { + continue; + } + sample.processes += 1; + if let Some(status) = read_proc_status(pid) { + sample.rss_kb += status.rss_kb; + sample.threads += status.threads; + } + sample.open_fds += fs::read_dir(format!("/proc/{pid}/fd")) + .map(|entries| entries.count() as u64) + .unwrap_or(0); + if let Some(io) = read_proc_io(pid) { + sample.read_bytes += io.0; + sample.write_bytes += io.1; + } + } + + Some(sample) +} + +#[cfg(not(target_os = "linux"))] +fn collect_process_sample(_root_pid: u32) -> Option { + None +} + +#[cfg(target_os = "linux")] +fn read_proc_ppid(pid: u32) -> Option { + let stat = fs::read_to_string(format!("/proc/{pid}/stat")).ok()?; + let (_, fields) = stat.rsplit_once(") ")?; + fields.split_whitespace().nth(1)?.parse().ok() +} + +#[cfg(target_os = "linux")] +fn is_descendant( + mut pid: u32, + root_pid: u32, + parents: &std::collections::HashMap, +) -> bool { + loop { + if pid == root_pid { + return true; + } + let Some(&ppid) = parents.get(&pid) else { return false }; + if ppid == 0 || ppid == pid { + return false; + } + pid = ppid; + } +} + +#[cfg(target_os = "linux")] +struct ProcStatus { + rss_kb: u64, + threads: u64, +} + +#[cfg(target_os = "linux")] +fn read_proc_status(pid: u32) -> Option { + let status = fs::read_to_string(format!("/proc/{pid}/status")).ok()?; + let mut proc_status = ProcStatus { rss_kb: 0, threads: 0 }; + for line in status.lines() { + if let Some(rest) = line.strip_prefix("VmRSS:") { + proc_status.rss_kb = + rest.split_whitespace().next().and_then(|s| s.parse().ok()).unwrap_or(0); + } else if let Some(rest) = line.strip_prefix("Threads:") { + proc_status.threads = + rest.split_whitespace().next().and_then(|s| s.parse().ok()).unwrap_or(0); + } + } + Some(proc_status) +} + +#[cfg(target_os = "linux")] +fn read_proc_io(pid: u32) -> Option<(u64, u64)> { + let io = fs::read_to_string(format!("/proc/{pid}/io")).ok()?; + let mut read_bytes = 0; + let mut write_bytes = 0; + for line in io.lines() { + if let Some(rest) = line.strip_prefix("read_bytes:") { + read_bytes = rest.trim().parse().unwrap_or(0); + } else if let Some(rest) = line.strip_prefix("write_bytes:") { + write_bytes = rest.trim().parse().unwrap_or(0); + } + } + Some((read_bytes, write_bytes)) } fn check_source_freshness(source_dir: &Path) -> Result<(), anyhow::Error> { @@ -238,7 +661,6 @@ struct TestContext { test_name: String, sandbox_root: PathBuf, _temp_dir: Option, // Kept alive to prevent deletion - test_config: TestConfig, home_dir: PathBuf, } @@ -247,17 +669,22 @@ impl TestContext { let test_case_root = path.parent().unwrap().to_path_buf(); let test_name = test_case_root.file_name().unwrap().to_string_lossy().to_string(); let source_dir = test_case_root.join("source"); - check_source_freshness(&source_dir).map_err(|e| e.to_string())?; + profile_step(&test_name, None, "check_source_freshness", || { + check_source_freshness(&source_dir).map_err(|e| e.to_string()) + })?; let target_dir = get_target_dir(); - fs::create_dir_all(&target_dir)?; - let toolchain_path = get_toolchain_path(); - let temp = tempfile::Builder::new().prefix("anneal-test-").tempdir_in(&target_dir)?; + let temp = profile_step(&test_name, None, "create_sandbox", || { + fs::create_dir_all(&target_dir)?; + tempfile::Builder::new().prefix("anneal-test-").tempdir_in(&target_dir) + })?; let sandbox_root = temp.path().join(&test_name); let home_dir = temp.path().join("home"); - fs::create_dir_all(&home_dir)?; - copy_dir_contents(&source_dir, &sandbox_root)?; + profile_step(&test_name, None, "copy_fixture_source", || { + fs::create_dir_all(&home_dir)?; + copy_dir_contents(&source_dir, &sandbox_root) + })?; // Check if we should keep the test directory for debugging let temp_dir_to_store = if std::env::var("ANNEAL_KEEP_TEST_DIR").as_deref() == Ok("1") @@ -275,28 +702,24 @@ impl TestContext { }; // Copy extra inputs based on config. - for extra in &config.extra_inputs { - let extra_path = test_case_root.join(extra); - if extra_path.exists() { - let dest = sandbox_root.join(extra); - if let Some(parent) = dest.parent() { - // Create parent directories for the destination to support - // copying extra inputs into nested paths within the - // sandbox. - fs::create_dir_all(parent)?; + profile_step(&test_name, None, "copy_extra_inputs", || { + for extra in &config.extra_inputs { + let extra_path = test_case_root.join(extra); + if extra_path.exists() { + let dest = sandbox_root.join(extra); + if let Some(parent) = dest.parent() { + // Create parent directories for the destination to support + // copying extra inputs into nested paths within the + // sandbox. + fs::create_dir_all(parent)?; + } + fs::copy(&extra_path, dest)?; } - fs::copy(&extra_path, dest)?; } - } + Ok::<_, io::Error>(()) + })?; - Ok(Self { - test_case_root, - test_name, - sandbox_root, - _temp_dir: temp_dir_to_store, - test_config: config.clone(), - home_dir, - }) + Ok(Self { test_case_root, test_name, sandbox_root, _temp_dir: temp_dir_to_store, home_dir }) } fn create_shim( @@ -314,15 +737,6 @@ impl TestContext { let mut shim_content = String::new(); shim_content.push_str("#!/bin/sh\n"); - // For backward compatibility with legacy tests, we log "AENEAS INVOKED" - // for Aeneas. This allows existing tests to verify that Aeneas was - // actually called. - if binary == "aeneas" { - use std::fmt::Write; - writeln!(shim_content, "echo \"AENEAS INVOKED\" >> \"{}\"", log_file.display()) - .unwrap(); - } - shim_content.push_str(&format!( r#"for arg in "$@"; do echo "{}_ARG:$arg" >> "{}" @@ -360,43 +774,32 @@ echo "---END-INVOCATION---" >> "{}" Ok(shim_dir) } - fn run_anneal(&self, config: &TestConfig) -> assert_cmd::assert::Assert { - let mut cmd = assert_cmd::cargo_bin_cmd!("cargo-anneal"); + fn run_anneal(&self, config: &TestConfig, phase_name: Option<&str>) -> CommandRun { + let mut cmd = process::Command::new(assert_cmd::cargo::cargo_bin!("cargo-anneal")); cmd.env_clear(); // After clearing the environment to prevent scope leakage, we must - // manually forward essential host variables required for toolchains. + // manually forward essential host variables required by Cargo and the + // host toolchain. for var in [ "RUSTUP_HOME", "CARGO_HOME", "RUSTUP_TOOLCHAIN", - "ELAN_HOME", "LD_LIBRARY_PATH", "TMPDIR", "TMP", "TEMP", "USER", "USERNAME", - "ANNEAL_TOOLCHAIN_DIR", ] { if let Some(val) = std::env::var_os(var) { cmd.env(var, val); } } + cmd.env("ANNEAL_TOOLCHAIN_DIR", get_toolchain_base_dir()); cmd.env("HOME", &self.home_dir); - if let Ok(elan_home) = std::env::var("ELAN_HOME") { - cmd.env("ELAN_HOME", elan_home); - } else { - let elan_home = if std::env::var("__ZEROCOPY_LOCAL_DEV").is_ok() { - get_target_dir().join("anneal-home/.elan") - } else { - PathBuf::from(std::env::var("HOME").unwrap()).join(".elan") - }; - cmd.env("ELAN_HOME", elan_home); - } - // Resolve Mocks // Re-organizing execution flow: @@ -404,94 +807,102 @@ echo "---END-INVOCATION---" >> "{}" let mut charon_mock_mode = None; let mut aeneas_mock_mode = None; - if let Some(mock_config) = &config.mock { - if let Some(charon_mock) = &mock_config.charon { - let mock_src = self.test_case_root.join(charon_mock); + profile_step(&self.test_name, phase_name, "prepare_mocks", || { + if let Some(mock_config) = &config.mock { + if let Some(charon_mock) = &mock_config.charon { + let mock_src = self.test_case_root.join(charon_mock); - if charon_mock.ends_with(".sh") { + if charon_mock.ends_with(".sh") { + let bin_dir = self.sandbox_root.join("bin"); + fs::create_dir_all(&bin_dir).unwrap(); + let script_dest = bin_dir.join(charon_mock); + fs::copy(&mock_src, &script_dest).unwrap(); + + let mut perms = fs::metadata(&script_dest).unwrap().permissions(); + perms.set_mode(0o755); + fs::set_permissions(&script_dest, perms).unwrap(); + + charon_mock_mode = Some(MockMode::Script(script_dest)); + } else { + let mock_content = + fs::read_to_string(&mock_src).expect("Failed to read mock file"); + + let processed_mock = mock_content + .replace("[PROJECT_ROOT]", self.sandbox_root.to_str().unwrap()); + let processed_mock_file = self.sandbox_root.join("mock_charon.json"); + fs::write(&processed_mock_file, &processed_mock).unwrap(); + charon_mock_mode = Some(MockMode::FailWithOutput(processed_mock_file)); + } + } + if let Some(aeneas_script) = &mock_config.aeneas { + let script_src = self.test_case_root.join(aeneas_script); let bin_dir = self.sandbox_root.join("bin"); fs::create_dir_all(&bin_dir).unwrap(); - let script_dest = bin_dir.join(charon_mock); - fs::copy(&mock_src, &script_dest).unwrap(); + let script_dest = bin_dir.join("mock_aeneas.sh"); + fs::copy(&script_src, &script_dest).unwrap(); let mut perms = fs::metadata(&script_dest).unwrap().permissions(); perms.set_mode(0o755); fs::set_permissions(&script_dest, perms).unwrap(); - charon_mock_mode = Some(MockMode::Script(script_dest)); - } else { - let mock_content = - fs::read_to_string(&mock_src).expect("Failed to read mock file"); - - let processed_mock = - mock_content.replace("[PROJECT_ROOT]", self.sandbox_root.to_str().unwrap()); - let processed_mock_file = self.sandbox_root.join("mock_charon.json"); - fs::write(&processed_mock_file, &processed_mock).unwrap(); - charon_mock_mode = Some(MockMode::FailWithOutput(processed_mock_file)); + aeneas_mock_mode = Some(MockMode::Script(script_dest)); } } - if let Some(aeneas_script) = &mock_config.aeneas { - let script_src = self.test_case_root.join(aeneas_script); - let bin_dir = self.sandbox_root.join("bin"); - fs::create_dir_all(&bin_dir).unwrap(); - let script_dest = bin_dir.join("mock_aeneas.sh"); - fs::copy(&script_src, &script_dest).unwrap(); - - let mut perms = fs::metadata(&script_dest).unwrap().permissions(); - perms.set_mode(0o755); - fs::set_permissions(&script_dest, perms).unwrap(); - - aeneas_mock_mode = Some(MockMode::Script(script_dest)); - } - } + }); // Create shims for Charon and Aeneas. // - // Even if we are using the "real" binary, we wrap it in a shim to - // capture the arguments passed to it. This allows us to assert that - // Anneal calls the tools with the expected arguments. - - let toolchain_path = get_toolchain_path(); - let real_charon = toolchain_path.join("charon"); - let shim_dir = self.create_shim("charon", &real_charon, charon_mock_mode).unwrap(); + // Most integration tests run against the already-installed toolchain + // directly. Only tests that explicitly request mocks or command + // assertions use PATH shims. + let use_tool_shims = config.mock.is_some() || !config.command.is_empty(); + let original_path = std::env::var_os("PATH").unwrap_or_default(); + profile_step(&self.test_name, phase_name, "prepare_tool_shims", || { + if use_tool_shims { + let toolchain_bin_dir = get_toolchain_bin_dir(); + let shim_dir = self.sandbox_root.join("bin_shim"); + fs::create_dir_all(&shim_dir).unwrap(); + + if charon_mock_mode.is_some() || !config.command.is_empty() { + let real_charon = toolchain_bin_dir.join("charon"); + self.create_shim("charon", &real_charon, charon_mock_mode).unwrap(); + } + if aeneas_mock_mode.is_some() { + let real_aeneas = toolchain_bin_dir.join("aeneas"); + self.create_shim("aeneas", &real_aeneas, aeneas_mock_mode).unwrap(); + } - let real_aeneas = toolchain_path.join("aeneas"); - self.create_shim("aeneas", &real_aeneas, aeneas_mock_mode).unwrap(); + let new_path = std::env::join_paths( + std::iter::once(shim_dir) + .chain(std::iter::once(toolchain_bin_dir)) + .chain(std::env::split_paths(&original_path)), + ) + .unwrap(); + cmd.env("PATH", new_path); + cmd.env("ANNEAL_USE_PATH_FOR_TOOLS", "1"); + } else { + cmd.env("PATH", original_path); + } + }); cmd.env("ANNEAL_FORCE_TTY", "1"); cmd.env("FORCE_COLOR", "1"); - - cmd.env("ANNEAL_USE_PATH_FOR_TOOLS", "1"); cmd.env("RAYON_NUM_THREADS", "1"); - let original_path = std::env::var_os("PATH").unwrap_or_default(); - let new_path = std::env::join_paths( - std::iter::once(shim_dir).chain(std::env::split_paths(&original_path)), - ) - .unwrap(); - // Ensure deterministic LLBC generation within the integration test // sandbox by rebasing the `workspace_root` off the absolute filesystem // onto `/dummy`. let rustflags = format!("--remap-path-prefix={}=/dummy", self.test_case_root.display()); cmd.env("CARGO_TARGET_DIR", self.sandbox_root.join("target")); - cmd.env("PATH", new_path); cmd.env("RUSTFLAGS", rustflags); - // Redirect HOME to the persistent home directory within the sandbox. - // This ensures that the toolchain is looked up and potentially - // repaired/reinstalled in a location that is isolated from the - // user's actual home directory but remains persistent across - // multiple `anneal` invocations within this single test context. + // Redirect HOME to a persistent directory within the sandbox so + // user-local Cargo or tool output cannot leak across fixtures. cmd.env("HOME", &self.home_dir) .env("ANNEAL_TEST_DIR_NAME", "anneal_test_target") .env("ANNEAL_HASH_WITH_REMOVED_PREFIX", &self.sandbox_root); - for (k, v) in &config.env { - cmd.env(k, v); - } - if !self.sandbox_root.exists() { panic!("sandbox_root does NOT exist! {:?}", self.sandbox_root); } @@ -507,19 +918,25 @@ echo "---END-INVOCATION---" >> "{}" cmd.arg("verify"); } - cmd.assert() + run_command_with_profile(&self.test_name, phase_name, cmd) + .expect("failed to execute cargo-anneal") } } fn run_integration_test(path: &Path) -> datatest_stable::Result<()> { let path_str = path.to_string_lossy(); - - let anneal_toml_content = fs::read_to_string(path) - .unwrap_or_else(|e| panic!("Failed to read {}: {}", path.display(), e)); - let anneal_toml: AnnealToml = toml::from_str(&anneal_toml_content) - .unwrap_or_else(|e| panic!("Failed to parse {}: {}", path.display(), e)); let test_case_root = path.parent().unwrap(); let test_name = test_case_root.file_name().unwrap().to_string_lossy().to_string(); + let _fixture_scope = ProfileScope::new(&test_name, None, "fixture_total"); + + let anneal_toml_content = profile_step(&test_name, None, "read_manifest", || { + fs::read_to_string(path) + .unwrap_or_else(|e| panic!("Failed to read {}: {}", path.display(), e)) + }); + let anneal_toml: AnnealToml = profile_step(&test_name, None, "parse_manifest", || { + toml::from_str(&anneal_toml_content) + .unwrap_or_else(|e| panic!("Failed to parse {}: {}", path.display(), e)) + }); assert!( !anneal_toml.description.trim().is_empty(), "Test {} is missing a non-empty `description` field in anneal.toml", @@ -528,22 +945,16 @@ fn run_integration_test(path: &Path) -> datatest_stable::Result<()> { // Special handling for the "dirty_sandbox" test case. if path_str.contains("dirty_sandbox/anneal.toml") { - return run_dirty_sandbox_test(path); + return profile_step(&test_name, None, "dirty_sandbox_test", || { + run_dirty_sandbox_test(path) + }); } - // // Special handling for the "atomic_writes" test case. - // if path_str.contains("atomic_writes/anneal.toml") { - // return run_atomic_writes_test(path); - // } - // Special handling for the "toolchain_versioning" test case. - if path_str.contains("toolchain_versioning/anneal.toml") { - return run_toolchain_versioning_test(path); - } - // Load the test configuration from the associated 'anneal.toml' manifest. let config = anneal_toml.test.unwrap_or_default(); // `path` is `tests/fixtures//anneal.toml` - let ctx = TestContext::new(path, &config)?; + let ctx = + profile_step(&test_name, None, "create_test_context", || TestContext::new(path, &config))?; if config.phases.is_empty() { run_single_phase(&ctx, &config, None)?; @@ -563,21 +974,28 @@ fn run_integration_test(path: &Path) -> datatest_stable::Result<()> { // outputs. if !config.artifact.is_empty() { let anneal_run_root = ctx.sandbox_root.join("target/anneal/anneal_test_target"); - assert_artifacts_match(&anneal_run_root, &ctx.test_case_root, &config.artifact)?; + profile_step(&ctx.test_name, None, "assert_artifacts", || { + assert_artifacts_match(&anneal_run_root, &ctx.test_case_root, &config.artifact) + })?; } // Verify Commands if !config.command.is_empty() { - let log_file = ctx.sandbox_root.join("tool_args.log"); - if !log_file.exists() { - panic!("Command log file not found! Was the shim called?"); - } - let log_content = fs::read_to_string(log_file)?; - let invocations = parse_command_log(&log_content); - assert_commands_match(&invocations, &config.command); + profile_step(&ctx.test_name, None, "assert_commands", || { + let log_file = ctx.sandbox_root.join("tool_args.log"); + if !log_file.exists() { + panic!("Command log file not found! Was the shim called?"); + } + let log_content = fs::read_to_string(log_file)?; + let invocations = parse_command_log(&log_content); + assert_commands_match(&invocations, &config.command); + Ok::<_, io::Error>(()) + })?; } - assert_no_unmapped_files(&ctx, &config); + profile_step(&ctx.test_name, None, "assert_no_unmapped_files", || { + assert_no_unmapped_files(&ctx, &config) + }); Ok(()) } @@ -589,17 +1007,6 @@ fn assert_no_unmapped_files(ctx: &TestContext, config: &TestConfig) { allowed_paths.insert(ctx.test_case_root.join("source")); allowed_paths.insert(ctx.test_case_root.join("anneal.toml")); - // Track artifacts that are explicitly defined in the test configuration - // TOML. This allows them to bypass the unmapped file directory check. - if let Some(mock) = &config.mock { - if let Some(charon) = &mock.charon { - allowed_paths.insert(ctx.test_case_root.join(charon)); - } - if let Some(aeneas) = &mock.aeneas { - allowed_paths.insert(ctx.test_case_root.join(aeneas)); - } - } - for extra in &config.extra_inputs { allowed_paths.insert(ctx.test_case_root.join(extra)); } @@ -670,184 +1077,58 @@ fn run_single_phase( base_config: &TestConfig, phase: Option<&TestPhase>, ) -> datatest_stable::Result<()> { + let phase_name = phase.map(|phase| phase.name.as_str()); + let _phase_scope = ProfileScope::new(&ctx.test_name, phase_name, "phase_total"); + if let Some(phase) = phase && let Some(action) = &phase.action { if action == "touch_stale_file" { - let target_dir = ctx.sandbox_root.join("target"); - let generated_root = find_generated_root(&target_dir)?; - - let mut slug_dir = None; - for entry in fs::read_dir(&generated_root)? { - let entry = entry?; - if entry.file_type()?.is_dir() { - slug_dir = Some(entry.path()); - break; + return profile_step(&ctx.test_name, phase_name, "action_touch_stale_file", || { + let generated_root = + ctx.sandbox_root.join("target/anneal/anneal_test_target/lean/generated"); + if !generated_root.exists() { + return Err(format!( + "Generated Lean directory not found at {}", + generated_root.display() + ) + .into()); } - } - let slug_dir = slug_dir.ok_or_else(|| { - io::Error::new(io::ErrorKind::NotFound, "No slug directory found in generated root") - })?; - let stale_file = slug_dir.join("Stale.lean"); - std::fs::write(&stale_file, "INVALID LEAN CODE").unwrap(); - assert!(stale_file.exists()); - - return Ok(()); - } else if action == "delete_lake_dir" { - // Delete the `.lake` build artifacts directory. This is used in - // `stale_output` tests to force Lake to regenerate its build - // artifacts from scratch, ensuring that stale cached data doesn't - // mask bugs in artifact generation or synchronization. - let lean_root = ctx.sandbox_root.join("target/anneal/anneal_test_target/lean"); - let lake_dir = lean_root.join(".lake"); - if lake_dir.exists() { - fs::remove_dir_all(&lake_dir).expect("Failed to delete .lake directory"); - } - return Ok(()); - } else if action.starts_with("delete_toolchain_file ") { - let file_name = action.strip_prefix("delete_toolchain_file ").unwrap(); - let toolchain_root = ctx.home_dir.join(".anneal/toolchain"); - - // The toolchain directory name includes a short hash of the version, - // which changes whenever the managed dependencies are updated. To - // remain robust across version changes, we scan for any directory - // existing within the toolchain root. - let build_dir = fs::read_dir(&toolchain_root)? - .filter_map(|e| e.ok()) - .find(|e| e.file_type().map(|t| t.is_dir()).unwrap_or(false)) - .ok_or_else(|| { - io::Error::new(io::ErrorKind::NotFound, "Toolchain build directory not found") - })? - .path(); - let target_file = build_dir.join(file_name); - if target_file.exists() { - fs::remove_file(&target_file).expect("Failed to delete toolchain file"); - } - return Ok(()); - } else if action.starts_with("corrupt_toolchain_file ") { - let file_name = action.strip_prefix("corrupt_toolchain_file ").unwrap(); - let toolchain_root = ctx.home_dir.join(".anneal/toolchain"); - - // Scan for the hash-prefixed toolchain directory. - let build_dir = fs::read_dir(&toolchain_root)? - .filter_map(|e| e.ok()) - .find(|e| e.file_type().map(|t| t.is_dir()).unwrap_or(false)) - .ok_or_else(|| { - io::Error::new(io::ErrorKind::NotFound, "Toolchain build directory not found") - })? - .path(); - let target_file = build_dir.join(file_name); - if target_file.exists() { - // We corrupt the file with a known string that our assertions can - // identify later. - fs::write(&target_file, "CORRUPTED CONTENT") - .expect("Failed to corrupt toolchain file"); - } - return Ok(()); - } else if action.starts_with("assert_toolchain_binary ") { - let rest = action.strip_prefix("assert_toolchain_binary ").unwrap(); - let mut parts = rest.split_whitespace(); - let file_name = parts - .next() - .ok_or_else(|| io::Error::new(io::ErrorKind::InvalidInput, "Missing file name"))?; - let expected_hash = parts.next(); - - let toolchain_root = ctx.home_dir.join(".anneal/toolchain"); - if !toolchain_root.exists() { - let home_exists = ctx.home_dir.exists(); - let mut entries = Vec::new(); - if home_exists && let Ok(rd) = fs::read_dir(&ctx.home_dir) { - for e in rd.filter_map(|e| e.ok()) { - entries.push(e.file_name().to_string_lossy().to_string()); - } - } - panic!( - "Toolchain root missing at {:?}! home exists: {}, home contents: {:?}", - toolchain_root, home_exists, entries - ); - } - // Scan for the hash-prefixed toolchain directory. - let build_dir = fs::read_dir(&toolchain_root)? - .filter_map(|e| e.ok()) - .find(|e| e.file_type().map(|t| t.is_dir()).unwrap_or(false)) - .ok_or_else(|| { - io::Error::new(io::ErrorKind::NotFound, "Toolchain build directory not found") - })? - .path(); - let target_file = build_dir.join(file_name); - - match expected_hash { - Some("missing") => { - // Assert that the file has been successfully deleted/removed. - if target_file.exists() { - panic!( - "Expected toolchain file '{}' to be missing, but it exists", - file_name - ); - } - } - Some("corrupted") => { - // Assert that the file exists and contains the "CORRUPTED - // CONTENT" string written by a previous - // `corrupt_toolchain_file` action. - if !target_file.exists() { - panic!( - "Expected toolchain file '{}' to exist (corrupted), but it doesn't", - file_name - ); - } - let content = - fs::read_to_string(&target_file).expect("Failed to read toolchain file"); - if content != "CORRUPTED CONTENT" { - panic!( - "Expected toolchain file '{}' to be corrupted with 'CORRUPTED CONTENT', but it has different content", - file_name - ); - } - } - Some(expected_hash) => { - // Normal hash verification mode. - if !target_file.exists() { - panic!("Expected toolchain file '{}' to exist, but it doesn't", file_name); - } - let mut file = fs::File::open(&target_file)?; - let mut hasher = sha2::Sha256::new(); - std::io::copy(&mut file, &mut hasher)?; - let actual_hash = format!("{:x}", hasher.finalize()); - - if actual_hash != expected_hash { - panic!( - "Hash mismatch for toolchain file '{}'.\nExpected: {}\nActual: {}", - file_name, expected_hash, actual_hash - ); - } - } - None => { - // If no hash is specified, just assert existence. - if !target_file.exists() { - panic!("Expected toolchain file '{}' to exist, but it doesn't", file_name); + let mut slug_dir = None; + for entry in fs::read_dir(&generated_root)? { + let entry = entry?; + if entry.file_type()?.is_dir() { + slug_dir = Some(entry.path()); + break; } } - } - return Ok(()); - } else if action.starts_with("assert_toolchain_file_missing ") { - let file_name = action.strip_prefix("assert_toolchain_file_missing ").unwrap(); - let toolchain_root = ctx.home_dir.join(".anneal/toolchain"); - if let Ok(entries) = fs::read_dir(&toolchain_root) { - for entry in entries.filter_map(|e| e.ok()) { - if entry.file_type().map(|t| t.is_dir()).unwrap_or(false) { - let target_file = entry.path().join(file_name); - if target_file.exists() { - panic!( - "Expected toolchain file '{}' to be missing, but it exists", - file_name - ); - } - } + let slug_dir = slug_dir.ok_or_else(|| { + io::Error::new( + io::ErrorKind::NotFound, + "No slug directory found in generated root", + ) + })?; + + let stale_file = slug_dir.join("Stale.lean"); + std::fs::write(&stale_file, "INVALID LEAN CODE").unwrap(); + assert!(stale_file.exists()); + + Ok(()) + }); + } else if action == "delete_lake_dir" { + return profile_step(&ctx.test_name, phase_name, "action_delete_lake_dir", || { + // Delete the `.lake` build artifacts directory. This is used in + // `stale_output` tests to force Lake to regenerate its build + // artifacts from scratch, ensuring that stale cached data doesn't + // mask bugs in artifact generation or synchronization. + let lean_root = ctx.sandbox_root.join("target/anneal/anneal_test_target/lean"); + let lake_dir = lean_root.join(".lake"); + if lake_dir.exists() { + fs::remove_dir_all(&lake_dir).expect("Failed to delete .lake directory"); } - } - return Ok(()); + Ok(()) + }); } else { panic!("Unknown action: {}", action); } @@ -869,9 +1150,40 @@ fn run_single_phase( } } - let assert = ctx.run_anneal(&config); + // `datatest_stable` may schedule fixtures concurrently regardless of + // `RUST_TEST_THREADS`. Real toolchain runs copy/use the installed Lean + // dependency tree and can exhaust host-wide file handles if many do that at + // once. Mock-only tests do not hit that path, so keep those parallel while + // serializing the resource-heavy command execution. + let run = if config.mock.is_none() { + let permit = profile_step(&ctx.test_name, phase_name, "wait_toolchain_run_slot", || { + acquire_toolchain_run_slot() + }); + emit_profile_event(json!({ + "event": "toolchain_run_slot_acquired", + "test": ctx.test_name, + "phase": phase_name, + "slot": permit.slot, + "jobs": permit.jobs, + "wait_ms": permit.wait.as_millis(), + })); + let run = ctx.run_anneal(&config, phase_name); + emit_profile_event(json!({ + "event": "toolchain_run_slot_released", + "test": ctx.test_name, + "phase": phase_name, + "slot": permit.slot, + "jobs": permit.jobs, + "hold_ms": permit.hold_duration().as_millis(), + })); + run + } else { + ctx.run_anneal(&config, phase_name) + }; + let assert = run.assert; // Verify Exit Status + let _assert_status_scope = ProfileScope::new(&ctx.test_name, phase_name, "assert_exit_status"); let assert = match config.expected_status { ExpectedStatus::Failure => assert.failure(), ExpectedStatus::KnownBug => { @@ -888,6 +1200,7 @@ fn run_single_phase( } ExpectedStatus::Success => assert.success(), }; + drop(_assert_status_scope); // Verify the standard error output of the simulated command. // @@ -899,27 +1212,31 @@ fn run_single_phase( // manifest. let output = assert.get_output(); if let Some(stderr_file) = &config.stderr_file { - assert_output_file( - &ctx.test_case_root, - &ctx.sandbox_root, - &ctx.test_name, - &ctx.home_dir, - stderr_file, - &output.stderr, - "Stderr", - ); + profile_step(&ctx.test_name, phase_name, "assert_stderr", || { + assert_output_file( + &ctx.test_case_root, + &ctx.sandbox_root, + &ctx.test_name, + &ctx.home_dir, + stderr_file, + &output.stderr, + "Stderr", + ) + }); } if let Some(stdout_file) = &config.stdout_file { - assert_output_file( - &ctx.test_case_root, - &ctx.sandbox_root, - &ctx.test_name, - &ctx.home_dir, - stdout_file, - &output.stdout, - "Stdout", - ); + profile_step(&ctx.test_name, phase_name, "assert_stdout", || { + assert_output_file( + &ctx.test_case_root, + &ctx.sandbox_root, + &ctx.test_name, + &ctx.home_dir, + stdout_file, + &output.stdout, + "Stdout", + ) + }); } Ok(()) @@ -943,22 +1260,28 @@ fn assert_output_file( let replace_path = sandbox_root.to_str().unwrap(); let target_dir = get_target_dir(); - let toolchain_path = get_toolchain_path(); let target_path_str = target_dir.to_str().unwrap(); - let toolchain_path_str = toolchain_path.to_str().unwrap(); + let toolchain_base = get_toolchain_base_dir(); + let toolchain_base_str = toolchain_base.to_str().unwrap(); + let toolchain_install_dir = get_toolchain_install_dir(); + let toolchain_install_dir_str = toolchain_install_dir.to_str().unwrap(); + let toolchain_bin_dir = get_toolchain_bin_dir(); + let toolchain_bin_dir_str = toolchain_bin_dir.to_str().unwrap(); let home_path_str = home_dir.to_str().unwrap(); // Replace volatile environment-specific paths with static placeholders. // // - `replace_path` corresponds to the sandbox root, which varies per // test run. - // - `toolchain_path_str` corresponds to the global toolchain. + // - `toolchain_*` paths correspond to the shared pre-installed toolchain. // - `target_path_str` corresponds to the cargo target directory or override. // - `home_path_str` corresponds to the user's home directory (redirected in // tests). let actual_clean = sanitize_output( &actual_str .replace(replace_path, "[PROJECT_ROOT]") - .replace(toolchain_path_str, "[CACHE_ROOT]") + .replace(toolchain_bin_dir_str, "[CACHE_ROOT]") + .replace(toolchain_install_dir_str, "[CACHE_ROOT]") + .replace(toolchain_base_str, "[CACHE_ROOT]") .replace(home_path_str, "[HOME]") .replace(target_path_str, "[TARGET_DIR]"), ); @@ -997,89 +1320,20 @@ fn parse_command_log(content: &str) -> Vec> { current_args = Vec::new(); } else if let Some(arg) = line.strip_prefix("CHARON_ARG:") { current_args.push(arg.to_string()); - } else if let Some(arg) = line.strip_prefix("ARG:") { - // Backward compat/fallback - current_args.push(arg.to_string()); } } invocations } -/// Verifies that the generating `lakefile.lean` and `lean-toolchain` files -/// contain the correct Aeneas commit hash and Lean toolchain version, -/// matching the values specified in `Cargo.toml`. -fn run_toolchain_versioning_test(path: &Path) -> datatest_stable::Result<()> { - let config = TestConfig { - args: Some(vec!["verify".into(), "--allow-sorry".into()]), - ..Default::default() - }; - - // 1. Setup TestContext - let ctx = TestContext::new(path, &config)?; - - // 3. Run - let assert = ctx.run_anneal(&config); - assert.success(); - - // 4. Verify generated lakefile.lean and lean-toolchain - let target_dir = ctx.sandbox_root.join("target"); - - // Parse `Cargo.toml` to get the expected values. We expect the tests to be - // running in the workspace root, so we can find `Cargo.toml` there. - let cargo_toml_path = - PathBuf::from(std::env::var("CARGO_MANIFEST_DIR").unwrap()).join("Cargo.toml"); - let cargo_toml_content = fs::read_to_string(&cargo_toml_path)?; - let cargo_toml: toml::Value = toml::from_str(&cargo_toml_content)?; - let metadata = cargo_toml - .get("package") - .and_then(|p| p.get("metadata")) - .and_then(|m| m.get("build_rs")) - .expect("Cargo.toml must have [package.metadata.build_rs]"); - - let expected_rev = metadata.get("aeneas_rev").and_then(|v| v.as_str()).unwrap(); - let expected_toolchain = metadata.get("lean_toolchain").and_then(|v| v.as_str()).unwrap(); - - // Check `lakefile.lean` for the Aeneas revision. Even if using a local - // Aeneas path (which the test likely is), we expect the revision to be - // present in a comment. - let lean_dir = target_dir.join("anneal/anneal_test_target/lean"); - - let lakefile_path = lean_dir.join("lakefile.lean"); - let lakefile_content = fs::read_to_string(&lakefile_path)?; - - if !lakefile_content.contains(expected_rev) { - panic!( - "lakefile.lean does not contain expected aeneas_rev '{}'. Content:\n{}", - expected_rev, lakefile_content - ); - } - - // Check `lean-toolchain` for the correct Lean version. - let toolchain_path = lean_dir.join("lean-toolchain"); - let toolchain_content = fs::read_to_string(&toolchain_path)?; - - // toolchain content usually has a newline - if !toolchain_content.trim().contains(expected_toolchain) { - panic!( - "lean-toolchain does not contain expected toolchain '{}'. Content:\n{}", - expected_toolchain, toolchain_content - ); - } - - Ok(()) -} - fn assert_commands_match(invocations: &[Vec], expectations: &[CommandExpectation]) { for exp in expectations { let found = invocations.iter().any(|cmd| is_subsequence(cmd, &exp.args)); - if !exp.should_not_exist && !found { + if !found { panic!( "Expected command invocation with args {:?} was not found.\nCaptured Invocations: {:#?}", exp.args, invocations ); - } else if exp.should_not_exist && found { - panic!("Unexpected command invocation with args {:?} WAS found.", exp.args); } } } @@ -1144,9 +1398,8 @@ fn assert_artifacts_match( } } - // We match strictly on the slug prefix: "{package}-{target}-" - // Updated to use PascalCase to match scanner.rs logic - // let prefix = format!("{}-{}-", exp.package, exp.target); + // We match strictly on the PascalCase package/target prefix produced by + // scanner.rs. let pkg_pascal = to_pascal(&exp.package); let target_pascal = to_pascal(&exp.target); let prefix = format!("{}{}", pkg_pascal, target_pascal); @@ -1207,19 +1460,6 @@ fn assert_artifacts_match( } } - if matched_all { - for needle in &exp.content_lacks { - if content.contains(needle) { - matched_all = false; - collected_errors.push_str(&format!( - "Artifact '{}' contains unexpected content.\nUnexpected: '{}'\nPath: {:?}\n\n", - file_name, needle, path - )); - break; - } - } - } - if matched_all { any_matched_all = true; break; @@ -1274,67 +1514,21 @@ fn assert_artifacts_match( } // Because hash suffixes are opaque to the harness, multiple - // artifacts might match the package prefix. We use catch_unwind - // to test each candidate against the expected golden directory. The - // expectation passes if any one artifact matches. - // The expectation passes if any one artifact matches. + // artifacts might match the package prefix. The expectation + // passes if any one artifact matches. let mut any_matched = false; let mut collected_errors = String::new(); for file_name in matching_items { let actual_path = scan_dir.join(file_name); - let result = std::panic::catch_unwind(|| { - if actual_path.is_dir() != expected_path.is_dir() { - panic!( - "Type mismatch: expected {:?} (is_dir: {}), actual {:?} (is_dir: {})", - expected_path, - expected_path.is_dir(), - actual_path, - actual_path.is_dir() - ); - } - - if actual_path.is_dir() { - assert_directories_match(&expected_path, &actual_path).unwrap(); - } else { - let e_txt = - fs::read_to_string(&expected_path).unwrap().replace("\r\n", "\n"); - let a_txt = - fs::read_to_string(&actual_path).unwrap().replace("\r\n", "\n"); - if e_txt != a_txt { - use similar::{ChangeTag, TextDiff}; - let diff = TextDiff::from_lines(&e_txt, &a_txt); - let mut diff_str = String::new(); - for change in diff.iter_all_changes() { - let sign = match change.tag() { - ChangeTag::Delete => "-", - ChangeTag::Insert => "+", - ChangeTag::Equal => " ", - }; - diff_str.push_str(&format!("{sign}{change}")); - } - panic!("Mismatch in {:?}:\n{}", expected_path, diff_str); - } - } - }); - - match result { - Ok(_) => { + match artifact_path_matches(&expected_path, &actual_path) { + Ok(()) => { any_matched = true; break; } - Err(e) => { - let err_msg = if let Some(s) = e.downcast_ref::<&str>() { - s.to_string() - } else { - "Unknown panic during assertion".to_string() - }; - collected_errors.push_str(&format!( - "Artifact '{}' mismatch:\n{}\n", - file_name, err_msg - )); - } + Err(e) => collected_errors + .push_str(&format!("Artifact '{}' mismatch:\n{}\n", file_name, e)), } } @@ -1351,53 +1545,89 @@ fn assert_artifacts_match( Ok(()) } -fn assert_directories_match(expected: &Path, actual: &Path) -> io::Result<()> { +fn artifact_path_matches(expected: &Path, actual: &Path) -> Result<(), String> { + if actual.is_dir() != expected.is_dir() { + return Err(format!( + "Type mismatch: expected {:?} (is_dir: {}), actual {:?} (is_dir: {})", + expected, + expected.is_dir(), + actual, + actual.is_dir() + )); + } + + if actual.is_dir() { + directories_match(expected, actual) + } else { + files_match(expected, actual) + } +} + +fn files_match(expected: &Path, actual: &Path) -> Result<(), String> { + let e_txt = fs::read_to_string(expected) + .map_err(|e| format!("Failed to read expected file {:?}: {}", expected, e))? + .replace("\r\n", "\n"); + let a_txt = fs::read_to_string(actual) + .map_err(|e| format!("Failed to read actual file {:?}: {}", actual, e))? + .replace("\r\n", "\n"); + if e_txt != a_txt { + return Err(format!("Mismatch in {:?}:\n{}", expected, diff_text(&e_txt, &a_txt))); + } + Ok(()) +} + +fn directories_match(expected: &Path, actual: &Path) -> Result<(), String> { for entry in new_sorted_walkdir(expected) { - let entry = entry.map_err(io::Error::other)?; + let entry = entry.map_err(|e| e.to_string())?; if !entry.file_type().is_file() { continue; } let rel = entry.path().strip_prefix(expected).unwrap(); let act = actual.join(rel); if !act.exists() { - panic!( + return Err(format!( "Missing file in actual artifact:\nExpected: {:?}\nActual is missing: {:?}", entry.path(), act - ); + )); } - let e_txt = fs::read_to_string(entry.path())?.replace("\r\n", "\n"); - let a_txt = fs::read_to_string(&act)?.replace("\r\n", "\n"); - if e_txt != a_txt { - use similar::{ChangeTag, TextDiff}; - let diff = TextDiff::from_lines(&e_txt, &a_txt); - let mut diff_str = String::new(); - for change in diff.iter_all_changes() { - let sign = match change.tag() { - ChangeTag::Delete => "-", - ChangeTag::Insert => "+", - ChangeTag::Equal => " ", - }; - diff_str.push_str(&format!("{sign}{change}")); - } - panic!("Mismatch in {:?}:\n{}", rel, diff_str); + if let Err(e) = files_match(entry.path(), &act) { + return Err(format!("Mismatch in {:?}:\n{}", rel, e)); } } // Check for extra files in actual for entry in new_sorted_walkdir(actual) { - let entry = entry.map_err(io::Error::other)?; + let entry = entry.map_err(|e| e.to_string())?; if !entry.file_type().is_file() { continue; } let rel = entry.path().strip_prefix(actual).unwrap(); let exp = expected.join(rel); if !exp.exists() { - panic!("Extra file found in actual artifact that is not in expected:\n{:?}", rel); + return Err(format!( + "Extra file found in actual artifact that is not in expected:\n{:?}", + rel + )); } } Ok(()) } +fn diff_text(expected: &str, actual: &str) -> String { + use similar::{ChangeTag, TextDiff}; + let diff = TextDiff::from_lines(expected, actual); + let mut diff_str = String::new(); + for change in diff.iter_all_changes() { + let sign = match change.tag() { + ChangeTag::Delete => "-", + ChangeTag::Insert => "+", + ChangeTag::Equal => " ", + }; + diff_str.push_str(&format!("{sign}{change}")); + } + diff_str +} + fn copy_dir_contents(src: &Path, dst: &Path) -> io::Result<()> { fs::create_dir_all(dst)?; for entry in fs::read_dir(src)? { @@ -1426,7 +1656,6 @@ fn copy_dir_contents(src: &Path, dst: &Path) -> io::Result<()> { // - Lock-waiting messages from Cargo or other tools (removed) // - Hexadecimal hashes in file paths or versions (replaced with ``) // - Execution timings (replaced with `