From ab61cc24d89b097c4c21fef03a084d5e6c98ec6b Mon Sep 17 00:00:00 2001 From: Carlo Perassi Date: Wed, 23 Sep 2026 14:09:15 +0200 Subject: [PATCH] feat: accept documentation proposals from anyone 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 --- .github/workflows/validate-submission.yml | 24 +++++++--- CONTRACT.md | 8 ++++ CONTRIBUTING.md | 7 +++ tests/test_validator.py | 54 +++++++++++++++++++++++ tests/test_workflow_contract.py | 8 ++++ tools/frontier_validate.py | 26 ++++++++++- 6 files changed, 119 insertions(+), 8 deletions(-) diff --git a/.github/workflows/validate-submission.yml b/.github/workflows/validate-submission.yml index 2be36dbd..8a884b31 100644 --- a/.github/workflows/validate-submission.yml +++ b/.github/workflows/validate-submission.yml @@ -72,23 +72,32 @@ jobs: [[ "$behind" =~ ^[0-9]+$ ]] echo "behind=$behind" >> "$GITHUB_OUTPUT" + # A documentation proposal (Markdown under docs/, no Lean, no claim) is + # accepted here and stops: there is nothing to build, and no candidate + # code should run for it. The trusted receiver decides that from the + # changed paths, never from the branch name. - name: Trusted cheap preflight + id: preflight env: BEHIND_BY: ${{ steps.freshness.outputs.behind || '0' }} - run: >- - python3 trusted/tools/validate-submission - --base-dir "$GITHUB_WORKSPACE/trusted" - --candidate-dir "$GITHUB_WORKSPACE/candidate" - --preflight-only - --behind-by "$BEHIND_BY" - --json-out "$GITHUB_WORKSPACE/preflight-report.json" + run: | + python3 trusted/tools/validate-submission \ + --base-dir "$GITHUB_WORKSPACE/trusted" \ + --candidate-dir "$GITHUB_WORKSPACE/candidate" \ + --preflight-only \ + --behind-by "$BEHIND_BY" \ + --json-out "$GITHUB_WORKSPACE/preflight-report.json" + docs_only="$(python3 -c 'import json,sys; print(str(json.load(open(sys.argv[1]))["observed"].get("docs_only", False)).lower())' "$GITHUB_WORKSPACE/preflight-report.json")" + echo "docs_only=$docs_only" >> "$GITHUB_OUTPUT" - name: Build trusted validation image + if: steps.preflight.outputs.docs_only != 'true' run: docker build -f trusted/tools/Dockerfile.validator -t leanfrontier-validator:ci trusted # The candidate lakefile has already been proven identical to trusted # infrastructure. Network is available only for dependency acquisition. - name: Fetch pinned dependencies and compiled Mathlib cache + if: steps.preflight.outputs.docs_only != 'true' run: | for attempt in 1 2 3; do docker run --rm \ @@ -101,6 +110,7 @@ jobs: done - name: Restricted formal validation + if: steps.preflight.outputs.docs_only != 'true' run: | mkdir -p "$GITHUB_WORKSPACE/report-output" chmod 0777 "$GITHUB_WORKSPACE/report-output" diff --git a/CONTRACT.md b/CONTRACT.md index 8c595b35..ba5926d4 100644 --- a/CONTRACT.md +++ b/CONTRACT.md @@ -29,6 +29,14 @@ An ordinary submission also MUST NOT modify `lake-manifest.json`, `lean-toolchain`, `CONTRACT.md`, `README.md`, `MANIFEST.md`, prompts, tests, or any other trusted infrastructure. +A **documentation proposal** is the one other contribution an ordinary +contributor may open: a pull request changing only Markdown files under `docs/`, +with no Lean source and no submission record. It carries no claim, builds +nothing, and runs no candidate code. `docs/catalogue/` is generated from the +corpus and `docs/website/` is published under the project's name, so neither is +prose a submitter may edit. A documentation proposal is never merged +unattended: a person reads it, because nothing mechanical reads prose. + The receiver rejects binary files, archives, symlinks, generated payloads, hidden files outside the permitted source tree, and executable content that is not ordinary Lean source. Consumers build LeanFrontier from source and import diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 3adaa007..9ec34f55 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -44,6 +44,13 @@ don't hold accepted work back in a queue. Only conjectures have a quota Substantive extensions that build on accepted results are especially welcome. +## Proposing documentation + +A pull request that changes only Markdown under `docs/` needs no claim and no +Lean source. The receiver accepts it as a documentation proposal and skips the +build entirely; a maintainer then reads it and merges it. `docs/catalogue/` is +generated and `docs/website/` is published, so neither can be changed this way. + ## Questions and project maintenance Use GitHub issues for questions, protocol proposals, and non-sensitive bug diff --git a/tests/test_validator.py b/tests/test_validator.py index 6bbcd3b4..ed74219b 100644 --- a/tests/test_validator.py +++ b/tests/test_validator.py @@ -188,6 +188,60 @@ def test_a_local_run_detects_a_stale_branch_from_git(self) -> None: git("merge", "-q", "main") self.assertEqual(frontier_validate.commits_behind("main", repo), 0) + def docs_tree(self) -> None: + for root in (self.base, self.candidate): + (root / "docs").mkdir(exist_ok=True) + (root / "docs" / "CONTRIBUTION-DIRECTIONS.md").write_text("# directions\n") + (self.candidate / "LeanFrontier" / "Algebra" / "New.lean").unlink() + (self.candidate / "Submissions" / "valid-bundle.json").unlink() + + def test_a_documentation_only_change_is_accepted_without_a_claim(self) -> None: + """Twice a docs PR from the one external contributor was refused for not being a submission. + + `maintenance/` only routes around the submission rules for the owner, so + a fork cannot propose documentation at all. + """ + self.docs_tree() + (self.candidate / "docs" / "CONTRIBUTION-DIRECTIONS.md").write_text("# directions\n\nnew target\n") + status, report = self.validate() + self.assertEqual(status, 0, report["diagnostics"]) + self.assertTrue(report["accepted"]) + self.assertTrue(report["observed"]["docs_only"]) + + def test_a_new_documentation_file_is_accepted(self) -> None: + self.docs_tree() + (self.candidate / "docs" / "threat-model.md").write_text("# threat model\n") + status, report = self.validate() + self.assertEqual(status, 0, report["diagnostics"]) + + def test_documentation_mixed_with_lean_source_is_rejected(self) -> None: + self.docs_tree() + (self.candidate / "docs" / "CONTRIBUTION-DIRECTIONS.md").write_text("# directions\n\nnew\n") + (self.candidate / "LeanFrontier" / "Algebra" / "Sneak.lean").write_text("theorem sneak : True := trivial\n") + status, report = self.validate() + self.assertEqual(status, 1) + self.assertFalse(report["observed"].get("docs_only")) + + def test_the_published_site_and_catalogue_are_not_documentation(self) -> None: + """docs/website is deployed to Pages and docs/catalogue is generated.""" + for relative in ("docs/website/index.html", "docs/catalogue/index.html"): + with self.subTest(path=relative): + self.setUp() + self.docs_tree() + target = self.candidate / relative + target.parent.mkdir(parents=True, exist_ok=True) + target.write_text("

hello

\n") + status, report = self.validate() + self.assertEqual(status, 1) + codes = {item["code"] for item in report["diagnostics"]} + self.assertIn("PATH_POLICY_VIOLATION", codes) + + def test_documentation_may_not_delete(self) -> None: + self.docs_tree() + (self.candidate / "docs" / "CONTRIBUTION-DIRECTIONS.md").unlink() + status, report = self.validate() + self.assertEqual(status, 1) + def test_unauthorized_path_is_rejected(self) -> None: (self.candidate / "README.md").write_text("payload") self.assert_rejected("PATH_POLICY_VIOLATION") diff --git a/tests/test_workflow_contract.py b/tests/test_workflow_contract.py index 86fe70fc..024d0fb6 100644 --- a/tests/test_workflow_contract.py +++ b/tests/test_workflow_contract.py @@ -50,6 +50,14 @@ def test_a_stale_pull_request_is_named_as_stale(self) -> None: # Untrusted values reach the shell only through the environment. self.assertNotIn("compare/${{", WORKFLOW) + def test_a_documentation_change_skips_the_lean_stages(self) -> None: + self.assertIn('--json-out "$GITHUB_WORKSPACE/preflight-report.json"', WORKFLOW) + self.assertIn("docs_only", WORKFLOW) + # Every stage that builds or runs candidate code is gated on it. + for stage in ("Build trusted validation image", "Fetch pinned dependencies", "Restricted formal validation"): + index = WORKFLOW.index(stage) + self.assertIn("steps.preflight.outputs.docs_only != 'true'", WORKFLOW[index:index + 900], stage) + def test_receiver_has_restricted_formal_execution_and_report(self) -> None: for required in ( "--network none", diff --git a/tools/frontier_validate.py b/tools/frontier_validate.py index b253015f..3ccd905f 100644 --- a/tools/frontier_validate.py +++ b/tools/frontier_validate.py @@ -190,6 +190,21 @@ def is_allowed_path(path: str) -> bool: return path.startswith("LeanFrontier/") or SUBMISSION_RE.fullmatch(path) is not None +def is_documentation_path(path: str) -> bool: + """Prose a contribution may propose on its own, with no Lean and no claim. + + Markdown under `docs/` only. `docs/catalogue/` is generated from the corpus + and `docs/website/` is deployed to GitHub Pages, so neither is prose a + submitter may edit: a change there would publish under the project's name. + """ + return ( + path.startswith("docs/") + and path.endswith(".md") + and not path.startswith("docs/catalogue/") + and not path.startswith("docs/website/") + ) + + def line_count(path: Path) -> int: try: return path.read_text(encoding="utf-8").count("\n") + 1 @@ -369,6 +384,15 @@ def static_preflight(base: Path | None, candidate: Path, limits: dict[str, Any], changed, before = changed_paths(base, candidate) corpus = corpus_skeletons(base) report.observations["changed_files"] = sorted(changed) + # A documentation proposal: prose, no Lean, no claim, nothing to build. It + # is admitted by the same trusted receiver as everything else, and merged by + # a human like every other change that is not an ordinary submission. + if changed and all(path is not None and is_documentation_path(relative) for relative, path in changed.items()): + oversized = [relative for relative, path in changed.items() if path is not None and path.stat().st_size > limits["max_individual_file_bytes"]] + for relative in oversized: + report.reject("RESOURCE_LIMIT_EXCEEDED", "individual file exceeds policy limit", relative) + report.observations["docs_only"] = not oversized + return {}, None if len(changed) > limits["max_changed_files"]: report.reject("RESOURCE_LIMIT_EXCEEDED", "too many changed files") changed_bytes = 0 @@ -1129,7 +1153,7 @@ def main(argv: list[str] | None = None) -> int: base, candidate, submitted_modules(changed), [e for e in metadata.get("entrypoints", []) if isinstance(e, str)], metadata, load_json(DEFAULT_CONJECTURE), report) - if report.accepted and not args.preflight_only: + if report.accepted and not args.preflight_only and not report.observations.get("docs_only"): if metadata is None: report.reject("SCHEMA_INVALID", "no valid metadata record was available for audit") else: