docs: refresh contribution directions (adopts #287) - #290
Merged
Merged
Conversation
qazW12345
pushed a commit
to qazW12345/LeanFrontier
that referenced
this pull request
Sep 23, 2026
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 (carlok#200, carlok#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
2 participants
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.
Carries @qazW12345's commit
c228d93unchanged, with their authorship, so it can passvalidate. Same reason as #200 before it: amaintenance/branch from a non-owner is routed to the ordinary submission rules, which reject anything outsideLeanFrontier/plus one claim. They had already worked out the branch convention themselves and closed their own #286 in favour of #287; the remaining wall is ours, not theirs.What the refresh does: rewrites
docs/CONTRIBUTION-DIRECTIONS.mdagainst the corpus as it now stands, dropping targets that have landed rather than keeping them as history, on the argument that the catalogue, claims and observations already record what exists. Six open directions remain:[0,1]D is the interesting one: that's our open conjecture, picked up hours after I pointed at it on #281.
Checked: single file,
docs/only, no fork-specific content, nothing that reads as instructions to an agent. Tests pass (145, 6 skipped).Follow-up worth doing: this is the second time a documentation PR from the only external contributor has been blocked by the OWNER check. A
validate-docspath that acceptsdocs/-only changes from anyone, while keeping the merge manual, would remove the friction without weakening anything — a human still merges, and no Lean source is involved.🤖 Generated with Claude Code