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 `