Skip to content

chore: add review rubric + PR template (governance) - #118

Merged
Xinze-Li-Moqian merged 1 commit into
mainfrom
chore/review-rubric
Jul 21, 2026
Merged

chore: add review rubric + PR template (governance)#118
Xinze-Li-Moqian merged 1 commit into
mainfrom
chore/review-rubric

Conversation

@Xinze-Li-Moqian

Copy link
Copy Markdown
Contributor

Adds two governance docs under .github/ (no change to the Lean library):

  • .github/REVIEW.md — a fixed reviewer checklist. Splits machine gates (CI: build / no-sorry / linters / shake — don't re-check) from human dimensions (correctness, reuse, API, naming, generality), plus an adoption-PR section (faithful port, correct layer, axiom-clean, Review Issues — OpenGA Hopf–Rinow Formalization #112 exposure).
  • .github/PULL_REQUEST_TEMPLATE.md — author self-check mirroring the rubric.

Goal: reviews pass a repeatable checklist rather than ad-hoc judgment (borrowed from the TauCeti review model). Roles and the milestone are linked in REVIEW.md.

A fixed, repeatable review checklist (.github/REVIEW.md) and a PR template
(.github/PULL_REQUEST_TEMPLATE.md), so reviews score named dimensions
(correctness / reuse / API / naming / generality + adoption-specific
fidelity / layer / axiom-clean / #112 exposure) instead of ad-hoc judgment.
Machine gates stay in CI; the rubric covers what CI can't.
@Xinze-Li-Moqian
Xinze-Li-Moqian merged commit 4837006 into main Jul 21, 2026
3 checks passed
@Xinze-Li-Moqian
Xinze-Li-Moqian deleted the chore/review-rubric branch July 21, 2026 14:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant