[hermes] In dev, install prebuilts in target

This allows developers to isolate their development from their use of
`cargo hermes verify` globally. It also makes development slightly
easier to integrate with Docker, as `cargo run setup`, when run in the
container, doesn't try to write to paths that aren't writeable (this is
specifically a problem since we re-define the UID of the user in the
container in order to match the external UID, making them not root in
the container, but thus making them not have write permissions to root's
home directory).

gherrit-pr-id: Gzjx2m23qp7ycaxvr2hvvsspjslbysoix

Author: joshlf

hermes/Dockerfile

@@ -1,17 +1,21 @@
 FROM ubuntu:24.04 AS base
 
-# Relocate toolchains so non-root developers can access and write to them when mapping UIDs
+# Relocate toolchains so non-root developers can access and write to them when
+# mapping UIDs.
 ENV RUSTUP_HOME=/opt/rustup \
     CARGO_HOME=/opt/cargo \
     ELAN_HOME=/opt/elan \
     PATH="/opt/cargo/bin:/opt/elan/bin:${PATH}"
 
-# Install build dependencies, Rust, and Lean
 RUN apt-get update && DEBIAN_FRONTEND=noninteractive apt-get install -y git curl build-essential pkg-config libssl-dev && \
     curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --no-modify-path && \
     rm -rf /var/lib/apt/lists/*
 
-# Install elan (Lean toolchain manager)
+# Charon strictly requires a specific nightly compiler version to execute.
+# FIXME: Extract this version string dynamically from `src/setup.rs` in the future.
+RUN rustup toolchain install --no-self-update nightly-2026-02-07 --profile minimal
+
+# Install elan (Lean toolchain manager).
 RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --no-modify-path
 
 # Prepare a globally writable cache directory to hold both the integration test
@@ -21,44 +25,17 @@ RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -
 RUN mkdir -p /cache && chmod 777 /cache && \
     chmod -R a+rwX /opt/rustup /opt/cargo /opt/elan
 
-# Direct Hermes tests to write ephemeral integration targets here to leverage overlayfs
+# Direct Hermes tests to write ephemeral integration targets here to leverage
+# overlayfs.
 ENV HERMES_INTEGRATION_TARGET_DIR=/cache/hermes_target
 WORKDIR /workspace
 
-# Copy vendored requirements
-COPY .cargo .cargo
-COPY vendor vendor
-
-ENV __ZEROCOPY_LOCAL_DEV="1"
+FROM base AS dev
 
-# Copy only the hermes crate logic
-COPY Cargo.toml Cargo.toml
-COPY build.rs build.rs
-COPY src src
-# Since Cargo.toml explicitly declares [[test]] "integration", this file must exist for Cargo to parse it.
-COPY tests/integration.rs tests/integration.rs
-# Copy tools because they are part of the workspace members
+COPY testdata testdata
 COPY tools tools
 
-# Download and verify the required versions of Charon and Aeneas.
-RUN cargo run --bin cargo-hermes setup && \
-    rm -rf /workspace/target /opt/cargo/registry /opt/cargo/git
-
-# Charon strictly requires a specific nightly compiler version to execute.
-# FIXME: Extract this version string dynamically from `src/setup.rs` in the future.
-RUN rustup toolchain install nightly-2026-02-07 --profile minimal && \
-    chmod -R a+rwX /opt/rustup /opt/cargo /opt/elan
-
-# To pre-build Mathlib for local development, we run a fast dummy test. We don't
-# use this in CI because copying the multiple GB produced in this image is
-# slower in CI than just re-building from scratch.
-FROM base AS dev
-COPY tests/fixtures/syntax_error tests/fixtures/syntax_error
-RUN cargo test --test integration -- syntax_error && \
-    chmod -R a+rwX /cache
+# Download Lean/Elan and pre-build the Mathlib cache and Aeneas standard library.
+RUN ./tools/prebuild_lean_libs.sh
 
-# Any `/workspace/target` generated here will be shadowed by the host's bind
-# mount, so removing it is purely to reduce image size slightly before
-# shadowing. Because of this shadowing, there would be no benefit to keeping
-# it.
-RUN rm -rf /workspace/target
+RUN chmod -R a+rwX /cache /opt/rustup /opt/cargo /opt/elan

hermes/src/setup.rs

@@ -138,8 +138,15 @@ pub struct Toolchain {
 impl Toolchain {
     /// Resolves the toolchain manager and acquires a shared lock.
     pub fn resolve() -> Result<Self> {
-        let home =
-            dirs::home_dir().ok_or_else(|| anyhow::anyhow!("Could not find home directory"))?;
+        let home = if std::env::var("__ZEROCOPY_LOCAL_DEV").is_ok() {
+            std::path::PathBuf::from(
+                std::env::var("CARGO_MANIFEST_DIR").unwrap_or_else(|_| ".".to_string()),
+            )
+            .join("target")
+            .join("hermes-home")
+        } else {
+            dirs::home_dir().ok_or_else(|| anyhow::anyhow!("Could not find home directory"))?
+        };
         let platform = Platform::detect()?;
         let aeneas_hash = platform.expected_archive_hash();
 

hermes/tests/fixtures/allow_sorry_fallbacks/expected.stderr

@@ -69,4 +69,4 @@
  59 │ /// ```
     ╰────
 
-Error: Lean verification failed. Consider running `cargo run generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.
+Error: Lean verification failed. Consider running `cargo hermes generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.

hermes/tests/fixtures/charon_version_mismatch/expected.stderr

@@ -1,4 +1,4 @@
 Error: Charon version mismatch.
 Expected: 0.1.174
 Found:    0.0.0
-Please run `cargo run setup` to install the correct version.
+Please run `cargo hermes setup` to install the correct version.

hermes/tests/fixtures/const_generics/expected.stderr

@@ -8,4 +8,4 @@
  9 │ /// ```
    ╰────
 
-Error: Lean verification failed. Consider running `cargo run generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.
+Error: Lean verification failed. Consider running `cargo hermes generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.

hermes/tests/fixtures/diagnostic_mapping/expected.stderr

@@ -36,4 +36,4 @@
  42 │ /// ```
     ╰────
 
-Error: Lean verification failed. Consider running `cargo run generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.
+Error: Lean verification failed. Consider running `cargo hermes generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.

hermes/tests/fixtures/edge_cases_logic/test_5_4_std_types/expected.stderr

@@ -21,4 +21,4 @@ Note: Expected a function because this term is being applied to the argument
   Std.U32
 
 Hint: The identifier `Vec` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.
-Error: Lean verification failed. Consider running `cargo run generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.
+Error: Lean verification failed. Consider running `cargo hermes generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.

hermes/tests/fixtures/edge_cases_mut_refs/test_3_3_ret_mut/expected.stderr

@@ -28,4 +28,4 @@ Note: Expected a function because this term is being applied to the argument
   Std.U32
 
 Hint: The identifier `Vec` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.
-Error: Lean verification failed. Consider running `cargo run generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.
+Error: Lean verification failed. Consider running `cargo hermes generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.

hermes/tests/fixtures/enums_pattern_matching/expected.stderr

@@ -12,4 +12,4 @@
  10 │ ///   | Enum.B b => b
     ╰────
 
-Error: Lean verification failed. Consider running `cargo run generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.
+Error: Lean verification failed. Consider running `cargo hermes generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.

hermes/tests/fixtures/is_valid_verification/expected.stderr

@@ -92,4 +92,4 @@
  29 │ /// ```
     ╰────
 
-Error: Lean verification failed. Consider running `cargo run generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.
+Error: Lean verification failed. Consider running `cargo hermes generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.