diff --git a/anneal/v2/chase-aeneas-versions.sh b/anneal/v2/chase-aeneas-versions.sh index 56ea54635a..c5e46f78ae 100755 --- a/anneal/v2/chase-aeneas-versions.sh +++ b/anneal/v2/chase-aeneas-versions.sh @@ -87,6 +87,7 @@ need() { need curl need sha256sum need tar +need gzip need zstd need strings need python3 @@ -145,6 +146,7 @@ if [[ ! -f "$charon_bin" ]]; then exit 1 fi +set +o pipefail commit_date=$( strings "$charon_bin" | grep -o 'rustc version .* ([0-9a-f]\{9\} [0-9]\{4\}-[0-9]\{2\}-[0-9]\{2\})' | @@ -152,20 +154,36 @@ commit_date=$( grep -o '[0-9]\{4\}-[0-9]\{2\}-[0-9]\{2\}' | tr -d '\n' ) +set -o pipefail -if [[ -z "$commit_date" ]]; then - echo "could not infer Rust commit date from charon binary" >&2 - exit 1 -fi - -rust_date=$( - python3 - "$commit_date" <<'PY' +rust_date= +if [[ -n "$commit_date" ]]; then + rust_date=$( + python3 - "$commit_date" <<'PY' import datetime import sys print((datetime.date.fromisoformat(sys.argv[1]) + datetime.timedelta(days=1)).isoformat()) PY -) + ) +fi + +if [[ -z "$rust_date" ]]; then + set +o pipefail + rust_date=$( + strings "$charon_bin" | + grep -o 'channel = "nightly-[0-9]\{4\}-[0-9]\{2\}-[0-9]\{2\}"' | + head -n 1 | + sed -E 's/channel = "nightly-([^"]+)"/\1/' | + tr -d '\n' + ) + set -o pipefail +fi + +if [[ -z "$rust_date" ]]; then + echo "could not infer Rust toolchain date from charon binary" >&2 + exit 1 +fi lean_dir="$work_dir/lean-toolchain" mkdir -p "$lean_dir" @@ -177,7 +195,7 @@ 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 +for component in cargo 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" @@ -187,7 +205,7 @@ for component in rustc rust-std rustc-dev llvm-tools miri; do 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"/ + cp -R "$comp_dir"/* "$rust_dir"/ done rust_src_archive="$work_dir/rust-src-nightly.tar.gz" @@ -197,7 +215,11 @@ 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"/ +cp -R "$top_dir/rust-src"/* "$rust_dir"/ +if [[ -d "$rust_dir/share/man" ]]; then + find "$rust_dir/share/man" -type f ! -name '*.gz' -exec gzip -n {} + +fi +chmod -R a+rX,a-w "$rust_dir" rust_output_hash=$(hash_path_sri "$rust_dir") mathlib_rev=$( diff --git a/anneal/v2/flake.nix b/anneal/v2/flake.nix index 3c0057ab66..433fcf5c64 100644 --- a/anneal/v2/flake.nix +++ b/anneal/v2/flake.nix @@ -42,10 +42,10 @@ rustDate = "2026-05-31"; leanVersion = "v4.30.0-rc2"; - rustToolchainSha256 = if system == "x86_64-linux" then "sha256-tdLBvDewiNTUKOdMJ1pkU7mPrUY0xTFOZWdG9dDNiAk=" - else if system == "aarch64-linux" then "sha256-5gGGsObb22cKc2beF5UWMEJN4Df4PM23hK0A4QJ/kEM=" - else if system == "x86_64-darwin" then "sha256-v3By/ilhfQEfNECMoNlMC0pQndo5Lq1CTTbjcsaXMPw=" - else if system == "aarch64-darwin" then "sha256-I8pM8VuoBc5R/4ZR3ZiuHmbQjn361QOXTTU+kD5B0p8=" + rustToolchainSha256 = if system == "x86_64-linux" then "sha256-MmvOgC3shIOVMWT1MTRajw8JuLwRk/P3LsmGVslNGKw=" + else if system == "aarch64-linux" then "sha256-gWFajI7TJyjslQLZm4VWBBsKA6nYe1lNQwrgUp2hwSA=" + else if system == "x86_64-darwin" then "sha256-dBLHRLo3omD7KRq0D8lzg6XiQfDKWOMD6YTrLQhEneo=" + else if system == "aarch64-darwin" then "sha256-X7ndqbjsmnjL6KZzNCxkVFJPzAsAjUqerD/wc1rxK5E=" else throw "Unsupported system: ${system}"; leanToolchainSha256 = if system == "x86_64-linux" then "sha256-o47cQjSLK5YL8YZ2raaj+mGAvvO+dIDfVeP2L+WoyMs=" @@ -151,6 +151,7 @@ " cp -r $comp_dir/* $out/" " rm -rf tmp_extract" "}" + "extract_component \"cargo\"" "extract_component \"rustc\"" "extract_component \"rust-std\"" "extract_component \"rustc-dev\"" @@ -616,6 +617,7 @@ aeneas/packages/mathlib/lake-manifest.json \ aeneas/packages/mathlib/.lake/config/mathlib/lakefile.olean \ lean/bin/lean \ + rust/bin/cargo \ rust/bin/rustc; do if ! grep -Fxq "$path" "$TMPDIR/archive/entries"; then echo "ERROR: expected archive entry missing: $path" >&2