From 8b204531842638a4f39b0a1812a96ae7ef68d66c Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 19:13:31 -0400 Subject: [PATCH 1/2] doc(contributing): state the public-surface rules of the module system Records what invalidates importers under Lean's module system, as measured for #584: only the exported `.olean`, which holds public statements, exposed bodies, public attributes and each public declaration's axiom set. Helpers are private by default, `@[expose]` stays on bodies that downstream proofs unfold, private `fun_prop` rules use `attribute [local fun_prop]`, and tests and abstracts are updated when a declaration they name becomes private. Refs #584, #587 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- CONTRIBUTING.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 858d5e329..324ac92f2 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -53,6 +53,21 @@ Mathlib's standard linter set already enforces the mechanical part; reviews enfo Improving an interface never weakens the mathematics: keep the models, encodings, independent resource bounds and nonvacuity of the results it touches. +### Public surface under the module system + +Importers rebuild only when a module's exported `.olean` changes. That file holds public +statements, exposed bodies, attributes of public declarations, and the axioms each public +declaration depends on. Editing docstrings, private declarations, proofs or non-exposed bodies +leaves it unchanged, unless a proof edit changes that axiom set. + +- Helpers are `private` by default. Keep `@[expose]` for bodies that downstream proofs unfold. +- A private `@[fun_prop]` theorem still exports its rule, and `fun_prop` then fails in importers. + Write `attribute [local fun_prop] helper` instead. Private `simp` lemmas, Aesop rules and + instances stay local. +- Tests and abstracts cannot name private declarations, so update them in the same PR. +- `scripts/quality_report.py` shows where each declaration is used and which exposed bodies no + other module unfolds. Its counts are review signals, not rules. + ## AI assistance and review AI-assisted and human-written contributions follow the same standards. Disclose which AI tools From 52104e32e8b24f5bff7e4eacfc1a821c96f05c37 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 19:29:13 -0400 Subject: [PATCH 2/2] doc(contributing): qualify the module-system rules for `import all` and the report Addresses the review of #609. The rebuild and private-access rules hold for ordinary imports; `import all` also loads private information and lets a companion module use it. The report records references and named unfolding, not reduction by `rfl` or `decide`. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- CONTRIBUTING.md | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 324ac92f2..1f3f88ef8 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -55,18 +55,21 @@ resource bounds and nonvacuity of the results it touches. ### Public surface under the module system -Importers rebuild only when a module's exported `.olean` changes. That file holds public -statements, exposed bodies, attributes of public declarations, and the axioms each public -declaration depends on. Editing docstrings, private declarations, proofs or non-exposed bodies -leaves it unchanged, unless a proof edit changes that axiom set. +Under an ordinary `import`, importers rebuild only when a module's exported `.olean` changes. That +file holds public statements, exposed bodies, attributes of public declarations, and the axioms +each public declaration depends on. Editing docstrings, private declarations, proofs or +non-exposed bodies leaves it unchanged, unless a proof edit changes that axiom set. `import all` +also loads private information, so such edits do reach its clients. - Helpers are `private` by default. Keep `@[expose]` for bodies that downstream proofs unfold. - A private `@[fun_prop]` theorem still exports its rule, and `fun_prop` then fails in importers. Write `attribute [local fun_prop] helper` instead. Private `simp` lemmas, Aesop rules and instances stay local. -- Tests and abstracts cannot name private declarations, so update them in the same PR. -- `scripts/quality_report.py` shows where each declaration is used and which exposed bodies no - other module unfolds. Its counts are review signals, not rules. +- Ordinary imports cannot name private declarations. When privatizing, update the tests and + abstracts that name them in the same PR, or give a companion module `import all`. +- `scripts/quality_report.py` records where each declaration is referenced and where other modules + unfold a definition by name. Reduction by `rfl` or `decide` is not recorded, and its counts are + review signals, not rules. ## AI assistance and review