chore(project): shrink public module interfaces - #22
Draft
BoltonBailey wants to merge 3 commits into
Draft
Conversation
Under the module system a module's interface is what every downstream module must rebuild against. Two things inflate it: `public import X` re-exports X to everything downstream, and `@[expose]` puts a definition's body in the interface rather than just its signature. This narrows both, mechanically and conservatively: - 525 of 920 blanket `@[expose] public section` become `public section`, so definition bodies stay private to their defining module; - 113 `public import X` become `import X`, as reported by `lake shake`. Only removals were applied. Shake also suggests compensating *additions* to restore a public closure it has narrowed; those are deliberately ignored, so this can only shrink an interface, never widen one. Every individual change was verified by a full build of all five CI targets and reverted if it broke anything, so no proof was weakened or adjusted to accommodate a narrower interface. Measured effect on the built artifacts: 891 KB moved out of a 68.75 MB public interface, with the private side growing by the same amount. The reach of `@[expose]` is limited here because a public theorem's statement stays in the interface regardless, and this library is mostly theorems. The remaining 395 exposes and the rest of shake's import report are untouched; they are the candidates whose removal did not build. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Second batch of the mechanical interface narrowing begun in the previous commit, produced and verified the same way: only removals are applied, each one is gated on a full build of all five CI targets, and anything that breaks is reverted rather than accommodated. - 48 further `@[expose] public section` become `public section`; - 19 further `public import X` become `import X`. The expose pass is now complete: 573 of 920 blankets removed, 347 left because their definition bodies are genuinely needed downstream. The import pass ran a fresh `lake shake` afterwards and is roughly 9% done. Two findings worth recording, both arguing against expecting much more from this direction: Re-scanning after 573 de-exposures unlocked only about 37 newly-legal import demotions (~1011 candidates expected, 1048 found). De-exposing does make demotions legal that were not before, but the effect is small here. Acceptance falls off sharply with a module's downstream reach. The expose pass ran cone-size ascending and went from ~86% accepted among near-leaves to ~44% among the widely-imported modules, where almost any downstream proof that unfolds a definition blocks the change. The public surface of this library is largely load-bearing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`scripts/shake_minimize.py` drives the mechanical narrowing performed in the two preceding commits, and can resume it. Under the module system a module's interface is what downstream modules rebuild against. `public import X` re-exports X to everything downstream, and `@[expose]` puts a definition's body in the interface rather than just its signature. The two constrain each other: a public declaration's signature may only mention names from public imports, and an exposed body must too, so de-exposing is what makes some import demotions legal. The script runs either shrink as a resumable queue. The safety property is that it only ever applies *removals*. `lake shake` also suggests compensating *additions* to restore a public closure it has narrowed; those are deliberately ignored, so a change that would need one simply fails its build and is rolled back. Every candidate is verified by a full build of all five CI gate targets individually, and no proof is ever adjusted to accommodate a narrower interface. Implementation notes: - imports may wrap across two lines to satisfy the 100-column limit, so edits work on whole import statements and re-wrap only when needed; - `meta import` lines are never touched, and shake's `-- shake: keep` and `keep-all` annotations are honoured; - expose candidates are ordered by transitive dependent count ascending, which front-loads the cheap, near-certain wins — a module can only break things downstream of it, and that cone is also the rebuild cost; - state is rewritten after every verified step and SIGTERM is trapped, so an interrupted run leaves the tree at the last green state. CONTRIBUTING.md documents the expose-before-imports workflow. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR removes
exposeandpublic, to try to make the import interface more minimal and make the library in general faster to compile.🤖 Generated with Claude Code