[kim-em]

Allow submissions to select an approved stable or RC benchmark configuration through their source lean-toolchain files. Freeze that selection after fetching the exact archived source; evaluation repeats it against the same benchmark commit, applies the pinned configuration before installing Lean, and regenerates selected pristine workspaces before overlaying solver files. Older snapshots retain their single-toolchain behavior.

Restore libraries used only by solver imports using the trusted benchmark's selective cache helper. Preparation parses headers and restores registered library targets with compilation disabled; comparator alone elaborates solver code. Use selective restoration for root preparation too, retaining historical and preprimed replay behavior.

Archive parser failures cannot prevent source retention. Unsupported or mixed requests produce completed, terminal rejections rather than retryable infrastructure failures or larger-runner retries. Normal evaluation artifacts and State completion carry that rejection, and issue reports identify the configuration problem.

Record the selected toolchain in immutable public verification/<result_id>.json receipts and finalized archive sidecars. Preserve it through envelope migration. Existing result rows, IDs and receipts remain unchanged. Historical single-pin replay builders explicitly refuse multi-configuration benchmark snapshots rather than infer the RC root pin for a stable result; those snapshots require profile-aware replay using the recorded configuration.

Companion benchmark: leanprover/lean-eval#670. Merge and promote this runner change first, then merge the benchmark change. CFSG and Stacks cache publications must match the chosen full dependency set before those imports can be evaluated.

Validation: the full offline suite passes (1,182 tests; four opt-in skips), including configuration ordering, terminal rejection, archive retention, immutable provenance, migration and replay guards. Benchmark integration verifies stable selection, regeneration, solver overlay, actual cache restoration and scoring with both kernels. Workflow linting, syntax checks and action-pin audits pass. Latest-head GitHub CI is pending.