[anneal] Move setup and CI onto Nix archive

Share the exocrate installer between Anneal and v2, and have non-v2 Anneal install the same Nix-built omnibus archive that v2 already produces. The generated Lean workspace can then use the archive layout directly instead of cloning and rewriting Lake dependencies at runtime.

Update Anneal CI to build the archive with Nix, install it before root tests and example checks, and run the Lean-heavy integration suite serially. The workflow no longer depends on a Docker image that pre-bakes the old setup output.

gherrit-pr-id: Gefzjo7bqy3imk4ti4im5wep4jz3upvrm

Author: mdittmer

.github/workflows/anneal.yml

@@ -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.
 #

anneal/Cargo.lock

@@ -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

anneal/Cargo.toml

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

anneal/Dockerfile

@@ -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" "$@"