Repository navigation
ci: check the evaluation pipeline accepts the pinned toolchain - #661
Merged
Merged
Conversation
The benchmark owns lean-toolchain, but lean-eval-submissions, the Worker and State each validate the toolchain string against their own contracts. Bumping to v4.35.0-rc3 on 2026-09-28 broke every server-dispatched evaluation from 2026-09-30 until the contracts were widened on 2026-10-07, while this repository's CI stayed green. The new check fetches the live contracts from the protected main branches and the shared acceptance vectors in State, and fails the classify job when the pin is rejected by any of them. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
lean-eval-state is private, so its schemas cannot be fetched from a public CI job; its own CI binds them to the same vectors, which now live in lean-eval-submissions. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…ctors Only trailing newlines are dropped from lean-toolchain, matching the pipeline's shell substitution. The two schemas are read at their known toolchain locations and must be anchored patterns Python's re reads the same way; anything else fails closed. Each pattern is also checked against every shared accepted and rejected vector, so a drifted schema is reported even when the pin itself passes. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Python's $ also matches before a trailing newline, so the shared rejected vector with a trailing newline was reported as accepted by every schema. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds
scripts/check_pipeline_toolchain_contract.pyand runs it in the classify job. The benchmark ownslean-toolchain, but lean-eval-submissions, the Worker and State each validate the toolchain string against their own contracts; the bump to v4.35.0-rc3 on 2026-09-28 broke every server-dispatched evaluation from 2026-09-30 until the contracts were widened on 2026-10-07, while this repository's CI stayed green. The check fetches the evaluation-completion and replay-queue schemas and the shared toolchain acceptance vectors from lean-eval-submissions main (leanprover/lean-eval-submissions#2000; State is private and binds its own contracts to the same vectors in its CI) and fails when the pin is rejected by any of them. Offline tests drive it over afile://tree. CI on this PR passes only once #2000 has merged.🤖 Prepared with Claude Code