feat: accept documentation proposals from anyone - #291
Merged
Merged
Conversation
A pull request changing only Markdown under docs/ is now admitted with no claim, no Lean source and no build. Twice the one external contributor tried to improve docs/CONTRIBUTION-DIRECTIONS.md and was refused: an ordinary submission may only touch LeanFrontier/ plus one claim, and the maintenance path requires OWNER, so a fork could not propose prose at all. Both times a maintainer had to cherry-pick the commit (#200, #290). The receiver decides from the changed paths, never from the branch name. docs/catalogue/ is generated from the corpus and docs/website/ is published under the project's name, so neither counts as prose a submitter may edit. Size limits still apply, deletions are still refused, and a mixed change (docs plus anything else) is an ordinary submission and fails as one. In the workflow the preflight now reports docs_only, and the image build, dependency fetch and restricted formal validation are gated on it: no candidate code runs for a prose change. Nothing merges unattended, because no mechanical check reads prose. Verified end to end: the real receiver on a docs-only diff against main returns accepted with docs_only true and no diagnostics. Co-Authored-By: Claude Opus 5 <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
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.
Closes the friction #290 documented. Twice now, @qazW12345 has tried to improve
docs/CONTRIBUTION-DIRECTIONS.mdand been refused by the receiver: an ordinary submission may change onlyLeanFrontier/plus one claim, and themaintenance/path is gated on OWNER, so a fork cannot propose prose at all. Both times a maintainer cherry-picked the commit instead (#200, #290).The rule
A pull request whose every changed path is a Markdown file under
docs/is a documentation proposal: no claim, no Lean, no build.docs/catalogue/anddocs/website/are excluded. The first is generated from the corpus; the second is deployed to Pages, so a change there would publish under the project's name.Workflow
The preflight now reports
docs_only, and the three stages that build or run candidate code are gated on it:So a prose change costs one short job instead of a Docker build and a Mathlib fetch.
Evidence
main→accepted: True,docs_only: True,changed_files: ['docs/CONTRIBUTION-DIRECTIONS.md'], no diagnostics, no Lean run.docs/website/anddocs/catalogue/both rejected as path violations; a docs deletion rejected; and a workflow contract test pinning that each Lean stage carries thedocs_onlygate.Full suite: 151 tests, 6 skipped.
CONTRACT.md§2 andCONTRIBUTING.mddescribe the new contribution type.🤖 Generated with Claude Code