ci: enable parallel CI-first draft PR validation - #603
Draft
PerAlexandersson wants to merge 2 commits into
Draft
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
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.
Implements #598 and the user-approved CI-first workflow. Preserves the build check and all source guards, makes the ordinary default Lake build explicit, scopes validation concurrency by PR/ref, separates docs generation from proof validation, and confines Pages permissions to a serialized trusted-main publishing job with an exact-SHA freshness gate. Updates README/AGENTS to permit source-checked draft branch checkpoints before remote compilation, while requiring green exact-revision builds and applicable axiom checks before integration.
Verified locally: YAML structure/security assertions, import-parser tests, root imports, architecture self-test/check, proof-status self-test/check, generated tactic coverage and git diff --check. No local Lean/Lake/compiler run. This is intentionally a draft awaiting remote CI. Comparator remains unchanged. No repository settings or branch-protection changes, automatic merge, or default-branch push.
Docs dry-run uses a pinned upstream action revision whose deploy=false input was inspected; trusted-main docs/deployment needs observation after integration and is not claimed verified by this PR run. Closes #598 only after acceptance.