Repository navigation
Add manual compute coverage and exact-profile backfill planning - #2169
Merged
Merged
Conversation
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
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.
Historical compute coverage should be accounted for without adding scheduled recovery or replay work to ordinary submissions. Add two manual operator tools: a public Results/State coverage report, and a create-only planner for missing server replay tasks using already-qualified exact original benchmark/toolchain profiles.
The tools reuse existing replay tasks and historical inventory/controllers, report blocked profiles instead of substituting newer toolchains, and produce deterministic candidate event packets. They do not append State, fetch/decrypt source, dispatch proofs, hold callback credentials, or change replay gates. No workflow or production behavior changes are added.
This follow-up is separate from the acceptance reporting rollout in #2163. It accepts existing public State v6; v7 acceptance receipts are included when available from leanprover/lean-eval-state#51. It is not a prerequisite for deploying the reporting UI or editor. See
docs/compute-history.md.Validation: two behavioral tests cover coverage classification, missing qualification, exact toolchain selection, deterministic packets and existing-task reuse; stdlib-only scripts pass Ruff and syntax checks. No historical proofs or State mutations were run.