[anneal] Move setup and CI onto Nix archive

anneal/Cargo.toml

@@ -1,5 +1,5 @@
 [workspace]
-members = [".", "tools/doc_gen"]
+members = [".", "exocrate", "tools/doc_gen"]
 
 [package]
 name = "cargo-anneal"
@@ -21,6 +21,22 @@ publish = true
 
 exclude = [".*", "testdata"]
 
+[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 +62,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 +103,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

@@ -57,17 +57,16 @@ WORKDIR /workspace
 COPY --from=extractor --chown=anneal:anneal /app/Cargo.toml.no_workspace ./Cargo.toml
 COPY --chown=anneal:anneal Cargo.lock ./
 
-# Copy source files needed for setup.
-COPY --chown=anneal:anneal src/setup.rs src/util.rs ./src/
+# Copy source files needed to compile dependency-heavy modules.
+COPY --chown=anneal:anneal src/setup.rs ./src/
+COPY --chown=anneal:anneal exocrate/Cargo.toml ./exocrate/Cargo.toml
+COPY --chown=anneal:anneal exocrate/src ./exocrate/src
 COPY --chown=anneal:anneal build.rs ./
-COPY --chown=anneal:anneal tools/prune_mathlib.py ./tools/
 
-# 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())
 }

exocrate/Cargo.toml → anneal/exocrate/Cargo.toml

@@ -5,13 +5,12 @@ edition = "2024"
 
 [dependencies]
 dirs = "6.0.0"
-fs4 = "1.1.0"
+fs2 = "0.4.3"
 log = "0.4.29"
-sha2 = "0.11.0"
+sha2 = "0.10.9"
 sha2-const = "0.1.3"
 tar = "0.4.45"
 tempfile = "3.27.0"
-toml_const = "1.3.0"
 ureq = "3.3.0"
 zstd = "0.13.3"