diff --git a/.github/workflows/anneal.yml b/.github/workflows/anneal.yml index e93649fd14..c30a4b8d3d 100644 --- a/.github/workflows/anneal.yml +++ b/.github/workflows/anneal.yml @@ -286,7 +286,7 @@ jobs: 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 }} @@ -471,6 +471,100 @@ jobs: fi fi + v2_nix_cache: + name: Warm Nix Cache for V2 + 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 + + - 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 below? + - 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 + 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 + + 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] + 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 + + - 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 + + # 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 + # reproducible instead of following whatever nightly happens to be latest. + - name: Install latest nightly Rust + uses: dtolnay/rust-toolchain@e97e2d8cc328f1b50210efc529dca0028893a2d9 # zizmor: ignore[superfluous-actions] + with: + toolchain: nightly + + - name: Run V2 tests + run: cargo test --workspace --all-features # include, e.g., tests that assume exocrate prebuilt + working-directory: anneal/v2 # Used to signal to branch protections that all other jobs have succeeded. all-jobs-succeed: @@ -485,7 +579,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] + needs: [build_docker_env, anneal_tests, verify_examples, measure_image_size, v2_nix_cache, v2] steps: - name: Mark the job as failed run: exit 1 diff --git a/anneal/v2/Cargo.lock b/anneal/v2/Cargo.lock index 502d942e23..d15da17a08 100644 --- a/anneal/v2/Cargo.lock +++ b/anneal/v2/Cargo.lock @@ -8,6 +8,65 @@ version = "2.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "320119579fcad9c21884f5c4861d16174d0e06250625266f50fe6898340abefa" +[[package]] +name = "aho-corasick" +version = "1.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ddd31a130427c27518df266943a5308ed92d4b226cc639f5a8f1002816174301" +dependencies = [ + "memchr", +] + +[[package]] +name = "anstream" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "824a212faf96e9acacdbd09febd34438f8f711fb84e09a8916013cd7815ca28d" +dependencies = [ + "anstyle", + "anstyle-parse", + "anstyle-query", + "anstyle-wincon", + "colorchoice", + "is_terminal_polyfill", + "utf8parse", +] + +[[package]] +name = "anstyle" +version = "1.0.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "940b3a0ca603d1eade50a4846a2afffd5ef57a9feac2c0e2ec2e14f9ead76000" + +[[package]] +name = "anstyle-parse" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "52ce7f38b242319f7cabaa6813055467063ecdc9d355bbb4ce0c68908cd8130e" +dependencies = [ + "utf8parse", +] + +[[package]] +name = "anstyle-query" +version = "1.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "40c48f72fd53cd289104fc64099abca73db4166ad86ea0b4341abe65af83dadc" +dependencies = [ + "windows-sys 0.61.2", +] + +[[package]] +name = "anstyle-wincon" +version = "3.0.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "291e6a250ff86cd4a820112fb8898808a366d8f9f58ce16d1f538353ad55747d" +dependencies = [ + "anstyle", + "once_cell_polyfill", + "windows-sys 0.61.2", +] + [[package]] name = "anyhow" version = "1.0.102" @@ -45,7 +104,10 @@ checksum = "1e748733b7cbc798e1434b6ac524f0c1ff2ab456fe201501e6497c8417a4fc33" name = "cargo-anneal" version = "0.1.0-alpha.22" dependencies = [ + "clap", + "env_logger", "exocrate", + "log", "toml_const", ] @@ -67,6 +129,52 @@ version = "1.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" +[[package]] +name = "clap" +version = "4.6.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ddb117e43bbf7dacf0a4190fef4d345b9bad68dfc649cb349e7d17d28428e51" +dependencies = [ + "clap_builder", + "clap_derive", +] + +[[package]] +name = "clap_builder" +version = "4.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "714a53001bf66416adb0e2ef5ac857140e7dc3a0c48fb28b2f10762fc4b5069f" +dependencies = [ + "anstream", + "anstyle", + "clap_lex", + "strsim", +] + +[[package]] +name = "clap_derive" +version = "4.6.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f2ce8604710f6733aa641a2b3731eaa1e8b3d9973d5e3565da11800813f997a9" +dependencies = [ + "heck", + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "clap_lex" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c8d4a3bb8b1e0c1050499d1815f5ab16d04f0959b233085fb31653fbfc9d98f9" + +[[package]] +name = "colorchoice" +version = "1.0.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1d07550c9036bf2ae0c684c4297d503f838287c83c53686d05370d0e139ae570" + [[package]] name = "const-oid" version = "0.10.2" @@ -132,6 +240,29 @@ dependencies = [ "windows-sys 0.61.2", ] +[[package]] +name = "env_filter" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32e90c2accc4b07a8456ea0debdc2e7587bdd890680d71173a15d4ae604f6eef" +dependencies = [ + "log", + "regex", +] + +[[package]] +name = "env_logger" +version = "0.11.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0621c04f2196ac3f488dd583365b9c09be011a4ab8b9f37248ffcc8f6198b56a" +dependencies = [ + "anstream", + "anstyle", + "env_filter", + "jiff", + "log", +] + [[package]] name = "equivalent" version = "1.0.2" @@ -312,12 +443,42 @@ dependencies = [ "serde_core", ] +[[package]] +name = "is_terminal_polyfill" +version = "1.70.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a6cb138bb79a146c1bd460005623e142ef0181e3d0219cb493e02f7d08a35695" + [[package]] name = "itoa" version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" +[[package]] +name = "jiff" +version = "0.2.27" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "392c70591e8749fe235ddaf513e6f58b26bce3dcc16524cecc8936f75afa161e" +dependencies = [ + "jiff-static", + "log", + "portable-atomic", + "portable-atomic-util", + "serde_core", +] + +[[package]] +name = "jiff-static" +version = "0.2.27" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "47b605b0c050d845fc355bb11eb3f9a8deddc218ea60c76e61aa1f2adfb2c96a" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "jobserver" version = "0.1.34" @@ -342,9 +503,9 @@ checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66" [[package]] name = "libredox" -version = "0.1.16" +version = "0.1.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e02f3bb43d335493c96bf3fd3a321600bf6bd07ed34bc64118e9293bdffea46c" +checksum = "f02ab6bace2054fb888a3c16f990117b579d14a3088e472d63c6011fa185c9d3" dependencies = [ "libc", ] @@ -363,9 +524,9 @@ checksum = "616ec5685824bcc94416c6d4a7a446eea774a31efd7062c8480ba6fd06d7a6e5" [[package]] name = "memchr" -version = "2.8.0" +version = "2.8.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f8ca58f447f06ed17d5fc4043ce1b10dd205e060fb3ce5b979b8ed8e59ff3f79" +checksum = "6b947ae49db0d222b1dbc6b113ce7248a3fc3a6ca21b696717bfc000ba4484d8" [[package]] name = "miniz_oxide" @@ -383,6 +544,12 @@ version = "1.21.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9f7c3e4beb33f85d45ae3e3a1792185706c8e16d043238c593331cc7cd313b50" +[[package]] +name = "once_cell_polyfill" +version = "1.70.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "384b8ab6d37215f3c5301a95a4accb5d64aa607f1fcb26a11b5303878451b4fe" + [[package]] name = "option-ext" version = "0.2.0" @@ -444,6 +611,21 @@ version = "0.3.33" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "19f132c84eca552bf34cab8ec81f1c1dcc229b811638f9d283dceabe58c5569e" +[[package]] +name = "portable-atomic" +version = "1.13.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c33a9471896f1c69cecef8d20cbe2f7accd12527ce60845ff44c153bb2a21b49" + +[[package]] +name = "portable-atomic-util" +version = "0.2.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c2a106d1259c23fac8e543272398ae0e3c0b8d33c88ed73d0cc71b0f1d902618" +dependencies = [ + "portable-atomic", +] + [[package]] name = "prettyplease" version = "0.2.37" @@ -495,6 +677,35 @@ dependencies = [ "thiserror", ] +[[package]] +name = "regex" +version = "1.12.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e10754a14b9137dd7b1e3e5b0493cc9171fdd105e0ab477f51b72e7f3ac0e276" +dependencies = [ + "aho-corasick", + "memchr", + "regex-automata", + "regex-syntax", +] + +[[package]] +name = "regex-automata" +version = "0.4.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6e1dd4122fc1595e8162618945476892eefca7b88c52820e74af6262213cae8f" +dependencies = [ + "aho-corasick", + "memchr", + "regex-syntax", +] + +[[package]] +name = "regex-syntax" +version = "0.8.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dc897dd8d9e8bd1ed8cdad82b5966c3e0ecae09fb1907d58efaa013543185d0a" + [[package]] name = "ring" version = "0.17.14" @@ -649,6 +860,12 @@ version = "1.0.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8ee5873ec9cce0195efcb7a4e9507a04cd49aec9c83d0389df45b1ef7ba2e649" +[[package]] +name = "strsim" +version = "0.11.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f" + [[package]] name = "subtle" version = "2.6.1" @@ -832,6 +1049,12 @@ version = "0.8.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b8c0a043c9540bae7c578c88f91dda8bd82e59ae27c21baca69c8b191aaf5a6e" +[[package]] +name = "utf8parse" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821" + [[package]] name = "wasi" version = "0.11.1+wasi-snapshot-preview1" diff --git a/anneal/v2/Cargo.toml b/anneal/v2/Cargo.toml index 741514e3ca..853b7f7f5c 100644 --- a/anneal/v2/Cargo.toml +++ b/anneal/v2/Cargo.toml @@ -1,6 +1,10 @@ [workspace] members = ["."] +[features] +# Enables tests that assume a prebuilt exocrate archive. +exocrate_tests = [] + [package] name = "cargo-anneal" edition = "2024" @@ -21,6 +25,9 @@ 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" @@ -40,3 +47,6 @@ url = "https://example.com/macos-aarch64.tar.zst" [dependencies] exocrate = { path = "../../exocrate" } toml_const = "1.3.0" +clap = { version = "4.5", features = ["derive"] } +env_logger = "0.11" +log = "0.4" diff --git a/anneal/v2/chase-aeneas-versions.sh b/anneal/v2/chase-aeneas-versions.sh new file mode 100755 index 0000000000..98dc4eeada --- /dev/null +++ b/anneal/v2/chase-aeneas-versions.sh @@ -0,0 +1,229 @@ +#!/usr/bin/env bash +# Chase the version inputs that are coupled to an Aeneas release asset. + +set -euo pipefail + +usage() { + cat >&2 <<'USAGE' +usage: chase-aeneas-versions.sh RELEASE_TAG [--target linux-x86_64] [--work-dir DIR] [--keep] + +Downloads an Aeneas release archive, extracts the Lean and Rust toolchain +versions it was built against, and computes the recursive Nix hashes used by +flake.nix for the matching Lean and Rust toolchain directories. + +The mathlib-cache-download output hash depends on Lake's CDN cache result and +is reported as a follow-up Nix fixed-output hash to refresh after these values. +USAGE +} + +target=linux-x86_64 +work_dir= +keep=0 + +if [[ $# -lt 1 ]]; then + usage + exit 2 +fi + +release_tag=$1 +shift + +while [[ $# -gt 0 ]]; do + case "$1" in + --target) + target=${2:?missing --target value} + shift 2 + ;; + --work-dir) + work_dir=${2:?missing --work-dir value} + shift 2 + ;; + --keep) + keep=1 + shift + ;; + -h|--help) + usage + exit 0 + ;; + *) + echo "unknown argument: $1" >&2 + usage + exit 2 + ;; + esac +done + +case "$target" in + linux-x86_64) + rust_platform=x86_64-unknown-linux-gnu + lean_platform=linux + ;; + linux-aarch64) + rust_platform=aarch64-unknown-linux-gnu + lean_platform=linux_aarch64 + ;; + macos-x86_64) + rust_platform=x86_64-apple-darwin + lean_platform=darwin + ;; + macos-aarch64) + rust_platform=aarch64-apple-darwin + lean_platform=darwin_aarch64 + ;; + *) + echo "unsupported Aeneas target: $target" >&2 + exit 2 + ;; +esac + +need() { + command -v "$1" >/dev/null 2>&1 || { + echo "required command not found: $1" >&2 + exit 1 + } +} + +need curl +need sha256sum +need tar +need zstd +need strings +need date +need nix + +if [[ -z "$work_dir" ]]; then + work_dir=$(mktemp -d) +else + mkdir -p "$work_dir" +fi + +cleanup() { + if [[ "$keep" -eq 0 ]]; then + rm -rf "$work_dir" + else + echo "kept work directory: $work_dir" >&2 + fi +} +trap cleanup EXIT + +download() { + local url=$1 + local dst=$2 + if [[ ! -f "$dst" ]]; then + echo "downloading $url" >&2 + curl -fL --retry 3 --retry-delay 2 -o "$dst" "$url" + fi +} + +hash_path_sri() { + nix hash path --type sha256 --sri "$1" +} + +aeneas_archive="$work_dir/aeneas-$target.tar.gz" +aeneas_url="https://github.com/AeneasVerif/aeneas/releases/download/$release_tag/aeneas-$target.tar.gz" +download "$aeneas_url" "$aeneas_archive" +aeneas_sha256_hex=$(sha256sum "$aeneas_archive" | awk '{print $1}') + +extract_dir="$work_dir/aeneas" +mkdir -p "$extract_dir" +tar -xzf "$aeneas_archive" -C "$extract_dir" + +lean_toolchain_file="$extract_dir/backends/lean/lean-toolchain" +if [[ ! -f "$lean_toolchain_file" ]]; then + echo "Aeneas archive did not contain backends/lean/lean-toolchain" >&2 + exit 1 +fi + +lean_raw=$(tr -d '\n' < "$lean_toolchain_file") +lean_version=${lean_raw#leanprover/lean4:} +lean_raw_version=${lean_version#v} + +charon_bin="$extract_dir/charon" +if [[ ! -f "$charon_bin" ]]; then + echo "Aeneas archive did not contain charon" >&2 + exit 1 +fi + +commit_date=$( + strings "$charon_bin" | + grep -o 'rustc version .* ([0-9a-f]\{9\} [0-9]\{4\}-[0-9]\{2\}-[0-9]\{2\})' | + head -n 1 | + grep -o '[0-9]\{4\}-[0-9]\{2\}-[0-9]\{2\}' | + tr -d '\n' +) + +if [[ -z "$commit_date" ]]; then + echo "could not infer Rust commit date from charon binary" >&2 + exit 1 +fi + +# FIXME: This requires GNU date. macOS targets above are valid release targets, +# but the host script itself will fail on BSD date until this date arithmetic is +# made portable. +rust_date=$(date -d "$commit_date + 1 day" +%Y-%m-%d) + +lean_dir="$work_dir/lean-toolchain" +mkdir -p "$lean_dir" +lean_archive="$work_dir/lean-$lean_raw_version-$lean_platform.tar.zst" +lean_url="https://releases.lean-lang.org/lean4/$lean_version/lean-$lean_raw_version-$lean_platform.tar.zst" +download "$lean_url" "$lean_archive" +zstd -dc "$lean_archive" | tar -x -C "$lean_dir" --strip-components=1 +lean_output_hash=$(hash_path_sri "$lean_dir") + +rust_dir="$work_dir/rust-toolchain" +mkdir -p "$rust_dir" +for component in rustc rust-std rustc-dev llvm-tools miri; do + archive="$work_dir/$component-nightly-$rust_platform.tar.gz" + url="https://static.rust-lang.org/dist/$rust_date/$component-nightly-$rust_platform.tar.gz" + download "$url" "$archive" + tmp_extract="$work_dir/extract-$component" + rm -rf "$tmp_extract" + mkdir -p "$tmp_extract" + tar -xzf "$archive" -C "$tmp_extract" + top_dir=$(find "$tmp_extract" -mindepth 1 -maxdepth 1 -type d | head -n 1) + comp_dir=$(find "$top_dir" -mindepth 1 -maxdepth 1 -type d | head -n 1) + cp -R "$comp_dir"/. "$rust_dir"/ +done + +rust_src_archive="$work_dir/rust-src-nightly.tar.gz" +download "https://static.rust-lang.org/dist/$rust_date/rust-src-nightly.tar.gz" "$rust_src_archive" +tmp_extract="$work_dir/extract-rust-src" +rm -rf "$tmp_extract" +mkdir -p "$tmp_extract" +tar -xzf "$rust_src_archive" -C "$tmp_extract" +top_dir=$(find "$tmp_extract" -mindepth 1 -maxdepth 1 -type d | head -n 1) +cp -R "$top_dir/rust-src"/. "$rust_dir"/ +rust_output_hash=$(hash_path_sri "$rust_dir") + +mathlib_rev=$( + grep -A2 'require mathlib from git' "$extract_dir/backends/lean/lakefile.lean" | + grep -o '@ "[^"]*"' | + sed -E 's/@ "([^"]*)"/\1/' | + head -n 1 +) + +cat < $out/metadata.json" + "{" + " \"lean-toolchain\": \"\$LEAN_VERSION\"," + " \"rust-toolchain-date\": \"\$RUST_DATE\"," + " \"rust-toolchain-version\": \"\$RUST_VERSION\"" + "}" + "EOF" + ]; + }; + + # Minimal project metadata used to fetch the Mathlib cache. + packages.aeneas-metadata-files = pkgs.stdenv.mkDerivation { + pname = "aeneas-metadata-files"; + version = "1.0.0"; + + src = self.packages.${system}.aeneas-download-linux-x86_64; + + nativeBuildInputs = with pkgs; [ + gnutar + gzip + ]; + + dontUnpack = true; + + buildPhase = builtins.concatStringsSep "\n" [ + "mkdir -p $out" + "tar -xzf $src -C $out --strip-components=2 \\" + " backends/lean/lakefile.lean \\" + " backends/lean/lake-manifest.json \\" + " backends/lean/lean-toolchain" + ]; + }; + + # Fetches Mathlib's precompiled Lake cache in a fixed-output derivation. + packages.mathlib-cache-download = pkgs.stdenv.mkDerivation { + pname = "mathlib-cache-download"; + version = "0.1.0"; + + dontUnpack = true; + + # Preserve downloaded artifacts exactly. + dontPatchShebangs = true; + dontPatchELF = true; + dontStrip = true; + + outputHashMode = "recursive"; + outputHashAlgo = "sha256"; + outputHash = "sha256-tj5BeYGWSmXvYdzChrqaG9aN7so/+jAM5qWPI8tcN6U="; + + leanToolchainRaw = self.packages.${system}.lean-toolchain; + metadataFiles = self.packages.${system}.aeneas-metadata-files; + + nativeBuildInputs = with pkgs; [ + git + steam-run + gnutar + zstd + curl + cacert + ]; + + SSL_CERT_FILE = "${pkgs.cacert}/etc/ssl/certs/ca-bundle.crt"; + + buildPhase = builtins.concatStringsSep "\n" [ + "export HOME=$TMPDIR" + "mkdir -p project" + "cp $metadataFiles/lakefile.lean project/" + "cp $metadataFiles/lake-manifest.json project/" + "cp $metadataFiles/lean-toolchain project/" + "cd project" + "export PATH=\"$leanToolchainRaw/bin:${pkgs.git}/bin:${pkgs.curl}/bin:\$PATH\"" + "export LEAN_SYSROOT=\"$leanToolchainRaw\"" + "steam-run $leanToolchainRaw/bin/lake exe cache get" + ]; + + installPhase = builtins.concatStringsSep "\n" [ + "mkdir -p $out/cache/mathlib" + "cp -r $TMPDIR/.cache/mathlib/* $out/cache/mathlib/" + "mkdir -p $out/packages" + "cp -r .lake/packages/* $out/packages/" + "chmod -R +w $out/packages" + # Drop only traces that captured Nix store paths. + "find $out/packages -type f \\( -name \"*.trace\" -o -name \"*.hash\" \\) \\" + " -exec grep -q \"/nix/store\" {} \\; -delete" + # Mathlib's build cache is reconstructed from .ltar archives below. + "rm -rf $out/packages/mathlib/.lake" + # Git metadata is unnecessary for path dependencies. + "find $out/packages -type d -name \".git\" -exec rm -rf {} +" + ]; + }; + + # Unpacks Mathlib's precompiled .ltar archives. + packages.mathlib-cache-unpacked = pkgs.stdenv.mkDerivation { + pname = "mathlib-cache-unpacked"; + version = "0.1.0"; + + src = pkgs.runCommand "empty-src" {} "mkdir $out"; + + mathlibCache = self.packages.${system}.mathlib-cache-download; + leanToolchain = self.packages.${system}.lean-toolchain; + + nativeBuildInputs = with pkgs; [ + gnutar + zstd + ]; + + buildPhase = builtins.concatStringsSep "\n" [ + "mkdir -p $out/packages" + "cp -r $mathlibCache/packages/* $out/packages/" + "chmod -R +w $out/packages" + "LEANTAR_BIN=\$(find $mathlibCache/cache/mathlib -name \"leantar-*\" -type f -executable | head -n 1)" + "if [ -z \"\$LEANTAR_BIN\" ] && [ -x \"$leanToolchain/bin/leantar\" ]; then" + " LEANTAR_BIN=\"$leanToolchain/bin/leantar\"" + "fi" + "if [ -z \"\$LEANTAR_BIN\" ]; then" + " echo \"ERROR: leantar utility binary not found in mathlib cache or Lean toolchain!\"" + " exit 1" + "fi" + "echo \"Using leantar binary at: \$LEANTAR_BIN\"" + # Each archive expands into the project-wide .lake/build tree. + "find $mathlibCache/cache/mathlib -name \"*.ltar\" -print0 | \\" + " xargs -0 -n 1 -P 48 bash -c \"\$LEANTAR_BIN -d -C $out \\\"\\\$0\\\"\"" + # Keep the release archive reproducible. + "find $out -exec touch -h -d \"1970-01-01 00:00:00\" {} +" + ]; + }; + + # Builds the Aeneas Lean backend against vendored, relative Lake paths. + packages.aeneas-compiled = pkgs.stdenv.mkDerivation { + pname = "aeneas-compiled"; + version = "0.1.0"; + + src = pkgs.runCommand "empty-src" {} "mkdir $out"; + + leanToolchain = self.packages.${system}.lean-toolchain; + mathlibCache = self.packages.${system}.mathlib-cache-unpacked; + aeneasUnpacked = self.packages.${system}.aeneas-unpacked; + + nativeBuildInputs = with pkgs; [ + python3 + steam-run + gnutar + zstd + ]; + + buildPhase = builtins.concatStringsSep "\n" [ + "export HOME=$TMPDIR" + "export PATH=\"$leanToolchain/bin:\$PATH\"" + "export LEAN_SYSROOT=\"$leanToolchain\"" + # Let sandboxed Lean executables find libleanshared.so. + "export LD_LIBRARY_PATH=\"$leanToolchain/lib:$leanToolchain/lib/lean:\$LD_LIBRARY_PATH\"" + # The cache was fetched in the FOD; do not fetch it again here. + "export MATHLIB_NO_CACHE_ON_UPDATE=1" + "mkdir -p aeneas/backends aeneas/packages" + "cp -r $aeneasUnpacked/backends/lean aeneas/backends/lean" + "chmod -R +w aeneas" + "cd aeneas/backends/lean" + "cp -r $mathlibCache/packages/* ../../packages/" + "chmod -R +w ../../packages" + # Seed the project-wide build cache from unpacked Mathlib archives. + "mkdir -p .lake" + "cp -r $mathlibCache/.lake/build .lake/" + "chmod -R +w .lake" + # Copy global prebuilts into each path dependency for offline replay. + '' + python3 << 'EOF' + import os + import shutil + import re + + def discover_library_name(pkg_dir, dir_name): + toml_path = os.path.join(pkg_dir, "lakefile.toml") + if os.path.exists(toml_path): + with open(toml_path, "r") as f: + content = f.read() + match = re.search(r"\[{1,2}lean_lib\]{1,2}(?:\s*\n|[^\[\]])*?name\s*=\s*\"([^\"]+)\"", content) + if match: + return match.group(1) + match = re.search(r"^\s*name\s*=\s*\"([^\"]+)\"", content, re.MULTILINE) + if match: + return match.group(1).capitalize() + + lean_path = os.path.join(pkg_dir, "lakefile.lean") + if os.path.exists(lean_path): + with open(lean_path, "r") as f: + content = f.read() + match = re.search(r"lean_lib\s+(?:«([^»]+)»|\"([^\"]+)\"|([a-zA-Z0-9._-]+))", content) + if match: + return match.group(1) or match.group(2) or match.group(3) + match = re.search(r"package\s+(?:«([^»]+)»|\"([^\"]+)\"|([a-zA-Z0-9._-]+))", content) + if match: + val = match.group(1) or match.group(2) or match.group(3) + return val.capitalize() + + return dir_name.capitalize() + + global_cache = os.path.join(os.getcwd(), ".lake", "build") + packages_dir = os.path.abspath("../../packages") + + if os.path.exists(packages_dir): + for dir_name in os.listdir(packages_dir): + pkg_dir = os.path.join(packages_dir, dir_name) + if not os.path.isdir(pkg_dir): continue + pkg_name = discover_library_name(pkg_dir, dir_name) + dest_lib_dir = os.path.join(pkg_dir, ".lake", "build", "lib", "lean") + os.makedirs(dest_lib_dir, exist_ok=True) + src_lib_dir = os.path.join(global_cache, "lib", "lean", pkg_name) + if os.path.exists(src_lib_dir): + shutil.copytree(src_lib_dir, os.path.join(dest_lib_dir, pkg_name), dirs_exist_ok=True) + src_root_lib_dir = os.path.join(global_cache, "lib", "lean") + if os.path.exists(src_root_lib_dir): + for f in os.listdir(src_root_lib_dir): + if f.startswith(pkg_name + "."): + shutil.copy2(os.path.join(src_root_lib_dir, f), dest_lib_dir) + dest_ir_dir = os.path.join(pkg_dir, ".lake", "build", "ir") + src_ir_dir = os.path.join(global_cache, "ir", pkg_name) + if os.path.exists(src_ir_dir): + os.makedirs(dest_ir_dir, exist_ok=True) + shutil.copytree(src_ir_dir, os.path.join(dest_ir_dir, pkg_name), dirs_exist_ok=True) + EOF + '' + "python3 ${./rewrite-lake-vendor.py} --root . --packages-dir ../../packages" + "steam-run lake build" + "python3 ${./rewrite-lake-vendor.py} --root . --packages-dir ../../packages --rewrite-traces" + # Prune unused Lean modules and bulky upstream metadata. + '' + python3 << 'EOF' + import os + import shutil + + def prune_package(pkg_dir): + print(f"Pruning package at: {pkg_dir}") + traces_dir = os.path.join(pkg_dir, ".lake", "build", "lib", "lean") + if not os.path.exists(traces_dir): + print(f"No build traces found for {pkg_dir}, skipping pruning.") + return + used_modules = set() + for root, dirs, files in os.walk(traces_dir): + for file in files: + if file.endswith(".trace"): + abs_trace = os.path.join(root, file) + rel_trace = os.path.relpath(abs_trace, traces_dir) + mod_path = os.path.splitext(rel_trace)[0] + used_modules.add(mod_path) + print(f" - Found {len(used_modules)} used modules.") + all_lean_files = [] + for root, dirs, files in os.walk(pkg_dir): + if ".lake" in os.path.split(root)[1] or ".git" in os.path.split(root)[1]: + continue + for file in files: + if file.endswith(".lean"): + abs_lean = os.path.join(root, file) + rel_lean = os.path.relpath(abs_lean, pkg_dir) + all_lean_files.append(rel_lean) + print(f" - Found {len(all_lean_files)} total .lean files.") + unused_count = 0 + for rel_lean in all_lean_files: + if rel_lean == "lakefile.lean": + continue + mod_path = os.path.splitext(rel_lean)[0] + if mod_path not in used_modules: + abs_lean = os.path.join(pkg_dir, rel_lean) + os.remove(abs_lean) + unused_count += 1 + for sub in ["lib/lean", "ir"]: + sub_dir = os.path.join(pkg_dir, ".lake", "build", sub) + if os.path.exists(sub_dir): + mod_dir = os.path.join(sub_dir, os.path.dirname(mod_path)) + mod_name = os.path.basename(mod_path) + if os.path.exists(mod_dir): + for f in os.listdir(mod_dir): + if f.startswith(mod_name + "."): + os.remove(os.path.join(mod_dir, f)) + print(f" - Deleted {unused_count} unused .lean files and their build artifacts.") + meta_names = [".gitignore", ".gitattributes", "README.md", "LICENSE", "bors.toml", ".pre-commit-config.yaml", ".gitpod.yml"] + for name in meta_names: + p = os.path.join(pkg_dir, name) + if os.path.exists(p): os.remove(p) + meta_dirs = [".github", ".vscode", ".devcontainer", ".docker", "docs", "tests", "test"] + for name in meta_dirs: + p = os.path.join(pkg_dir, name) + if os.path.exists(p): shutil.rmtree(p, ignore_errors=True) + for root, dirs, files in os.walk(pkg_dir): + for file in files: + if file.endswith(".ltar"): os.remove(os.path.join(root, file)) + for root, dirs, files in os.walk(pkg_dir, topdown=False): + if root == pkg_dir: continue + if not os.listdir(root): os.rmdir(root) + + packages_root = os.path.abspath("../../packages") + if os.path.exists(packages_root): + for name in os.listdir(packages_root): + pkg_dir = os.path.join(packages_root, name) + if os.path.isdir(pkg_dir): + prune_package(pkg_dir) + + root_mathlib_build = os.path.join(os.getcwd(), ".lake", "build", "lib", "lean", "Mathlib") + if os.path.exists(root_mathlib_build): + print("Deleting root Mathlib build cache...") + shutil.rmtree(root_mathlib_build) + lib_lean_dir = os.path.join(os.getcwd(), ".lake", "build", "lib", "lean") + if os.path.exists(lib_lean_dir): + for f in os.listdir(lib_lean_dir): + if f.startswith("Mathlib."): + os.remove(os.path.join(lib_lean_dir, f)) + EOF + '' + "cd ../.." + "mkdir -p $out/backends $out/packages" + "cp -r backends/lean $out/backends/" + "cp -r packages/* $out/packages/" + "mkdir -p $out/bin" + "cp \$(find $aeneasUnpacked -maxdepth 1 -type f -executable) $out/bin/" + ]; + }; + + # Stages the relocatable toolchain bundle before compression. + packages.omnibus-tar = pkgs.stdenv.mkDerivation { + pname = "anneal-toolchain-omnibus-tar"; + version = "0.1.0"; + + src = pkgs.runCommand "empty-src" {} "mkdir $out"; + + nativeBuildInputs = with pkgs; [ + patchelf + file + gnutar + ]; + + aeneasBuild = self.packages.${system}.aeneas-compiled; + rustToolchain = self.packages.${system}.rust-toolchain; + leanToolchain = self.packages.${system}.lean-toolchain; + + buildPhase = builtins.concatStringsSep "\n" [ + "mkdir -p $TMPDIR/dist_staging" + "chmod -R +w $TMPDIR/dist_staging/" + "mkdir -p $TMPDIR/dist_staging/lean" + "cp -r $leanToolchain/* $TMPDIR/dist_staging/lean/" + "chmod -R +w $TMPDIR/dist_staging/lean" + "mkdir -p $TMPDIR/dist_staging/rust" + "cp -r $rustToolchain/* $TMPDIR/dist_staging/rust/" + "chmod -R +w $TMPDIR/dist_staging/rust" + "mkdir -p $TMPDIR/dist_staging/aeneas" + "cp -r $aeneasBuild/* $TMPDIR/dist_staging/aeneas/" + "chmod -R +w $TMPDIR/dist_staging/aeneas" + # Remove Nix dynamic-linker and RPATH references from ELF binaries. + "echo \"Cleaning up Nix store references...\"" + "find $TMPDIR/dist_staging -type f -executable | while read -r file; do" + " if file \"\$file\" | grep -q \"ELF 64-bit\"; then" + " echo \"Patching and stripping \$file...\"" + " if patchelf --print-interpreter \"\$file\" >/dev/null 2>&1; then" + " patchelf --set-interpreter /lib64/ld-linux-x86-64.so.2 \"\$file\" || true" + " fi" + " patchelf --set-rpath \"\" \"\$file\" || true" + " strip \"\$file\" || true" + " fi" + "done" + # Leave one stable placeholder for any residual absolute trace paths. + "echo \"Inserting relocatable placeholders inside trace files...\"" + "find $TMPDIR/dist_staging -type f -name \"*.trace\" | while read -r trace_file; do" + " substituteInPlace \"\$trace_file\" \\" + " --replace \"/build/aeneas/packages\" \"/ANNEAL_PLACEHOLDER_ROOT/aeneas/packages\" \\" + " --replace \"/build/aeneas/backends/lean\" \"/ANNEAL_PLACEHOLDER_ROOT/aeneas/backends/lean\"" + "done" + "chmod -R a-w $TMPDIR/dist_staging" + "cd $TMPDIR/dist_staging" + "tar -cf $out *" + ]; + }; + + # Final compressed toolchain archive. + packages.omnibus-archive = pkgs.stdenv.mkDerivation { + pname = "anneal-toolchain-omnibus"; + version = "0.1.0"; + + src = pkgs.runCommand "empty-src" {} "mkdir $out"; + + nativeBuildInputs = with pkgs; [ + zstd + ]; + + omnibusTar = self.packages.${system}.omnibus-tar; + + ANNEAL_ZSTD_LEVEL = 1; + + buildPhase = builtins.concatStringsSep "\n" [ + "ZSTD_LEVEL=\${ANNEAL_ZSTD_LEVEL:-1}" + "echo \"Compressing with Zstd level \$ZSTD_LEVEL...\"" + "zstd -\$ZSTD_LEVEL $omnibusTar -o $out" + ]; + }; + + packages.rust-toolchain = fetchRustToolchain { + rustDate = "2026-05-31"; + sha256 = "sha256-tdLBvDewiNTUKOdMJ1pkU7mPrUY0xTFOZWdG9dDNiAk="; + }; + + packages.lean-toolchain = fetchLeanToolchain { + leanVersion = "v4.30.0-rc2"; + sha256 = "sha256-o47cQjSLK5YL8YZ2raaj+mGAvvO+dIDfVeP2L+WoyMs="; + }; + + # Verifies that Aeneas metadata can drive toolchain derivations. + packages.test-ifd = + let + unpacked = self.packages.${system}.aeneas-unpacked; + + aeneasMetadata = builtins.fromJSON (builtins.readFile "${unpacked}/metadata.json"); + + leanVersion = aeneasMetadata.lean-toolchain; + rustVersion = aeneasMetadata.rust-toolchain-version; + rustDate = aeneasMetadata.rust-toolchain-date; + + dynamicRust = fetchRustToolchain { + inherit rustDate; + sha256 = self.packages.${system}.rust-toolchain.outputHash; + }; + + dynamicLean = fetchLeanToolchain { + inherit leanVersion; + sha256 = self.packages.${system}.lean-toolchain.outputHash; + }; + in + pkgs.runCommand "test-ifd-eval" {} (builtins.concatStringsSep "\n" [ + "echo \"Dynamic IFD Verification Success!\"" + "echo \"Extracted Lean Toolchain Version: ${leanVersion}\"" + "echo \"Extracted Rust Toolchain Version: ${rustVersion}\"" + "echo \"Dynamically Constructed Rust Toolchain Store Path: ${dynamicRust}\"" + "echo \"Dynamically Constructed Lean Toolchain Store Path: ${dynamicLean}\"" + "test -f ${dynamicRust}/bin/rustc" + "test -f ${dynamicLean}/bin/lean" + "echo \"Lean: ${leanVersion}, Rust: ${rustVersion}\" > $out" + "echo \"Wired Rust Toolchain: ${dynamicRust}\" >> $out" + "echo \"Wired Lean Toolchain: ${dynamicLean}\" >> $out" + ]); + + packages.default = self.packages.${system}.aeneas-unpacked; + }); +} diff --git a/anneal/v2/rewrite-lake-vendor.py b/anneal/v2/rewrite-lake-vendor.py new file mode 100755 index 0000000000..c943cb4d6f --- /dev/null +++ b/anneal/v2/rewrite-lake-vendor.py @@ -0,0 +1,175 @@ +#!/usr/bin/env python3 +"""Rewrite Lake dependencies to local vendored paths.""" + +from __future__ import annotations + +import argparse +import json +import os +import re +from pathlib import Path + + +REMOTE_TOML_KEYS = {"git", "url", "rev", "scope", "subDir", "inputRev"} + + +def quote_name(name: str) -> str: + if re.fullmatch(r"[A-Za-z_][A-Za-z0-9_']*", name): + return name + escaped = name.replace("\\", "\\\\").replace('"', '\\"') + return f'"{escaped}"' + + +def rel(from_file: Path, to_dir: Path) -> str: + return os.path.relpath(to_dir, from_file.parent) + + +def package_dirs(packages_dir: Path) -> dict[str, Path]: + return { + child.name: child + for child in packages_dir.iterdir() + if child.is_dir() and child.name != ".lake" + } + + +def replace_require_toml_blocks(path: Path, packages: dict[str, Path]) -> bool: + content = path.read_text() + block_re = re.compile(r"(?ms)^\s*\[\[require\]\]\s*\n(?:(?!^\s*\[\[).*\n?)*") + + changed = False + + def replace(match: re.Match[str]) -> str: + nonlocal changed + block = match.group(0) + name_match = re.search(r'(?m)^\s*name\s*=\s*"([^"]+)"\s*$', block) + if not name_match: + return block + name = name_match.group(1) + dep_dir = packages.get(name) + if dep_dir is None: + return block + if re.search(r'(?m)^\s*path\s*=', block) and not any(k in block for k in REMOTE_TOML_KEYS): + return block + + changed = True + return f'[[require]]\nname = "{name}"\npath = "{rel(path, dep_dir)}"\n' + + new_content = block_re.sub(replace, content) + if changed: + path.write_text(new_content) + return changed + + +def replace_require_lean(path: Path, packages: dict[str, Path]) -> bool: + content = path.read_text() + changed = False + + def local_req(name: str) -> str | None: + dep_dir = packages.get(name) + if dep_dir is None: + return None + return f'require {quote_name(name)} from "{rel(path, dep_dir)}"' + + patterns = [ + re.compile( + r'require\s+([A-Za-z_][A-Za-z0-9_\']*|«([^»]+)»|"([^"]+)")\s+from\s+git\s*\n\s*"[^"]+"\s*@\s*"[^"]+"' + ), + re.compile( + r'require\s+([A-Za-z_][A-Za-z0-9_\']*|«([^»]+)»|"([^"]+)")\s+from\s+git\s+"[^"]+"\s*@\s*"[^"]+"' + ), + re.compile(r'require\s+"[^"]+"\s*/\s*"([^"]+)"\s*@\s*git\s*"[^"]+"'), + ] + + for pattern in patterns: + + def replace(match: re.Match[str]) -> str: + nonlocal changed + name = next(group for group in match.groups() if group) + replacement = local_req(name) + if replacement is None: + return match.group(0) + changed = True + return replacement + + content = pattern.sub(replace, content) + + if changed: + path.write_text(content) + return changed + + +def rewrite_manifest(path: Path, packages: dict[str, Path]) -> bool: + data = json.loads(path.read_text()) + changed = False + rewritten = [] + + for pkg in data.get("packages", []): + name = pkg.get("name") + dep_dir = packages.get(name) + if dep_dir is None: + rewritten.append(pkg) + continue + + new_pkg = { + "type": "path", + "name": name, + "dir": rel(path, dep_dir), + "inherited": pkg.get("inherited", False), + } + if pkg != new_pkg: + changed = True + rewritten.append(new_pkg) + + if changed: + data["packages"] = rewritten + path.write_text(json.dumps(data, indent=2) + "\n") + return changed + + +def rewrite_trace_prefixes(root: Path, packages: dict[str, Path]) -> int: + prefixes = [(root.resolve(), ""), *((p.resolve(), "") for p in packages.values())] + count = 0 + + for trace in [*root.rglob("*.trace"), *(t for p in packages.values() for t in p.rglob("*.trace"))]: + try: + content = trace.read_text() + except UnicodeDecodeError: + continue + new_content = content + for prefix, replacement in prefixes: + new_content = new_content.replace(str(prefix) + os.sep, replacement) + if new_content != content: + trace.write_text(new_content) + count += 1 + return count + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("--root", type=Path, required=True, help="Root Lake package directory") + parser.add_argument("--packages-dir", type=Path, required=True, help="Vendored packages directory") + parser.add_argument( + "--rewrite-traces", + action="store_true", + help="Also strip package/root absolute prefixes from .trace files", + ) + args = parser.parse_args() + + root = args.root.resolve() + packages_dir = args.packages_dir.resolve() + packages = package_dirs(packages_dir) + + changed = 0 + for lakefile in [*root.rglob("lakefile.lean"), *packages_dir.rglob("lakefile.lean")]: + changed += int(replace_require_lean(lakefile, packages)) + for lakefile in [*root.rglob("lakefile.toml"), *packages_dir.rglob("lakefile.toml")]: + changed += int(replace_require_toml_blocks(lakefile, packages)) + for manifest in [*root.rglob("lake-manifest.json"), *packages_dir.rglob("lake-manifest.json")]: + changed += int(rewrite_manifest(manifest, packages)) + + trace_count = rewrite_trace_prefixes(root, packages) if args.rewrite_traces else 0 + print(f"rewrote {changed} Lake metadata files and {trace_count} trace files") + + +if __name__ == "__main__": + main() diff --git a/anneal/v2/src/main.rs b/anneal/v2/src/main.rs index 81b36137c2..d5b672d035 100644 --- a/anneal/v2/src/main.rs +++ b/anneal/v2/src/main.rs @@ -7,6 +7,29 @@ // This file may not be copied, modified, or distributed except according to // those terms. +use clap::Parser as _; + +/// Anneal +#[derive(clap::Parser, Debug)] +#[command(name = "cargo-anneal", version, about, long_about = None)] +struct Cli { + #[command(subcommand)] + command: Commands, +} + +#[derive(clap::Subcommand, Debug)] +enum Commands { + /// Setup Anneal dependencies + Setup(SetupArgs), +} + +#[derive(clap::Parser, Debug)] +pub struct SetupArgs { + /// Path to a local dependency archive to use instead of downloading. + #[arg(long, value_name = "path-to-local-archive")] + pub local_archive: Option, +} + exocrate::config! { const CONFIG: Config = Config { rel_dir_path: [".anneal", "toolchain"], @@ -23,4 +46,51 @@ exocrate::parse_remote_archive! { ]; } -fn main() {} +fn setup(args: SetupArgs) { + let location = if std::env::var("__ANNEAL_LOCAL_DEV").is_ok() { + exocrate::Location::LocalDev + } else { + exocrate::Location::UserGlobal + }; + let source = match args.local_archive { + Some(local_archive) => exocrate::Source::Local(local_archive), + None => exocrate::Source::Remote(REMOTE), + }; + + let installation_dir = CONFIG + .resolve_installation_dir_or_install(location, source) + // FIXME: Implement unified error reporting (e.g., via `anyhow`). + .expect("failed to resolve-or-install dependencies"); + log::info!("anneal toolchain is installed at {:?}", installation_dir); +} + +fn main() { + // Suppressing timestamps removes a source of nondeterminism that is + // difficult to work around in integration tests. + env_logger::builder().format_timestamp(None).init(); + + let mut args_iter = std::env::args_os().peekable(); + let bin_name = args_iter.next().unwrap_or_else(|| "cargo-anneal".into()); + // If we're being run as a cargo plugin, the second argument will be "anneal". + if args_iter.peek().is_some_and(|arg| arg == "anneal") { + args_iter.next(); + } + let args = Cli::parse_from(std::iter::once(bin_name).chain(args_iter)); + + match args.command { + Commands::Setup(args) => setup(args), + } +} + +#[cfg(test)] +mod tests { + #[cfg(feature = "exocrate_tests")] + #[test] + fn test_setup() { + super::setup(super::SetupArgs { + // ASSUMPTION: Dependency builder installs archive at + // `target/anneal-exocrate.tar.zst`. + local_archive: Some("target/anneal-exocrate.tar.zst".into()), + }) + } +}