[kim-em]

Support submissions on Lean v4.35.0 and v4.36.0-rc2, each with a benchmark-owned, fully pinned dependency configuration. The root checkout defaults to rc2. The same problem sources must compile under both configurations; no comparison of their elaborated meanings is required. Portable formulations repair the projectivization, tensor-action and abelianization API differences.

Add isolated configuration preparation and source-archive toolchain selection. The closest lean-toolchain above each attempted workspace selects an approved configuration; missing pins use the default, and mixed or unsupported requests are rejected after archival. Configuration preparation keeps build outputs separate, and the runner regenerates selected pristine workspaces before overlaying solver code. Intake and evaluation retain the exact benchmark commit and selected toolchain.

Allow solution imports from CFSG and Stacks while continuing to reject them in trusted statements. Parse import headers without elaborating solver code, register the required cache services, and restore explicit module targets with compilation disabled. Both public services are configured and verified: CFSG at https://cfsg-downloads.axiommath.workers.dev/lake, Stacks at https://stacks-cache.axiommath.workers.dev/lake. Empty endpoint overrides retain these defaults.

CI requires catalog compilation on stable and RC, exercises cache restoration and sandbox/scoring on both, and preserves the existing required verify, security and restore check names. Committed default workspaces remain owned by the main-branch regenerator.

Runner prerequisite completed: leanprover/lean-eval-submissions#2182 is merged at 8b0005d3 and promoted through staging and production. It selects the archived configuration, regenerates workspaces, fetches solution-only caches, and records toolchain provenance in immutable verification receipts and archive sidecars.

External cache compatibility: stable pins Mathlib 074063781836922cb02701cd12943c9f51731afa and TauCeti 1f9b4414105d86e487a4ac4c3d3397076a44d0d2; rc2 pins Mathlib 2ddf59c8f14245864e6c0ed227a2dab76b9efea2 and TauCeti be86813dc92e6bac8614c2c2dd34572145df09c0. CFSG's current publication targets 4.35.0-rc3. Stacks targets 4.35.0 but Mathlib 56a00585, so both libraries still need cache publications matching an approved full dependency set. Unused solution libraries do not block ordinary submissions.

Validation:

• All 296 catalog modules build under stable without unexpected warnings; rc2's complete catalog build and the three updated compatibility modules also pass.
• Eight generated workspaces affected by these API changes build across the two configurations without unexpected warnings.
• 77 Python tests and all 173 stable Lean unit tests pass. The opt-in real Lake test also passes on stable; rc2's real Lake tests passed separately.
• All five stable sandbox/verifier probes and the complete scoring workflow pass, including invalid-proof rejection, both kernels, and a solution-only Lean Pool import. RC probes passed separately.
• All 312 default workspaces regenerate, inventory validation passes, and workflow lint/action-pin checks are clean.
• A deeply nested source TOML request is archived successfully and then rejected without invoking a compiler.

Latest-head GitHub CI and cache restoration passed, including all stable/RC catalog shards, scoring jobs, inventory aggregation and the required verify check. The classifier now parses headers without materializing package dependencies; its coverage checks pass on both toolchains. Benchmark CI materializes only pinned package metadata for the solution-only CFSG/Stacks dependencies, keeping ordinary validation within its deadlines; submission evaluation retains full source checkouts. Tests cover the metadata policy, exact revision and actual sparse Git materialization, and an isolated stable project passes manifest validation and workspace generation with these metadata-only packages.

[kim-em]

Prerequisite for production use: leanprover/lean-eval-submissions#2182 restores library caches after solver files are overlaid and uses selective restoration when preparing the benchmark root.