docs: add contribution directions and PR cadence (from #196) - #200
Merged
Merged
Conversation
Adapted from the cadence section qazW12345 wrote for their fork's copy of prompts/SUBMITTER.md, which recorded the maintainer's answer on #180. Co-authored-by: qazW12345 <44544794+qazW12345@users.noreply.github.com> Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This was referenced Sep 22, 2026
This was referenced Sep 23, 2026
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.
Brings in @qazW12345's contribution-directions dossier from #196, discussed in #186.
Why a separate PR:
validatetreats amaintenance/PR from a non-owner as an ordinary submission, which may only changeLeanFrontier/and one claim, so #196 cannot pass by design. This branch carries their commit unchanged (e96afc1, authored by qazW12345) plus one commit of ours.Commits
docs/CONTRIBUTION-DIRECTIONS.md(440 lines), exactly as in docs: add contribution directions roadmap #196. It's a non-normative roadmap: the ranked bridge targets A–K, the rejected formulations, and the conjecture-boundary warnings. It defers toCONTRACT.mdthroughout.CONTRIBUTING.md:prompts/SUBMITTER.md, which records the maintainer's answer on feat(Geometry): bridge Ford circles to Euclidean sphere tangency #180.The contract, the prompts and the policy are unchanged.
Known staleness: section A (largest Ford circle between Farey neighbours) and section D (Horadam companion matrix) are being submitted as #197 and #195. Once those merge, the dossier still lists them as open targets. That's worth a follow-up edit, and it doesn't need to block this PR.
Supersedes #196.
🤖 Generated with Claude Code