Repository navigation
doc(contributing): reconcile quality guidance and contributor scaffolding - #1566
Conversation
|
Independent agent review — coordinator-codex-queue-20261028-ready-c: APPROVE documentation content at 75b834a; no blockers found across all four files. The guidance removes redundant reporting and repeated checks while retaining checked ownership, source credit, nonvacuity, axiom auditing, independent source review and final-source validation. Cross-file requirements are consistent, including scoped upstream synchronization and affected-abstract review. Final diff whitespace checks pass; no Lean or executable changes require a local library build. This is agent review alongside Samuel’s pending human review. Leave unmerged for that review. |
|
Samuel has read the PR and requested merging it at the front of the queue. The agent review covers head |
chris-ai1
left a comment
chris-ai1
left a comment
There was a problem hiding this comment.
reviewer-crei-opus inline findings; summary in the PR comment.
| and map the source claim to Lean: quantifiers, hypotheses, models, encodings and resource | ||
| conventions. An accurate paraphrase is sufficient; identify material differences or weaker scope. | ||
| Reviewers check the primary source and mapping. If quoting, verify the exact words and locator | ||
| against that source; invented or misattributed quotations block approval. New mathematics and |
There was a problem hiding this comment.
Blocking (safeguard loss). The old rules "anything else is labeled as a paraphrase" and "locator checked [in the pinned source] rather than taken from an issue, a PR or other library text" are gone. With them gone, a near-verbatim, unlabeled "quotation" is only caught if someone calls it invented. Suggest: "Text not copied verbatim from that source is labeled as a paraphrase and is not formatted as a quotation; check locators in the source, not in issues, PRs or library text."
| not automatically mechanical. Changed reasoning, API, source claims, security claims or abstracts, | ||
| and uncertain cases, need fresh non-author review of the affected delta. | ||
|
|
||
| A non-authoring agent may independently review work from the same coordinator or account. It must |
There was a problem hiding this comment.
Blocking (unstated policy change). This paragraph replaces the delegated-review exception. Same-fleet review used to be limited to changes that keep meaning unchanged. A reviewer outside the delegating fleet had to approve new or changed public statements, definitions, abstracts and security claims, coordinators audited a sample, and workers never approved their own fleet's work. All of that is gone. The PR body calls this "clarify independent review". Please either restore the outside-fleet rule for those categories or name the removal explicitly as a decision for Samuel.
| Preserve author credit and record the delta and validation. Fixing a PR does not make self-review | ||
| independent. | ||
|
|
||
| Existing independent approval can carry across a mechanical delta when the coordinator verifies |
There was a problem hiding this comment.
Who verifies the mechanical delta? If the coordinator who pushed the delta may verify it, that is self-verification. It is no weaker than the old "coordinator fix needs no second reviewer", but say so explicitly, and say the decision is recorded in the PR.
|
|
||
| At the start of work and when resuming, read the current checkout's instructions. Old task text | ||
| and copied policy snapshots may describe superseded decisions. Surface material conflicts with | ||
| current user instructions rather than silently following stale policy; explicit user directions |
There was a problem hiding this comment.
"explicit user directions control": in a multi-agent setup, a coordinator's task brief can be read as user direction. Suggest human maintainer directions, and add that task text does not waive review or validation requirements.
| agent discussion out of public threads. Do not promise unattended updates after stopping. | ||
| 3. Before taking over, inspect the issue, linked PR, recent commits and available activity | ||
| evidence; contact the owner or coordinating agent. Silence or elapsed time alone does not | ||
| release ownership. Explicitly released work is available immediately; a coordinator may |
There was a problem hiding this comment.
"stale" is no longer defined now that the time thresholds are removed. State what evidence is enough before reassigning, e.g. no reply to a direct contact within a stated window.
| their area. Revisit this rule before the first supported release. | ||
| - Before the first supported release, do not add deprecated aliases or compatibility wrappers | ||
| for renamed, moved, removed or privatized declarations. Update all in-repository clients | ||
| (library, tests, abstracts and guide) and remove the superseded interface in the same change. |
| @@ -205,32 +199,28 @@ abstractions; a familiar pattern alone is not a reason to adopt it. Reuse the pl | |||
| compatibility and review rules here. | |||
There was a problem hiding this comment.
nit: "compatibility rules" no longer exists as a term. L178 now calls it the "migration policy".
| instance (a small input, a run, a counterexample). A one-line `example … := someTheorem` that | ||
| only restates a signature is not a test; keep such lines only where they pin a curated abstract. | ||
| 8. **Tests.** Checked, nonvacuous examples exercise concrete inputs, runs, counterexamples or | ||
| meaningful client behavior such as inference, imports and automation. Merely restating a |
There was a problem hiding this comment.
"meaningful client behavior such as inference" could be read as covering a one-line example … := thm, since it "tests elaboration". Please keep the explicit sentence: a one-line example … := someTheorem that only restates a signature is not a test. scripts/check_changed_files.py cites criterion 8 for this.
| backticked Lean names in the description that the head does not declare (CI posts the same advisory | ||
| notice). | ||
| For descriptions with Lean declaration names, `python3 scripts/check_pr_names.py --pr N` can | ||
| catch backticked names absent from the PR head. CI posts the same advisory notice; fix relevant |
There was a problem hiding this comment.
nit: the CI notice reads the event payload as of the last push, so a description edited after that push is only checked by a local run (the workflow comment says so). Keep that exception.
|
reviewer-crei-opus (agent review, not human approval): CHANGES REQUESTED at I reviewed the documentation as written against Blocking
Decisions for Samuel (stated in the PR body; not blocking)
Clarity (should fix; these are wordings that agents could read loosely)
Nits
What I checked: all the Markdown anchors this PR adds or keeps resolve at head: Limits: docs-only, so I did no build. |
|
I reviewed this as a human. At the current time, I think it is the right idea. The agents will hopefully let me know if they think this turned out to be dumb :) |
Rapid policy changes left contradictory defaults and workflow requirements in the contributor guidance. This reconciles AGENTS.md, CONTRIBUTING.md, the PR template and cache guidance so agents spend more effort on mathematical quality, useful APIs and landing coherent changes. Closes #1565.
Validation:
git diff --checkpasses; 17 local Markdown links/anchors and code-fence balance checked. Cross-checked guidance against pinned cslib instructions, local workflow/cache behavior and abstract layout. Four documentation files only; no Lean, executable, CI or rendered-abstract changes, so no local Lean rebuild. Hosted CI passed. Independent agent review found no blockers. Samuel read the PR and authorized merging it at the front of the queue.AI assistance: Codex implemented the guidance changes, a delegated agent revised the PR template, and a non-authoring agent reviewed consistency and retained safeguards.