Skip to content

Commit 0083183

Browse files
kim-emclaude
andcommitted
chore(scripts): widen expose-pipeline parser to include [type_class] 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>
1 parent fac6ec2 commit 0083183

1 file changed

Lines changed: 8 additions & 3 deletions

File tree

scripts/build_with_diagnostics.py

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -204,20 +204,25 @@ def run_build(log_path: Path) -> int:
204204
)
205205
# Header: ` [reduction] unfolded declarations (max: N, num: M):`
206206
CATEGORY_HEADER_RE = re.compile(
207-
r"^\s*\[(reduction|kernel)\]\s+(unfolded declarations|"
208-
r"unfolded instances|unfolded reducible declarations)\s*"
207+
r"^\s*\[(reduction|kernel|type_class)\]\s+(unfolded declarations|"
208+
r"unfolded instances|unfolded reducible declarations|used instances)\s*"
209209
r"\(max: \d+, num: \d+\):\s*$"
210210
)
211211
# Entry: ` [reduction] Foo.bar ↦ 3`
212212
ENTRY_RE = re.compile(
213-
r"^\s*\[(reduction|kernel)\]\s+(\S.*?)\s+↦\s+(\d+)\s*$"
213+
r"^\s*\[(reduction|kernel|type_class)\]\s+(\S.*?)\s+↦\s+(\d+)\s*$"
214214
)
215215

216+
# `type_class / used instances` is needed because instance synthesis can
217+
# rely on a downstream-exposed body without ever recording an explicit
218+
# `recordUnfold` event (e.g. typeclass projection through a parent class).
219+
# Empirically, the report misses such uses if this category is omitted.
216220
CATEGORY_SHORT = {
217221
("reduction", "unfolded declarations"): "reduction/unfolded",
218222
("reduction", "unfolded instances"): "reduction/instances",
219223
("reduction", "unfolded reducible declarations"): "reduction/reducible",
220224
("kernel", "unfolded declarations"): "kernel/unfolded",
225+
("type_class", "used instances"): "type_class/used",
221226
}
222227

223228

0 commit comments

Comments
 (0)