feat(scripts): @[expose] removal-candidate report pipeline (draft)#217
Draft
kim-em wants to merge 27 commits into
Draft
feat(scripts): @[expose] removal-candidate report pipeline (draft)#217kim-em wants to merge 27 commits into
kim-em wants to merge 27 commits into
Conversation
Adds three scripts under `scripts/` for identifying Mathlib `@[expose]` defs that are not unfolded downstream (candidates for un-exposing): - `scripts/expose_enumerate.lean` (`lake exe expose_enumerate`) dumps every Mathlib `def`/`instance` whose body is currently in the exported view of the environment as JSONL. - `scripts/build_with_diagnostics.py` patches `lakefile.lean` to enable `set_option diagnostics true` / `diagnostics.threshold`, runs a full `lake build Mathlib`, parses per-file unfold counts. - `scripts/expose_report.py` joins the two, filters out same-module unfolds, and emits sorted JSONL/TSV/Markdown reports with zero-usage rows first. Motivated by Sebastian Ullrich's observation that `diagnostics=true` provides the unfold signal that `shake` lacks. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…peline When `build_with_diagnostics.py` enables `set_option diagnostics true` globally via `leanOptions`, five files in Mathlib fail to elaborate: four `#guard_msgs` mismatches caused by extra `[diag]` info messages, and one `aesop`/`naturality` synth failure in `Mathlib/CategoryTheory/Discrete/Basic.lean` that empirically also goes away with diagnostics off. The script now temporarily inserts `set_option diagnostics false` after the imports of each affected file before running `lake build`, and restores the originals via the same `try / finally` that restores `lakefile.lean`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… used instances` The diagnostic-based zero-usage signal previously included only the four unfold categories from `set_option diagnostics true`. Empirically, that missed cases where a downstream module's typeclass synthesis depends on an exposed instance's body without ever recording an explicit `recordUnfold`. Adding `[type_class] used instances` to the parsed categories drops ~1.6k decls (4%) from the zero-usage list — those are load-bearing and were previously misclassified as "safe". The widening doesn't fully close the gap: instance synthesis via parent-class projection (e.g. `SemilatticeSup` synthesized via `Lattice → Lattice.toSemilatticeSup`) records the projection instance, not the user-named `instLattice`, so reports for the user-named instance still show 0 usage even when it is load-bearing. The report remains useful as a candidate list for inspection, not a definitive safe list. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…line Adds a third complementary signal to the @[expose] removal-candidate report. The previous diagnostic-based signal had a blind spot for typeclass synthesis through parent-class projections: when a downstream module synthesizes `SemilatticeSup (Germ l β)` via `instLattice → Lattice.toSemilatticeSup`, Lean's `[type_class]` counter records `Lattice.toSemilatticeSup` (the projection) but not the source `Filter.Germ.instLattice`, so neither shows up as load-bearing. Worse, the projection chain `instLattice → instSemilatticeSup` is also invisible because `instSemilatticeSup` is only mentioned inside `instLattice`'s body, never directly in downstream code. Two new pieces: * `scripts/expose_static_refs.lean` (`lake exe expose_static_refs`). Walks the built env via `ConstantInfo.getUsedConstantsAsSet` and emits either per-(refModule, decl) aggregations (default mode) for cross-module reference counts, or per-decl reference lists (`decl` mode) for transitive closure. * `scripts/expose_report.py` now optionally consumes both `static_refs.jsonl` and `decl_refs.jsonl`. The latter enables one-hop transitive closure: any downstream use of decl K is propagated to every decl K's body references (filtered to cross-module edges as usual). On the `Mathlib.Order.Filter.Germ.Basic` test bench the candidate set goes from 4/7 correct (diagnostics only) → 7/7 (full pipeline). Total zero-usage candidates across Mathlib: 38k → 22.5k. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
A second test bench (Mathlib.Algebra.Order.Group.Synonym) exposed a
remaining false-positive class: a same-module `theorem ... := rfl`
that mentions an instance needs that instance's body to defeq, but the
report's same-module filter was unconditionally skipping intra-file
references. Without this signal, e.g. `OrderDual.instPow` shows
downstream_usage = 0 yet is load-bearing for `theorem toDual_pow := rfl`
in the same file.
Two changes:
* `expose_static_refs.lean` now tracks `theorem_count` per
(refModule, refName) pair: the subset of referencers that are `theorem`s
(proof-irrelevant, hence `:= rfl`-shaped intra-file uses).
* `expose_report.py` keeps same-module references when their
`theorem_count > 0`. A new `--include-same-module` flag (default off)
unconditionally counts same-module refs.
Validation across two new files:
Mathlib.Algebra.Order.Group.Synonym
- OrderDual.instPow: predicted load-bearing ✓ (was wrong before)
- OrderDual.instInvolutiveInv (usage=1): predicted load-bearing ✓
Mathlib.Data.Ordmap.Ordnode
- 7 zero-usage candidates un-exposed simultaneously: build passes ✓
Mathlib.Data.Num.Bitwise
- 4 zero-usage candidates un-exposed simultaneously: build passes ✓
Total: 19/19 predictions verified across two distinct kinds of files
(algebra synonyms + data structures + the original Filter.Germ test).
Total zero-usage candidates across Mathlib: 22.5k → 8.8k.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…mand First commit of the @[expose] removal-pipeline refactor (per /Users/kim/.claude/plans/can-you-decipher-sebastian-s-linked-duckling.md): introduces a single user-facing `lake exe no_expose` whose implementation lives in modular `scripts/NoExpose/*` files. The exe deliberately does NOT `import Mathlib`, so it builds in seconds; it loads Mathlib at runtime via `Lean.withImportModules` (proven in a deleted milestone-0 prototype). This commit lands: - `scripts/no_expose.lean` — tiny dispatch entry point - `scripts/NoExpose/Cli.lean` — hand-rolled subcommand parser - `scripts/NoExpose/Paths.lean` — data-artifact paths + Lake project autodetect (mirrors `scripts/mk_all.lean` / `scripts/lint-style.lean`) - `scripts/NoExpose/Report.lean` — reads `scripts/.no_expose/report.jsonl` (built by the legacy `expose_report.py` for now) and renders per-file text/json/tsv recommendations - `lakefile.lean` — `lean_lib NoExpose` + `lean_exe no_expose` registrations `collect` and `edit` are stubs that print "not yet implemented" and exit 1; `report` and `clean` are functional. The legacy 4-script pipeline is untouched and remains the source of truth for `report.jsonl` until the rest of the refactor lands and parity tests pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds NoExpose.Env (enumeration + static refs + decl refs, no Mathlib import) and NoExpose.Collect (orchestrator that opens the env once via withImportModules and emits all three JSONLs, then joins them into report.jsonl). With --skip-build, `lake exe no_expose collect` produces the same data shape as the old Python+Lean pipeline. Also restores `num_using_files` / `top_using_files` JSON keys; the prior `using` → `usingMap` rename (Lean keyword conflict) had leaked into the output. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Three more modules of the `lake exe no_expose` rebuild: * Restore: backup any file before patching, restore on cleanup or startup-detected orphan recovery (state.json sidecar). * Diagnostics: lakefile-patch (Mathlib-shaped only in v1) + per-fragile-file `set_option diagnostics false` patches + build-log parser (ports `build_with_diagnostics.py`). * Edit: section / individual / auto strategies for removing `@[expose]`. Defaults to apply; --dry-run previews. Skips files with uncommitted changes (--force-dirty overrides). Writes unified-diff-ish audit trail to scripts/.no_expose/edits.patch. The full-build path (Diagnostics.runDiagnostics) is implemented but not yet wired into the collect dispatch — `--skip-build` remains the default working mode. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Diffs the new `lake exe no_expose` artifacts against the legacy Python+Lean pipeline output saved at scripts/.expose_report. Compares line counts (per-record JSONL); flags any divergence. Current parity: exposed.jsonl 51638 / 51638 (identical) static_refs.jsonl 2550386 / 2550386 (identical) report.jsonl 51638 / 51638 (identical) decl_refs.jsonl 485820 / 485822 (2-row delta, edge-case noise) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Three fixes uncovered while validating the edit on `Mathlib/Order/Filter/Germ/Basic.lean`: 1. **Dedupe by source line** before inserting `@[expose]`. Macros like `to_additive` produce additional report rows that share the source line of the originating decl; without dedup the edit inserts `@[expose]` once per row. 2. **Walk forward from the report's decl-block start to the actual decl-keyword line.** `Lean.findDeclarationRanges?` returns the start of the decl block (doc comment / first attribute), not the `def`/`instance` line. The previous code walked backward from the block-start, which placed `@[expose]` *before* the doc comment — syntactically valid but semantically a no-op (the attribute floats instead of binding to the decl). 3. **Merge into existing `@[...]`.** Lean does not allow stacked attribute blocks before a single declaration; if the line above the decl is already `@[foo]`, rewrite it to `@[expose, foo]` instead of inserting a new line. After these fixes, `lake build Mathlib.Order.Filter.Germ.Basic` succeeds on the edited file (only emits "@[expose] has no effect" warnings on a handful of abbrevs — that's an over-approximation of load-bearing decls, harmless and the basis of further tightening). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Three follow-ups for `lake exe no_expose`: * `runCollect` now invokes `runDiagnostics` (lakefile patch + full `lake build Mathlib` + log parse) when called without --skip-build. Mathlib-only in v1; downstream projects get a clear error and are pointed at --skip-build. Restores backups via `detectOrphan` at startup (recovers from interrupted runs). * `edit --verify` now runs `lake build <module>` on each modified file. On non-zero exit the file is rolled back from its in-memory pre-edit copy. * Pre-write parse validation (differential): re-parses the file with only `Init` in scope and refuses to write if the new text has more syntax errors than the original. Mathlib-defined notations cause false-positive parse errors, but they cancel out when comparing before/after, so the differential count is reliable. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Removes the prior `expose_enumerate.lean` / `expose_static_refs.lean` / `build_with_diagnostics.py` / `expose_report.py` pipeline and its parity-test script. Adds a README entry for `lake exe no_expose` and moves the `.gitignore` entry from `scripts/.expose_report/` to `scripts/.no_expose/`. Drops the corresponding `lean_exe` registrations from the lakefile. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The previous commit replaced the line instead of supplementing it, leaving anyone who still has the legacy data directory locally with noisy untracked entries in `git status`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Almost no one will have that directory locally; one-time noise for a handful of upgraders isn't worth carrying the entry forever. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Replace the line-shifted `quickDiff` audit format (which produced 677 hunks for a 16-edit file and could not be applied with `git apply`) with a proper LCS-based unified diff: `--- a/...`, `+++ b/...`, and `@@ -A,B +C,D @@` hunks with three lines of context. Both the `--dry-run` stdout preview and the persisted `scripts/.no_expose/edits.patch` now apply cleanly via `git apply`. Gate the `edits.patch` append on apply mode; `--dry-run` no longer mutates the audit trail. Also switch a deprecated `String.dropRight` to `String.dropEnd` to silence a build warning. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Cleanup pass on the `no_expose` modules: - Drop the `--collect-on-demand` flag, which only ever printed a TODO. - Replace the "v1 punts on --verify" block in Edit.lean with a description of what --verify actually does. - Correct Diagnostics.lean's reference to a nonexistent --full-build flag and its inaccurate "stream line-by-line" docstring. - Lift `jsonEscape` from Env.lean and Report.lean into Paths.lean. - Drop the `let _ := project` marker line; rename binder to `_project`. - Trim Cli.lean module header. - Note the deliberate no-`import Mathlib` design in scripts/README.md. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Across `lake exe no_expose` (constructor, display strings, JSON field key, doc comments). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`no_expose edit` auto-detects section vs individual layout deterministically from file content; the user-facing `--strategy` override only ever produced no-ops when forced against the wrong file shape. `no_expose report --format tsv` was redundant with json. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Drop the `--all` flag: with no PATH arguments, report every file in `report.jsonl` (sorted) instead of erroring. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The individual-strategy stripper returned a bare `Option`, so every failed line was lumped into one anonymous "skipped" bucket and the bucket was logged *after* an early "no changes" return — meaning a file like `Mathlib/Util/WithWeakNamespace.lean` (no `@[expose]` on the decls; exposure comes from `public meta section`) just printed "no changes" with no explanation. Tag the skip reason (`noAttribute` vs `multiAttribute`), surface it before the early return, and add Case C in `stripIndividualOne` to recognise `@[expose, ...]` bundles as a distinct case. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds `NoExpose.SourceScan`, a text-level scanner that walks each
`.lean` source file once and classifies every top-level declaration
into one of `ExposeSource` ∈ {explicit, sectionAttr, meta, unknown}.
The env walk can only tell us *that* a constant is exposed, not *why*
— `@[expose]` is discarded at elaboration — so we reconstruct the
source by re-reading the file.
Threaded through the pipeline:
* `DeclRecord.exposeSource` populated by `augmentAndWrite` after the
env walk; written into `exposed.jsonl` as `expose_source`.
* `Verdict.classify` gains `nonAttrExposed` for the `meta`/`unknown`
cases; only `explicit`/`sectionAttr` decls can become
`safeToUnexpose`. This is the right fix for the
`Mathlib/Util/WithWeakNamespace.lean` false-positive: its decls
are exposed by `public meta section`, not by `@[expose]`.
* `Edit.chooseStrategy` picks `section` iff any record reports
`.sectionAttr`, replacing the previous text scan for
`@[expose] public section`.
KNOWN BAD: the standalone scanner test (run on
`Mathlib/Util/WithWeakNamespace.lean` and
`Mathlib/Analysis/Normed/Field/Lemmas.lean` via `lake env lean
--run`) produces the expected classifications, but the full `lake
exe no_expose collect --skip-build` run segfaults during the apply
phase, after successfully scanning all 5707 candidate files. Both a
nested `HashMap String (HashMap Nat _)` and a flattened `HashMap
(String × Nat) _` reproduced it. Streaming the augmented records
straight to disk (current state) hasn't been verified yet — the run
was killed before it reached the apply step on the most recent
attempt.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Resolves the SIGSEGV that hit consistently during the post-env-walk "apply" phase of `lake exe no_expose collect`. Root cause: `DeclRecord` fields included strings derived from `Name`s allocated inside the imported `Environment`. Even after stringifying `name` and `module` to `String` at enumeration time, *any* iteration over `recs` outside the `withImportModules` block segfaulted. The imported environment's arena-allocated string storage was being torn down on scope exit; the surviving record fields pointed into it. Fix: write `exposed.jsonl` *inside* `withImportModules` (the records are valid there), then release the env, then re-read the JSONL from disk for the source-scan pass. After re-read, the data is fully heap-allocated independent of any imported env state. `NoExpose.Env.augmentExposedFile` does the read-back-and-rewrite. It groups records by source file, scans each file once with a candidate-bounded `wanted` filter (so the per-file map size is at most the number of candidates in that file), joins, and streams the updated records back to disk. Single-file scan map alive at any moment; no global cross-file table. Verified end-to-end on Mathlib: * exit 0 (was 139) * expose-source breakdown printed: 65 explicit / 40,536 section / 1,843 meta / 9,194 unknown (51,638 total). * `lake exe no_expose report Mathlib/Util/WithWeakNamespace.lean` now correctly reports `3 non-@[expose]` (was `3 safe-to-unexpose` — the original bug). * `lake exe no_expose edit --dry-run` on the same file: clean "no changes" with no false skip diagnostics. * `lake exe no_expose edit --dry-run` on a `@[expose] public section` file (Normed/Field/Lemmas.lean): unchanged correct diff. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The previous fix worked around the env-arena lifetime issue by writing
`exposed.jsonl` inside `withImportModules` and then re-reading the file
back outside to do the source-scan + rewrite-in-place. That involved
parsing each JSONL line, surgically replacing the `expose_source`
field, and writing it back — brittle string surgery, and one disk
write more than needed.
Cleaner approach: do the source-scan *inside* `withImportModules` too.
`CoreM` has `IO`, so reading source files works fine there, and the
records are still valid for the duration of the block. Write
`exposed.jsonl` once with `expose_source` already filled in.
Deletes `parseExposedLine`, `setExposeSourceField`, and
`augmentExposedFile`. Replaces them with `sourceScanRecords`, which
returns a parallel `Array ExposeSource` and a per-source count map.
The caller in `Collect.lean` produces the augmented record on the fly
in the write loop:
```lean
let (sources, counts) ← sourceScanRecords recs
IO.FS.withFile exposedPath .write fun h => do
for h2 : i in [:recs.size] do
h.putStrLn { recs[i] with exposeSource := sources[i]! }.toJsonLine
```
Also fixes four doc/comment items flagged in review: stale JSON field
names in `Report.lean`'s module docstring (`num_using_files` not
`num_usingMap_files`), "three formats" wording leftover from before
the TSV removal, and three lingering `v1` qualifiers in `Edit.lean`
docstrings.
Verified end-to-end on Mathlib: same expose-source breakdown
(65/40536/1843/9194 = 51638) and identical per-file reports as the
previous in-place-rewrite version.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* Copyright lines: `Lean FRO, LLC` (was `Kim Morrison`); `Authors:` line kept as Kim Morrison. * Drop stale `v1` qualifiers in error messages and module headers (Collect.lean, Diagnostics.lean). * Drop references to the deleted legacy pipeline (`expose_enumerate`, `expose_static_refs.lean`, `expose_report.py`, `build_with_diagnostics.py`). * Drop the implementation-detail note about `withImportModules` being inlined from `Mathlib.Lean.CoreM`. * `NoExpose.SourceScan.declKws`: add `syntax`, `macro`, `macro_rules`, `notation`, `elab`, `elab_rules`, `infix`/`infixl`/`infixr`/ `prefix`/`postfix`. Sample of the `unknown` classifications turned up notation/macro/syntax-defined constants that the scanner was missing; on `Mathlib/Tactic/ByCases.lean` `byCases!` now correctly classifies as `.meta` (was `.unknown`). The remaining `.unknown` cases are concentrated in files heavy with `to_additive`-style macros that generate anonymous instances; those have no `@[expose]` to remove and would need an upstream fix in the env-walk's instance filter, not in the scanner. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`Lean.findDeclarationRanges?.range.pos` reports the *block-start* line for `def`/`theorem`-shaped declarations (i.e. the first leading doc-comment or attribute line) but reports the *keyword* line for `macro`/`syntax`/`elab`-shaped declarations. The scanner used to emit only the block-start, so env records for `macro` decls — which point at the keyword line — never matched any scanner entry and fell back to `.unknown`. `scanFile` now emits `(blockStartLine, headLine, ExposeSource)`; `sourceScanRecords` inserts both lines into the per-file lookup map. Effect on Mathlib full collect: 8645 → 8415 `unknown` (230 fewer), mostly redistributed to `section` (+176) and `meta` (+54). Cumulative since the source-scan landed: 9194 → 8415 (~8.5% reduction). The remaining unknowns are still dominated by macro-generated anonymous instances. The deeper fix is upstream: `withImportModules` loads the env's constants but the `Lean.Meta.instanceExtension` state stays empty (`instanceNames.size == 0`), so our instance filter sees nothing and all instances make it through enumeration. Worth a separate investigation / bug report against Lean core. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Inverts the candidate-selection model. Previously `enumerate` walked every body-exposed `defnInfo` in the imported env (~51,638 candidates in Mathlib) and then a separate scanner tried to classify *why* each was exposed, with everything we couldn't classify ending up in a noisy `unknown`/`meta`/`nonAttrExposed` bucket of ~8-14k records. The new model: scan source for literal `@[expose]` occurrences and intersect them with env declaration ranges. The tool can only edit `@[expose]` attributes that exist in source, so this drives candidate selection directly from those occurrences. * `NoExpose.SourceScan` now exposes a tiny `scanExposeOccurrences` that emits one `ExposeOccurrence` per `@[expose]` text occurrence, carrying its source position and scope (`decl` vs `section_` with the section's closing line — including an end-of-file flush for sections that aren't closed explicitly, which is the Mathlib convention). * `NoExpose.Env.enumerate` now intersects scanned occurrences with `findDeclarationRanges?` ranges per file, emitting one `DeclRecord` per (occurrence, covered env decl) pair. The env stays the authority for names, ranges, kinds, and usage; the scanner only drives selection. `DeclRecord` gains `attrLine` (where the `@[expose]` text is) and `sectionLine` (set iff the attr is a section attribute). * `NoExpose.Report.Verdict` drops `nonAttrExposed` and the whole `ExposeSource` taxonomy. Three verdicts remain: `safeToUnexpose`, `neededDownstream`, `noopAlwaysExported`. By construction every record represents an actually-editable attribute. * `NoExpose.Edit.chooseStrategy` now keys off `sectionLine.isSome` (was: `ExposeSource == .sectionAttr`). Same logical decision, honest schema. * `editOneFile`: a source line is only safe to unexpose if *every* record at that line is safe — so we exclude any line that also appears in `neededDownstreamLines`. This handles `to_additive` twins (where one name is unused but its companion is needed). Verified end-to-end: * `lake exe no_expose collect --skip-build`: 46,538 records (down from 51,638), all of which correspond to a real `@[expose]` source occurrence. No more `unknown` taxonomy. * `report Mathlib/Util/WithWeakNamespace.lean` (the originally-broken case): "no exposed decls in report" — correct; this file has no `@[expose]`. * `report Mathlib/Analysis/Normed/Field/Lemmas.lean`: 4 records, all classified as `needed-downstream`. Unchanged behaviour vs the previous design for files that work. * `edit --dry-run` on `Lemmas.lean`: same correct diff as before. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Three intertwined edit bugs surfaced when applying section-strategy edits to `Mathlib/CategoryTheory/Limits/Cones.lean` and others: * `declKeywordLineFrom` treated multi-line `@[to_dual (attr := simps) /-- doc -/]` blocks as single-line attributes followed by a stray doc-comment line, overshooting the decl keyword. * The previous "merge into the existing `@[...]` block by prepending `expose, `" approach corrupted macros like `@[to_dual]` / `@[to_additive]` whose argument syntax can contain embedded `/-- doc -/`s. The previous "stack `@[expose]` on its own line above the decl" alternative is a Lean syntax error — `declModifiers` only permits one `@[...]` block per declaration. * Multiple records (e.g. a `to_dual` twin's record alongside the source's) could resolve to the same decl-keyword line and inject `expose` twice. Now: * `declKeywordLineFrom` recognises multi-line `@[...]` blocks (walks until a line ending in `]`, mirroring the existing handling of multi-line `/-- doc -/`). * `attrBlockBefore` finds the *one* attribute block immediately before the decl keyword, bounded to a small lookback window so it can never match a stray `]` from unrelated upstream content. * `applySectionStrategy` chooses between three placements: insert a fresh `@[expose]` line when no attribute block exists, otherwise append `, expose` to the existing block's body. Propagator macros (`to_dual`, `to_additive`) re-expose the twin automatically when the source is exposed (see `Mathlib.Tactic.Translate.Core`), so no special-casing is needed for them. * A per-`declIdx` `seen` set prevents double injection from twin records. Verified end-to-end on three files via `lake exe no_expose edit --verify`: * `Mathlib/Order/SetNotation.lean`: edit applies, `lake build` passes. * `Mathlib/CategoryTheory/Limits/Cones.lean`: edit applies, `lake build` passes (previously failed). * `Mathlib/Data/Ordmap/Ordnode.lean`: edit applies cleanly but `lake build` rolls it back — `Any.decidable` is marked safe-to-unexpose yet `Amem.decidable`'s `inferInstanceAs <| Decidable (Any _ t)` needs its body. That's a separate downstream-usage-signal gap (the diagnostics + static-refs data doesn't capture every instance-synthesis dependency), not a tool bug; `--verify` correctly catches it and rolls back. Co-Authored-By: Claude Opus 4.7 (1M context) <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 adds three scripts under
scripts/for identifying Mathlib@[expose]defs that aren't unfolded downstream (candidates for un-exposing):scripts/expose_enumerate.lean(lake exe expose_enumerate) dumps every Mathlibdefwhose body is currently in the exported view as JSONL.scripts/build_with_diagnostics.pypatcheslakefile.leanto enableset_option diagnostics true/diagnostics.threshold 0, runs a fulllake build Mathlib, and parses per-file unfold counts.scripts/expose_report.pyjoins the two, filters out same-module unfolds, and emits a sorted TSV report (zero-usage rows first).Motivated by Sebastian Ullrich's observation that
diagnostics=trueprovides the unfold signal thatshakelacks. Unblocked by leanprover/lean4#13630 (set_option diagnostics truepreviously crashed on private_sparseCasesOn_*helpers under the module system; fixed in nightly-2026-05-07).This is a draft for triggering CI / populating cache. Not intended to be merged as-is.
🤖 Prepared with Claude Code