Repository navigation
perf(api): measure and shrink the public declaration surface #584
Description
The module template's @[expose] public section makes nearly every declaration public. main has 18,113 public theorems against 2,115 private ones. Every public declaration is API that users must navigate and that carries deprecation obligations. Under the module system it is also part of the interface: adding one, or changing its statement, can invalidate downstream build artifacts (#569). Helpers that no other module uses don't need to be public.
1. Measure. Use the .ilean reference data that Lake already produces, or an equivalent Lean environment traversal. For every public declaration in Complexity/, count references from other library modules, from ComplexityTests/ only, and from abstracts/. Report by directory:
- never referenced outside their module;
- referenced only by tests;
- used by other modules.
Also count @[expose] definition bodies that no other module unfolds. Spot-check a sample against grep. Make the script reproducible and keep it under scripts/.
2. Pilot. In one or two high fan-out areas (for example Foundations/Data/List or a crypto directory), make the never-used-elsewhere helpers private, and narrow @[expose] where bodies aren't needed. Keep every public statement users rely on, and record the before/after interface size and the downstream invalidation effect of a typical helper edit. Clean-build time is expected to be roughly unchanged; the gain is in incremental rebuilds and API size. Say so honestly.
3. Policy. Propose a short AGENTS.md rule: helpers private by default, public only for intended API. Include the upstream implications (cslib conventions) and a compatibility rule for previously public names: a deprecation alias where outside users plausibly depend on them.
Done when: the measurement is published, the pilot has landed with measured effects, and the policy is proposed. Broad privatization across the library is follow-up work, done area by area, coordinated so it doesn't collide with in-flight PRs.
Endorsed by Samuel (2026-10-23).
Activity
SamuelSchlesinger commentedon Oct 23, 2026
Claimed by worker
worker-claude-584-c4b0c164(Claude Code, Opus 5.5), delegated by coordinatorcoordinator-claude-c4b0c164-20261023. Scope: Phase 1 only — the measurement script underscripts/and the published counts. Pilot privatization and the policy proposal wait for the coordinator's choice of area. Branch:perf/public-surface-584. State: active.SamuelSchlesinger commentedon Oct 23, 2026
worker-claude-584-c4b0c164: active. Scope widened by the coordinator to the shared #587 report:scripts/quality_report.py(with a small.oleanreader,scripts/QualityReport.lean) now computes this issue's reference classification plus the #587 per-area signals. Validating; baseline tables and the PR follow on branchperf/public-surface-584.feat(scripts): report public surface and quality signals per area
SamuelSchlesinger commentedon Oct 23, 2026
Measurement (Phase 1) at
main2549de63, produced byscripts/quality_report.py(#604). The same run produces the #587 per-area baseline.Of 26,376 public declarations written in
Complexity/, 11,815 (45%) are used by other library modules, 3,869 (15%) only by tests or abstracts (3,834 by tests), and 10,692 (41%) never outside their own module. 7,966 of those 10,692 are used inside their module (helpers) and the rest nowhere (terminal results or dead code). After setting aside declarations that may be used without being named (2,008:simp,fun_prop,aesop, instances, notation), that are named in module docs or READMEs (2,105), that are deprecated (314), and that a staying-public statement or exposed body mentions (1,039), 5,226 privatization candidates remain: 4,929 theorems and 297 definitions.Most candidates are theorems used only in the proofs of their own module, so privatizing them needs no statement changes. Definitions are mostly pinned by public statements, so a definition becomes private only together with the statements that mention it.
Exposure. 5,991 definitions are exposed through
@[expose](instances and abbreviations, which are exposed by default, are excluded). No other library module references 2,283 of them, and 2,023 more are referenced but never unfolded by name (unfold,delta, an element of asimp/rwlist, an equation lemma). That's evidence, not proof, that the body isn't needed, sincerflanddecideunfold silently. Tests and abstracts are non-module files that load private data, so they see every body whether or not it's exposed.Modules with the most declarations never referenced outside them
Computability.GenericRAM.Simulation.RunComputability.Machines.Turing.MultiTape.Halting.PartrecComputability.Machines.Turing.SingleTape.PartrecComputability.Complexity.Classes.ValiantVazirani.ReductionComputability.Circuit.Boolean.Iteration.PrimeCyclesComputability.Circuit.Rational.LaurentReductionComputability.Complexity.Classes.MIP.NEXPComputability.TreeEval.Reader.Cert.StepComputability.GenericRAM.Simulation.TuringComputability.Circuit.Rational.AffineComputability.Circuit.Boolean.CarrySaveComputability.Complexity.Classes.Space.GeneralizedGeography.ReductionComputability.Complexity.Parameterized.VertexCover.BussKernelComputability.Complexity.Classes.Alternation.GuessVerifyComputability.Complexity.Classes.ArthurMerlin.GraphNonIsomorphismComputability.Complexity.AffineDisperser.PolyTimeComputability.Circuit.Monotone.BipartiteMatchingComputability.Circuit.Boolean.WeightedThreshold.PotentialComputability.Complexity.Problems.SubsetSumComputability.Machines.Turing.MultiTape.Universal.ComposeMethod. References come from the
.ileanfiles that Lake writes beside each.olean. Lean's frontend fills them from the info trees of every command, including asynchronously elaborated proofs (Lean.Elab.Frontend,Lean.Server.References.findModuleRefs). Each reference records a full constant name with its defining module, the source range and the enclosing declaration. Only identifiers written in the source are recorded, never macro output. A small reader,scripts/QualityReport.lean, reads the three.oleanparts without importing them. It provides the declaration list, kinds, export status, docstrings, declaration ranges and the same-module constants that each exported statement or exposed body mentions. References to generated constants (.eq_1,.induct,.mk,.rec,.injEq,simpsandto_additivelemmas, …) count for their owner, and fields and constructors count for their structure.Reliability.
grep, and every classification held. One apparent cross-module use ofExtOp.majorityDeMorganCircuitturned out to be the unrelatedCslib.Circuits.Boolean.majorityDeMorganCircuit.Complexity/,ComplexityTests/orabstracts/. In a random sample of 25 from the remaining 1,954, every match was a name collision (mono,refl,run, …) or a doc mention, never a missed reference.to_additivelemmas and identifiers inside⟪…⟫notation, where the.ileandata is right.Caveats.
match_,_proof_andeq_Nnames.fun_prop, Aesop rules, instance resolution,ext/refl/trans,program_certificate,fo_realize. These declarations are flagged and kept out of the candidates. Explicit uses such assimp [foo],attribute [simp] fooand double-backtick names in tactic code are recorded.u ≼ vrecords nothing forBigOLe. Declarations named on the right-hand side of a notation, macro or syntax command are therefore flagged.open,exportand dot-notation resolution. Text-based checks have to allow for them, which is why the cross-check above uses final name components.What the module system treats as interface (from the toolchain source and a scratch-module experiment):
Importers rebuild when the exported
.oleanbytes change. Lake's trace for a plain import uses only that file's hash, with early cutoff;import alland non-module files (our tests and abstracts) also depend on the private parts.The exported
.oleanholds public statements (theorems become axioms), exposed bodies, inductive types, attribute entries for public declarations and compiler signature data. It also records the axioms each exported declaration's proof uses (exportedAxiomsExt).Docstrings and declaration ranges live in
.olean.serverand are not part of that trace.Measured on a scratch module, the exported
.oleanstayed byte-identical after:It changed after adding a public theorem, changing an exposed body, and, surprisingly, after a proof edit that changed the axiom set (
simp→decide:[propext, Quot.sound]→[]). Proof edits are interface-neutral only while the axioms they use stay the same, which in practice they almost always do.Rebuild fan-out is often much smaller than the set of transitive importers, because only
public importchains propagate.Foundations.Data.Fin.Tuplehas 693 transitive importers, but an interface change rebuilds only 146 modules.Private
@[simp]lemmas,@[aesop]rules and instances work inside their module and are not exported. A private@[fun_prop]theorem is different: Mathlib'sfun_propextension exports the entry anyway, andfun_propin an importing module then fails withUnknown constant `_private…`. A privatefun_prophelper needsattribute [local fun_prop], which works and exports nothing. A non-module test can't name a private declaration either, so privatizing a declaration that tests use means changing the tests.Pilot candidates (for the coordinator and Samuel). The largest invalidation payoff, measured as candidates times rebuild fan-out, is in the Machines and Circuit areas (
Universal.Compose,Encodings.Decoder,Complexity.BigO,Circuit.Depth). Both areas are Codex's.List(perf(list): split Basic into narrow topic modules and migrate consumers #573):BitString.Weight(fan-out 380),BitString.Block(346),Probability.Conditioning(159),StackTapeandBiTape(about 115 each) andBitString.PartialAssignment. It has few candidates in modules with high fan-out, so the before/after effect of a helper edit is easy to measure.PCP/ConstraintGraph,AssignmentTester,DegreeReduction,Classes/PHandReduction, with 1,486 candidates in that area.active: Phase 1 is done; the PR is #604 (awaiting review). Waiting for the pilot choice before any source edits.SamuelSchlesinger commentedon Oct 23, 2026
worker-claude-584-c4b0c164: the coordinator moved privatization to the area leads (#587), so there is no separate pilot. The policy is in #609 (a CONTRIBUTING subsection on the public surface under the module system, built on #604). State:awaiting reviewfor both #604 and #609.feat(scripts): report public surface and quality signals per area
SamuelSchlesinger commentedon Oct 23, 2026
worker-claude-584-c4b0c164: I addressed the #604 review ine8977be8: custom build directories are now checked, areas follow #587's assignments, and documentation in any module protects a declaration. Re-review is requested. #609 (policy) is awaiting review. Once #604 lands, I'll rerun the #587 baseline with the corrected area map.doc(contributing): state the public-surface rules of the module system
SamuelSchlesinger commentedon Oct 23, 2026
worker-claude-584-c4b0c164: both PRs are approved at their heads bycoordinator-codex-01a16ab8. #604 (scripts/quality_report.py) is approved at5ce04ec8and #609 (CONTRIBUTING policy) at52104e32; required CI is running on both. Once #604 lands, the #587 baseline needs a rerun with the corrected area map. Since2549de63, every path exceptInithas an owner.doc(contributing): state the public-surface rules of the module system
feat(scripts): report public surface and quality signals per area
SamuelSchlesinger commentedon Oct 24, 2026
Done. #604 delivered the measurement (
scripts/quality_report.py) and #609 the policy, both merged. Ongoing shrinking now runs under #587, which reruns the report after each area PR. —coordinator-claude-c4b0c164-20261023, after an issue audit byreviewer-claude-c4b0c164-01against main at about 17:00 UTC.