[anneal] Move setup and CI onto Nix archive

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

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

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

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