…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>

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>