From 3dae18ca2315982235151ac2222e85ee0f1d9df4 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 8 May 2026 10:12:50 +1000 Subject: [PATCH 01/27] feat(scripts): add @[expose] removal-candidate report pipeline 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) --- .gitignore | 2 + lakefile.lean | 8 + scripts/README.md | 15 ++ scripts/build_with_diagnostics.py | 276 ++++++++++++++++++++++++++++++ scripts/expose_enumerate.lean | 170 ++++++++++++++++++ scripts/expose_report.py | 159 +++++++++++++++++ 6 files changed, 630 insertions(+) create mode 100755 scripts/build_with_diagnostics.py create mode 100644 scripts/expose_enumerate.lean create mode 100755 scripts/expose_report.py diff --git a/.gitignore b/.gitignore index 3c886f148965e4..89ca47c750a1b6 100644 --- a/.gitignore +++ b/.gitignore @@ -8,3 +8,5 @@ **/__pycache__/ # Progress file from scripts/rm_set_option.py scripts/.rm_set_option_progress.jsonl +# Output directory from scripts/build_with_diagnostics.py and expose_report.py +scripts/.expose_report/ diff --git a/lakefile.lean b/lakefile.lean index c6ef52a6ff89f8..2868b5482fe9e1 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -127,6 +127,14 @@ lean_exe «check_title_labels» where lean_exe «nightly-testing-checklist» where srcDir := "scripts" +/-- `lake exe expose_enumerate` prints a JSONL list of every `def`/`instance` +in Mathlib whose body is currently in the exported view of the environment, +i.e. would be a candidate for un-exposing if it's not unfolded downstream. +Consumed by `scripts/expose_report.py`. -/ +lean_exe expose_enumerate where + srcDir := "scripts" + supportInterpreter := true + lean_exe mathlib_test_executable where root := `MathlibTest.MathlibTestExecutable diff --git a/scripts/README.md b/scripts/README.md index d2d5a2dc822347..4910f1e1b54b62 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -186,6 +186,21 @@ to module `Foo.Bar` (no `srcDir` indirection). lists (which occasionally leave lines over the 100-char limit). Usage: `scripts/fix_long_lines.py path:line ...` +- `expose_enumerate.lean`, `build_with_diagnostics.py`, `expose_report.py` + Three-stage pipeline that reports `@[expose]`-annotated defs which are not + unfolded by any other Mathlib file — i.e. candidates where `@[expose]` can + likely be removed. Stage 1: `lake exe expose_enumerate` dumps every exposed + def from the built Mathlib environment to JSONL. Stage 2: + `python3 scripts/build_with_diagnostics.py` patches `lakefile.lean` to + enable `set_option diagnostics true` / `diagnostics.threshold 0`, runs a + full `lake build Mathlib` (expect several hours; the change affects olean + hashes so cache is bypassed), and parses per-file unfold counts into + JSONL. Stage 3: `python3 scripts/expose_report.py` joins the two, filters + out same-module unfolds, and emits `report.tsv` sorted with zero-usage + decls first. Signal limitation: metaprograms that inspect + `ConstantInfo.value?` without a WHNF unfold will not appear in the + diagnostics, so a zero-usage row may still be load-bearing. + **CI workflow** - `lake-build-with-retry.sh` Runs `lake build` on a target until `lake build --no-build` succeeds. Used in the main build workflows. diff --git a/scripts/build_with_diagnostics.py b/scripts/build_with_diagnostics.py new file mode 100755 index 00000000000000..aab632505f37e2 --- /dev/null +++ b/scripts/build_with_diagnostics.py @@ -0,0 +1,276 @@ +#!/usr/bin/env python3 +""" +Part of the `@[expose]` removal-candidate reporting pipeline +(see `scripts/expose_enumerate.lean` and `scripts/expose_report.py`). + +Runs a full `lake build Mathlib` with `diagnostics=true` and +`diagnostics.threshold=0` enabled, captures per-file diagnostic output, and +emits one JSONL record per unfold event observed during elaboration. + +Workflow: + 1. Patch `lakefile.lean` to append the diagnostics options to + `mathlibLeanOptions` (this *does* affect the olean hash; a full local + rebuild is expected). + 2. Run `lake build Mathlib`, streaming and teeing output to + `scripts/.expose_report/build.log`. + 3. Parse the captured log into per-file unfold records. + 4. Emit `scripts/.expose_report/diagnostics.jsonl` — one record per + (file, decl, category) triple. + 5. Restore `lakefile.lean` (always; even on failure / Ctrl-C). + +Expected runtime: several hours for a full Mathlib rebuild with diagnostics. +Kim signed off on this cost: this is a one-off / occasional report. + +Usage: + python3 scripts/build_with_diagnostics.py + python3 scripts/build_with_diagnostics.py --skip-build # re-parse existing log + python3 scripts/build_with_diagnostics.py --log PATH # use alt log path + +Output records: + { + "file": "Mathlib/Foo/Bar.lean", + "decl": "Other.Module.name", + "count": 3, + "category": "reduction/unfolded" | "reduction/instances" + | "reduction/reducible" | "kernel/unfolded" + } + +Limitations: + * Signal is unfold-based; metaprograms that inspect `ConstantInfo.value?` + without triggering a WHNF unfold don't appear here. A decl absent from + this output may still be load-bearing downstream via metaprogramming. + * `diagnostics.threshold` is set to `0`: every unfold appears in the + report (counts > 0, since the threshold check is strictly-greater-than). + A "never unfolded downstream" verdict means absence from the per-file + diagnostic output — Lean does not emit zero-count rows. Un-exposure + candidates should still be verified by trying the change and + re-building, since metaprograms that inspect `ConstantInfo.value?` + without a WHNF unfold won't appear here either. + + Note: low thresholds previously triggered + https://github.com/leanprover/lean4/issues/13581 (private-helper + rendering crash) on `nightly-2026-05-06` and earlier. Fixed by + https://github.com/leanprover/lean4/pull/13630 (in + `nightly-2026-05-07` and later). +""" + +import argparse +import json +import os +import re +import shutil +import signal +import subprocess +import sys +from pathlib import Path + + +REPO_ROOT = Path(__file__).resolve().parent.parent +LAKEFILE = REPO_ROOT / "lakefile.lean" +OUTPUT_DIR = REPO_ROOT / "scripts" / ".expose_report" +DEFAULT_LOG = OUTPUT_DIR / "build.log" +DEFAULT_JSONL = OUTPUT_DIR / "diagnostics.jsonl" + +PATCH_MARKER_BEGIN = "-- BEGIN expose_report diagnostics patch" +PATCH_MARKER_END = "-- END expose_report diagnostics patch" + +# The extra LeanOptions lines inserted into `mathlibLeanOptions`. +PATCH_BLOCK = f""" {PATCH_MARKER_BEGIN} + ⟨`diagnostics, true⟩, + ⟨`diagnostics.threshold, (0 : Nat)⟩, + {PATCH_MARKER_END} +""" + +# Insertion anchor inside `mathlibLeanOptions := #[ ... ]`. We insert *after* +# this line (which has no trailing comment, so preserving trailing text is +# not an issue). +ANCHOR = " ⟨`autoImplicit, false⟩,\n" + + +def patch_lakefile() -> str: + """Insert the diagnostics options into mathlibLeanOptions. Returns the + original contents (for restoration).""" + original = LAKEFILE.read_text() + if PATCH_MARKER_BEGIN in original: + raise RuntimeError( + "lakefile.lean already contains expose_report patch markers; " + "restore it manually before running again." + ) + if ANCHOR not in original: + raise RuntimeError( + f"Could not find insertion anchor in lakefile.lean:\n {ANCHOR!r}" + ) + patched = original.replace(ANCHOR, ANCHOR + PATCH_BLOCK, 1) + LAKEFILE.write_text(patched) + return original + + +def restore_lakefile(original: str) -> None: + LAKEFILE.write_text(original) + + +def run_build(log_path: Path) -> int: + """Stream `lake build Mathlib` to stdout and to `log_path`. Returns exit.""" + log_path.parent.mkdir(parents=True, exist_ok=True) + cmd = ["lake", "build", "Mathlib"] + print(f"[build_with_diagnostics] running: {' '.join(cmd)}", flush=True) + with open(log_path, "w") as log: + proc = subprocess.Popen( + cmd, + cwd=str(REPO_ROOT), + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, + text=True, + bufsize=1, + ) + assert proc.stdout is not None + try: + for line in proc.stdout: + sys.stdout.write(line) + sys.stdout.flush() + log.write(line) + except KeyboardInterrupt: + proc.send_signal(signal.SIGINT) + raise + proc.wait() + return proc.returncode + + +# --- log parsing -------------------------------------------------------- + +# Build-progress line: "✔ [N/M] Built Mathlib.Foo.Bar" or "ℹ [N/M] Built …" +# File attribution is driven entirely off this line: lake prints a file's +# info/trace/warning output immediately after its `Built` header, so the +# current-file cursor is unambiguous within a block. +BUILT_RE = re.compile( + r"^[\u2714\u2139\u26A0\u2716]\s+\[\d+/\d+\]\s+Built\s+(\S+)" +) +# Header: ` [reduction] unfolded declarations (max: N, num: M):` +CATEGORY_HEADER_RE = re.compile( + r"^\s*\[(reduction|kernel)\]\s+(unfolded declarations|" + r"unfolded instances|unfolded reducible declarations)\s*" + r"\(max: \d+, num: \d+\):\s*$" +) +# Entry: ` [reduction] Foo.bar ↦ 3` +ENTRY_RE = re.compile( + r"^\s*\[(reduction|kernel)\]\s+(\S.*?)\s+↦\s+(\d+)\s*$" +) + +CATEGORY_SHORT = { + ("reduction", "unfolded declarations"): "reduction/unfolded", + ("reduction", "unfolded instances"): "reduction/instances", + ("reduction", "unfolded reducible declarations"): "reduction/reducible", + ("kernel", "unfolded declarations"): "kernel/unfolded", +} + + +def target_to_file(target: str) -> str | None: + """Convert `Mathlib.Foo.Bar` → `Mathlib/Foo/Bar.lean`. Non-file targets + (those containing ':') return None.""" + if ":" in target: + return None + return target.replace(".", "/") + ".lean" + + +def parse_log(log_path: Path, out_path: Path) -> dict: + """Parse `log_path` and write per-unfold JSONL records to `out_path`. + Returns a summary dict.""" + out_path.parent.mkdir(parents=True, exist_ok=True) + + current_file: str | None = None + current_category: str | None = None + records_written = 0 + decls_seen: set[str] = set() + files_seen: set[str] = set() + + with open(log_path) as log, open(out_path, "w") as out: + for raw in log: + line = raw.rstrip("\n") + + # 1. Update current-file context from the progress header. + m = BUILT_RE.match(line) + if m: + current_file = target_to_file(m.group(1)) + current_category = None + continue + + # 2. Diagnostic subcategory header. + m = CATEGORY_HEADER_RE.match(line) + if m: + tag, label = m.group(1), m.group(2) + current_category = CATEGORY_SHORT.get((tag, label)) + continue + + # 3. Entry line, only valid inside a known category and with a + # known current file. + m = ENTRY_RE.match(line) + if m and current_category is not None and current_file is not None: + tag, decl, count = m.group(1), m.group(2), int(m.group(3)) + # The entry's tag should match the header's tag; if not, we + # likely left the category silently. Reset and skip. + if not current_category.startswith(tag): + current_category = None + continue + record = { + "file": current_file, + "decl": decl, + "count": count, + "category": current_category, + } + out.write(json.dumps(record, separators=(",", ":")) + "\n") + records_written += 1 + decls_seen.add(decl) + files_seen.add(current_file) + continue + + # 4. Any other non-entry line ends a category block. + if line and not line.startswith(" "): + current_category = None + + return { + "records": records_written, + "unique_decls": len(decls_seen), + "files_with_diagnostics": len(files_seen), + } + + +def main() -> int: + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument("--skip-build", action="store_true", + help="don't run lake build; parse existing log only") + ap.add_argument("--log", type=Path, default=DEFAULT_LOG, + help=f"build log path (default: {DEFAULT_LOG})") + ap.add_argument("--out", type=Path, default=DEFAULT_JSONL, + help=f"output JSONL path (default: {DEFAULT_JSONL})") + args = ap.parse_args() + + OUTPUT_DIR.mkdir(parents=True, exist_ok=True) + + rc = 0 + if not args.skip_build: + original = patch_lakefile() + try: + rc = run_build(args.log) + finally: + restore_lakefile(original) + if rc != 0: + print(f"[build_with_diagnostics] lake build exited {rc}; " + f"log preserved at {args.log}. " + f"Re-run with --skip-build --log to reparse.", + file=sys.stderr) + # Still parse: partial output is useful. + + if not args.log.exists(): + print(f"error: log not found: {args.log}", file=sys.stderr) + return 2 + + summary = parse_log(args.log, args.out) + print(f"[build_with_diagnostics] wrote {summary['records']} records " + f"({summary['unique_decls']} unique decls, " + f"{summary['files_with_diagnostics']} files with diagnostics) " + f"to {args.out}", file=sys.stderr) + return rc + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/expose_enumerate.lean b/scripts/expose_enumerate.lean new file mode 100644 index 00000000000000..1d7885c9d8ef54 --- /dev/null +++ b/scripts/expose_enumerate.lean @@ -0,0 +1,170 @@ +/- +Copyright (c) 2026 Kim Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +import Mathlib.Lean.CoreM + +/-! +# expose_enumerate + +Enumerates all `def` and `instance` declarations in Mathlib whose bodies are +present in the exported view of the environment — i.e., are currently being +exposed to downstream modules, whether via an explicit `@[expose]` attribute +or via an enclosing `@[expose] public section`. + +This produces one half of the input needed by `scripts/expose_report.py`; +the other half comes from a Mathlib build with `diagnostics=true`. + +Output: JSONL on stdout, one record per decl with fields: + * `name` — full constant name (e.g. `"FreeAlgebra.lift"`) + * `kind` — `"def"` or `"instance"` + * `module` — module declaring the decl (e.g. `"Mathlib.Algebra.FreeAlgebra"`) + * `file` — relative path to source (e.g. `"Mathlib/Algebra/FreeAlgebra.lean"`) + * `line`, `col` — 1-based declaration position + * `effect` — `"exposed"` or `"noop-always-exported"` + +`noop-always-exported` marks decls for which `@[expose]` is redundant: their +bodies end up in the exported view regardless (e.g. `abbrev`s). Removing +`@[expose]` from these is trivially safe; they're kept in the report +primarily so users can see them. + +Usage: + lake exe expose_enumerate > exposed.jsonl + +Limitations: + * Does not distinguish "individual `@[expose]` attribute" from "enclosing + `@[expose] public section`" — the attribute is stripped before a decl + enters the environment (see Lean/Elab/MutualDef.lean). The source file + is reported so the user can inspect. + * Non-`Prop`-returning instances are always exported by the module system + regardless of `@[expose]`; this script does not currently flag them as + `noop-always-exported`. Treat a `kind = instance` row as potentially + noop. + * Captures only decls declared in modules whose name starts with + `Mathlib` (excludes `Cache`, `MathlibTest`, third-party deps). +-/ + +open Lean Core + +namespace Mathlib.ExposeReport + +/-- Is the declaration's body present in the *exported* view of the env? -/ +def isBodyExported (env : Environment) (name : Name) : Bool := + (env.setExporting true |>.find? name).any (·.hasValue) + +/-- Return the declaring Mathlib module, if the constant lives in Mathlib.* -/ +def declaringMathlibModule? (env : Environment) (name : Name) : Option Name := do + let idx ← env.getModuleIdxFor? name + let some mod := env.header.moduleNames[idx]? | none + guard (mod.getRoot == `Mathlib) + return mod + +/-- Convert `Mathlib.Foo.Bar` → `"Mathlib/Foo/Bar.lean"`. -/ +def moduleToPath (m : Name) : String := + let parts := m.toString.splitOn "." + "/".intercalate parts ++ ".lean" + +/-- Escape a string for inclusion in a JSON string literal. -/ +def escapeJson (s : String) : String := + s.foldl (init := "") fun acc c => acc ++ + match c with + | '"' => "\\\"" + | '\\' => "\\\\" + | '\n' => "\\n" + | '\r' => "\\r" + | '\t' => "\\t" + | c => c.toString + +structure DeclRecord where + name : Name + kind : String + «module» : Name + file : String + line : Nat + col : Nat + «effect» : String + +def DeclRecord.toJsonLine (d : DeclRecord) : String := + "{\"name\":\"" ++ escapeJson d.name.toString ++ + "\",\"kind\":\"" ++ d.kind ++ + "\",\"module\":\"" ++ escapeJson d.module.toString ++ + "\",\"file\":\"" ++ escapeJson d.file ++ + "\",\"line\":" ++ toString d.line ++ + ",\"col\":" ++ toString d.col ++ + ",\"effect\":\"" ++ d.effect ++ "\"}" + +/-- Name suffixes used for compiler-generated helpers of structures / inductives. -/ +def autoGenSuffixes : Array String := #[ + "recOn", "casesOn", "brecOn", "binductionOn", "below", "ibelow", "ndrec", + "ndrecOn", "recAux", "rec", "noConfusion", "noConfusionType", "sizeOf", + "sizeOf_spec", "injEq" +] + +/-- True if `name` looks like a compiler-generated helper we should exclude. -/ +def isAutoGen (env : Environment) (name : Name) : CoreM Bool := do + if Lean.isAuxRecursor env name then return true + if Lean.isNoConfusion env name then return true + if (env.getProjectionFnInfo? name).isSome then return true + if ← Lean.Meta.isMatcher name then return true + -- name ends in one of the standard auto-generated helper suffixes + if let .str _ last := name then + if autoGenSuffixes.contains last then return true + -- structure field-like: `Parent.toChild` when Parent extends Child + -- (caught by getProjectionFnInfo? in most cases) + return false + +/-- Collect records for every `def` in Mathlib whose body is exported and +whose exposure is not trivially guaranteed by some other mechanism (such as +being an abbrev or a non-Prop instance). + +`instance` decls are excluded: per the module system, a non-`Prop` instance +always has its body in the exported view regardless of `@[expose]`, and a +`Prop` instance's body is a proof (irrelevant to unfolding). Either way, +`@[expose]` on an instance has no semantic effect, so un-exposing one is +trivially safe — these decls aren't useful rows in the report and are +excluded to reduce noise. +-/ +def collect : CoreM (Array DeclRecord) := do + let env ← getEnv + let instSet := (Lean.Meta.instanceExtension.getState env).instanceNames + let mut out : Array DeclRecord := #[] + let mut instSkipped : Nat := 0 + for (name, info) in env.constants.toList do + let .defnInfo defnVal := info | continue + let some mod := declaringMathlibModule? env name | continue + if name.hasMacroScopes then continue + if name.isInternal then continue + if ← isAutoGen env name then continue + unless isBodyExported env name do continue + if instSet.contains name then + instSkipped := instSkipped + 1 + continue + let isAbbrev := defnVal.hints.isAbbrev + let kind := "def" + let «effect» := if isAbbrev then "noop-always-exported" else "exposed" + let some ranges ← Lean.findDeclarationRanges? name | continue + let pos := ranges.range.pos + out := out.push { + name + kind + «module» := mod + file := moduleToPath mod + line := pos.line + col := pos.column + «effect» + } + IO.eprintln s!"[expose_enumerate] excluded {instSkipped} instances (expose is a no-op)" + return out + +end Mathlib.ExposeReport + +open Mathlib.ExposeReport in +unsafe def main (_args : List String) : IO UInt32 := do + let searchPath ← addSearchPathFromEnv (← getBuiltinSearchPath (← findSysroot)) + CoreM.withImportModules #[`Mathlib] (searchPath := searchPath) (trustLevel := 1024) do + let records ← collect + let stdout ← IO.getStdout + for r in records do + stdout.putStrLn r.toJsonLine + return 0 diff --git a/scripts/expose_report.py b/scripts/expose_report.py new file mode 100755 index 00000000000000..d3e33cac59772c --- /dev/null +++ b/scripts/expose_report.py @@ -0,0 +1,159 @@ +#!/usr/bin/env python3 +""" +Part of the `@[expose]` removal-candidate reporting pipeline +(see `scripts/expose_enumerate.lean` and `scripts/build_with_diagnostics.py`). + +Joins the enumeration of exposed decls (from `lake exe expose_enumerate`) +with per-file unfold diagnostics (from `build_with_diagnostics.py`) and +produces: + + scripts/.expose_report/report.jsonl — one record per exposed decl + scripts/.expose_report/report.tsv — sorted TSV, zero-usage rows first + scripts/.expose_report/summary.md — aggregate counts + +Each report record carries: + name, kind, module, file, line, col, effect + downstream_usage — total cross-module unfold count observed + num_using_files — count of distinct files that unfolded the decl + top_using_files — up to 5 (file, count) pairs sorted descending + +"Downstream" means files other than the module that declared the decl. +Same-module unfolds are filtered out (a file can always unfold its own +locally-visible defs, regardless of `@[expose]`). + +Zero-`downstream_usage` rows with `effect = "exposed"` are the primary +actionable output: decls where `@[expose]` can be removed without affecting +any observed downstream unfold. `effect = "noop-always-exported"` zero-usage +rows (abbrevs) are also safe to un-expose, but trivially so. + +Limitations inherited from the signal: + * Unfold-based only; metaprograms inspecting `ConstantInfo.value?` don't + appear. A zero-usage row may still be load-bearing via metaprogramming. + * Lean's threshold is strictly `>`, so single-unfold events still count. + +Usage: + python3 scripts/expose_report.py +""" + +import argparse +import json +import sys +from collections import Counter, defaultdict +from pathlib import Path + + +REPO_ROOT = Path(__file__).resolve().parent.parent +OUTPUT_DIR = REPO_ROOT / "scripts" / ".expose_report" + + +def main() -> int: + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument("--exposed", type=Path, + default=OUTPUT_DIR / "exposed.jsonl", + help="enumeration JSONL from `lake exe expose_enumerate`") + ap.add_argument("--diagnostics", type=Path, + default=OUTPUT_DIR / "diagnostics.jsonl", + help="per-unfold JSONL from build_with_diagnostics.py") + ap.add_argument("--out-jsonl", type=Path, + default=OUTPUT_DIR / "report.jsonl") + ap.add_argument("--out-tsv", type=Path, + default=OUTPUT_DIR / "report.tsv") + ap.add_argument("--out-summary", type=Path, + default=OUTPUT_DIR / "summary.md") + args = ap.parse_args() + + if not args.exposed.exists(): + print(f"error: exposed JSONL missing: {args.exposed}", file=sys.stderr) + return 2 + if not args.diagnostics.exists(): + print(f"error: diagnostics JSONL missing: {args.diagnostics}", file=sys.stderr) + return 2 + + # Load enumeration: name -> record. + exposed: dict[str, dict] = {} + for raw in open(args.exposed): + r = json.loads(raw) + exposed[r["name"]] = r + + # Aggregate diagnostics, filtering to cross-module unfolds. + usage: Counter = Counter() + using_file_counts: dict[str, Counter] = defaultdict(Counter) + for raw in open(args.diagnostics): + d = json.loads(raw) + decl = d["decl"] + rec = exposed.get(decl) + if rec is None: + continue + if d["file"] == rec["file"]: + continue # same-module unfold, not a downstream signal + usage[decl] += d["count"] + using_file_counts[decl][d["file"]] += d["count"] + + # Build and sort report records. + records: list[dict] = [] + for name, rec in exposed.items(): + u = usage.get(name, 0) + top5 = using_file_counts.get(name, Counter()).most_common(5) + records.append({ + **rec, + "downstream_usage": u, + "num_using_files": len(using_file_counts.get(name, {})), + "top_using_files": [ + {"file": f, "count": c} for f, c in top5 + ], + }) + records.sort(key=lambda r: (r["downstream_usage"], r["module"], r["line"])) + + args.out_jsonl.parent.mkdir(parents=True, exist_ok=True) + with open(args.out_jsonl, "w") as f: + for r in records: + f.write(json.dumps(r, separators=(",", ":")) + "\n") + + with open(args.out_tsv, "w") as f: + f.write("name\tkind\teffect\tmodule\tsource\tdownstream_usage" + "\tnum_using_files\ttop_using_files\n") + for r in records: + top = ";".join(f"{x['file']}:{x['count']}" + for x in r["top_using_files"]) + f.write( + f"{r['name']}\t{r['kind']}\t{r['effect']}\t{r['module']}\t" + f"{r['file']}:{r['line']}\t{r['downstream_usage']}\t" + f"{r['num_using_files']}\t{top}\n" + ) + + total = len(records) + zero = sum(1 for r in records if r["downstream_usage"] == 0) + zero_noop = sum(1 for r in records + if r["downstream_usage"] == 0 + and r["effect"] == "noop-always-exported") + zero_exp = zero - zero_noop + low = sum(1 for r in records if 1 <= r["downstream_usage"] <= 5) + high = sum(1 for r in records if r["downstream_usage"] > 5) + + with open(args.out_summary, "w") as f: + f.write( + f"# `@[expose]` removal-candidate report\n\n" + f"- Total decls tracked: **{total}**\n" + f"- Zero downstream usage: **{zero}** (candidates for un-exposing)\n" + f" - `effect = exposed` (meaningful removals): **{zero_exp}**\n" + f" - `effect = noop-always-exported` (trivial no-ops): **{zero_noop}**\n" + f"- Low usage (1–5 unfolds): **{low}**\n" + f"- High usage (>5 unfolds): **{high}**\n\n" + f"Sorted report: `report.tsv`\n" + f"Full records: `report.jsonl`\n" + f"\n" + f"Caveat: the signal is unfold-based. Decls inspected by\n" + f"metaprograms without a WHNF unfold will not appear in any\n" + f"category, so a zero-usage row may still be load-bearing in\n" + f"practice. Verify by temporarily un-exposing a candidate and\n" + f"checking the build.\n" + ) + + print(f"[expose_report] {total} rows, {zero} zero-usage " + f"({zero_exp} meaningful, {zero_noop} noop-always-exported)", + file=sys.stderr) + return 0 + + +if __name__ == "__main__": + sys.exit(main()) From fac6ec2d6d61c1492942cd9d879b4c0629f76a0d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 8 May 2026 13:53:45 +1000 Subject: [PATCH 02/27] chore(scripts): work around #guard_msgs / aesop failures in expose pipeline 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) --- scripts/build_with_diagnostics.py | 75 +++++++++++++++++++++++++++---- scripts/expose_enumerate.lean | 21 ++++++++- 2 files changed, 86 insertions(+), 10 deletions(-) diff --git a/scripts/build_with_diagnostics.py b/scripts/build_with_diagnostics.py index aab632505f37e2..498cac0fe6f48b 100755 --- a/scripts/build_with_diagnostics.py +++ b/scripts/build_with_diagnostics.py @@ -74,22 +74,43 @@ PATCH_MARKER_BEGIN = "-- BEGIN expose_report diagnostics patch" PATCH_MARKER_END = "-- END expose_report diagnostics patch" -# The extra LeanOptions lines inserted into `mathlibLeanOptions`. +# Files that fail to elaborate when `diagnostics=true` is enabled globally. +# We turn diagnostics off in each one for the duration of the build, then +# restore the original source. Four are `#guard_msgs` mismatches caused by +# the extra `[diag]` info messages; the fifth is an `aesop`/`naturality` +# tactic failure that empirically also goes away with diagnostics off. +DIAGNOSTICS_OFF_FILES: list[str] = [ + "Mathlib/Tactic/Linter/ValidatePRTitle.lean", + "Mathlib/Order/Interval/Lex.lean", + "Mathlib/Tactic/NormNum/Ordinal.lean", + "Mathlib/Probability/ConditionalProbability.lean", + "Mathlib/CategoryTheory/Discrete/Basic.lean", +] +FILE_PATCH_LINE = ( + "-- expose_report: locally disable diagnostics so this file builds " + "under global `diagnostics=true`\nset_option diagnostics false\n" +) + +# Diagnostics options are inserted into `mathlibLeanOptions`. This DOES +# affect Lake's olean hash, so the build rebuilds Mathlib from scratch. The +# tradeoff is necessary: `weakLeanArgs` doesn't change the hash, but Lake +# then sees the existing oleans as up-to-date and skips re-elaboration — +# no re-elaboration means no diagnostics output. After this script +# finishes, run `lake exe cache get` to restore cached oleans (their +# unchanged hashes are still on the cache server). PATCH_BLOCK = f""" {PATCH_MARKER_BEGIN} ⟨`diagnostics, true⟩, ⟨`diagnostics.threshold, (0 : Nat)⟩, {PATCH_MARKER_END} """ -# Insertion anchor inside `mathlibLeanOptions := #[ ... ]`. We insert *after* -# this line (which has no trailing comment, so preserving trailing text is -# not an issue). +# Insertion anchor inside `mathlibLeanOptions := #[ ... ]`. ANCHOR = " ⟨`autoImplicit, false⟩,\n" def patch_lakefile() -> str: - """Insert the diagnostics options into mathlibLeanOptions. Returns the - original contents (for restoration).""" + """Insert the diagnostics weakLeanArgs into the mathlib package config. + Returns the original contents for restoration.""" original = LAKEFILE.read_text() if PATCH_MARKER_BEGIN in original: raise RuntimeError( @@ -109,6 +130,42 @@ def restore_lakefile(original: str) -> None: LAKEFILE.write_text(original) +def patch_diagnostics_off_files() -> dict[str, str]: + """Insert `set_option diagnostics false` after the imports of each file + in `DIAGNOSTICS_OFF_FILES`. Returns originals for restoration. + + Insertion point: the line *after* the last `import` / `public import` + line of the file. Works for both module-mode files (which have + `module` followed by imports) and non-module files. The copyright + comment block stays at the top. + """ + originals: dict[str, str] = {} + for rel in DIAGNOSTICS_OFF_FILES: + path = REPO_ROOT / rel + text = path.read_text() + originals[rel] = text + if FILE_PATCH_LINE in text: + continue + lines = text.splitlines(keepends=True) + last_import = -1 + for i, line in enumerate(lines): + stripped = line.lstrip() + if stripped.startswith("import ") or stripped.startswith("public import "): + last_import = i + if last_import < 0: + raise RuntimeError(f"no import line found in {rel}; " + f"don't know where to insert set_option") + insert_at = last_import + 1 + new_lines = lines[:insert_at] + ["\n", FILE_PATCH_LINE] + lines[insert_at:] + path.write_text("".join(new_lines)) + return originals + + +def restore_diagnostics_off_files(originals: dict[str, str]) -> None: + for rel, text in originals.items(): + (REPO_ROOT / rel).write_text(text) + + def run_build(log_path: Path) -> int: """Stream `lake build Mathlib` to stdout and to `log_path`. Returns exit.""" log_path.parent.mkdir(parents=True, exist_ok=True) @@ -248,11 +305,13 @@ def main() -> int: rc = 0 if not args.skip_build: - original = patch_lakefile() + original_lakefile = patch_lakefile() + original_files = patch_diagnostics_off_files() try: rc = run_build(args.log) finally: - restore_lakefile(original) + restore_lakefile(original_lakefile) + restore_diagnostics_off_files(original_files) if rc != 0: print(f"[build_with_diagnostics] lake build exited {rc}; " f"log preserved at {args.log}. " diff --git a/scripts/expose_enumerate.lean b/scripts/expose_enumerate.lean index 1d7885c9d8ef54..b5706a47988625 100644 --- a/scripts/expose_enumerate.lean +++ b/scripts/expose_enumerate.lean @@ -159,10 +159,27 @@ def collect : CoreM (Array DeclRecord) := do end Mathlib.ExposeReport +/-- Read module names to import from a file, one per line, blank lines and +`#`-comments ignored. -/ +def readModulesFile (path : System.FilePath) : IO (Array Name) := do + let text ← IO.FS.readFile path + let mut out : Array Name := #[] + for line in text.splitOn "\n" do + let line := line.trim + if line.isEmpty || line.startsWith "#" then continue + out := out.push line.toName + return out + open Mathlib.ExposeReport in -unsafe def main (_args : List String) : IO UInt32 := do +unsafe def main (args : List String) : IO UInt32 := do let searchPath ← addSearchPathFromEnv (← getBuiltinSearchPath (← findSysroot)) - CoreM.withImportModules #[`Mathlib] (searchPath := searchPath) (trustLevel := 1024) do + -- If a file path is given as the first argument, import the modules listed + -- there (one per line). Otherwise, default to the single `Mathlib` module. + let modules ← match args with + | path :: _ => readModulesFile path + | _ => pure #[`Mathlib] + IO.eprintln s!"[expose_enumerate] importing {modules.size} module(s)..." + CoreM.withImportModules modules (searchPath := searchPath) (trustLevel := 1024) do let records ← collect let stdout ← IO.getStdout for r in records do From 00831834d801efe3b28997f4bf374d50d979bae2 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 9 May 2026 10:10:33 +1000 Subject: [PATCH 03/27] chore(scripts): widen expose-pipeline parser to include `[type_class] used instances` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- scripts/build_with_diagnostics.py | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/scripts/build_with_diagnostics.py b/scripts/build_with_diagnostics.py index 498cac0fe6f48b..fabd955355fe19 100755 --- a/scripts/build_with_diagnostics.py +++ b/scripts/build_with_diagnostics.py @@ -204,20 +204,25 @@ def run_build(log_path: Path) -> int: ) # Header: ` [reduction] unfolded declarations (max: N, num: M):` CATEGORY_HEADER_RE = re.compile( - r"^\s*\[(reduction|kernel)\]\s+(unfolded declarations|" - r"unfolded instances|unfolded reducible declarations)\s*" + r"^\s*\[(reduction|kernel|type_class)\]\s+(unfolded declarations|" + r"unfolded instances|unfolded reducible declarations|used instances)\s*" r"\(max: \d+, num: \d+\):\s*$" ) # Entry: ` [reduction] Foo.bar ↦ 3` ENTRY_RE = re.compile( - r"^\s*\[(reduction|kernel)\]\s+(\S.*?)\s+↦\s+(\d+)\s*$" + r"^\s*\[(reduction|kernel|type_class)\]\s+(\S.*?)\s+↦\s+(\d+)\s*$" ) +# `type_class / used instances` is needed because instance synthesis can +# rely on a downstream-exposed body without ever recording an explicit +# `recordUnfold` event (e.g. typeclass projection through a parent class). +# Empirically, the report misses such uses if this category is omitted. CATEGORY_SHORT = { ("reduction", "unfolded declarations"): "reduction/unfolded", ("reduction", "unfolded instances"): "reduction/instances", ("reduction", "unfolded reducible declarations"): "reduction/reducible", ("kernel", "unfolded declarations"): "kernel/unfolded", + ("type_class", "used instances"): "type_class/used", } From f4765354955a2a73d8ee060ad2f1c277f529ed28 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 9 May 2026 14:37:03 +1000 Subject: [PATCH 04/27] feat(scripts): add static-reference signal for @[expose] removal pipeline MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- lakefile.lean | 9 ++ scripts/expose_report.py | 90 +++++++++++++++++--- scripts/expose_static_refs.lean | 144 ++++++++++++++++++++++++++++++++ 3 files changed, 232 insertions(+), 11 deletions(-) create mode 100644 scripts/expose_static_refs.lean diff --git a/lakefile.lean b/lakefile.lean index 2868b5482fe9e1..5e1aa2f4f61f92 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -135,6 +135,15 @@ lean_exe expose_enumerate where srcDir := "scripts" supportInterpreter := true +/-- `lake exe expose_static_refs` walks the built Mathlib environment and +emits a JSONL of (referencing-module, referenced-decl) pairs based on +`ConstantInfo.getUsedConstantsAsSet`. Complementary to `diagnostics.jsonl` +from `scripts/build_with_diagnostics.py`: catches typeclass-projection +sources that the diagnostic-based signal misses. -/ +lean_exe expose_static_refs where + srcDir := "scripts" + supportInterpreter := true + lean_exe mathlib_test_executable where root := `MathlibTest.MathlibTestExecutable diff --git a/scripts/expose_report.py b/scripts/expose_report.py index d3e33cac59772c..2f4f59de235684 100755 --- a/scripts/expose_report.py +++ b/scripts/expose_report.py @@ -54,6 +54,24 @@ def main() -> int: ap.add_argument("--diagnostics", type=Path, default=OUTPUT_DIR / "diagnostics.jsonl", help="per-unfold JSONL from build_with_diagnostics.py") + ap.add_argument("--static-refs", type=Path, + default=OUTPUT_DIR / "static_refs.jsonl", + help="static-reference JSONL from `lake exe expose_static_refs`. " + "Optional but recommended: catches typeclass-projection " + "sources that diagnostics misses. Use --no-static-refs " + "to disable.") + ap.add_argument("--no-static-refs", action="store_true", + help="ignore static_refs.jsonl even if present") + ap.add_argument("--decl-refs", type=Path, + default=OUTPUT_DIR / "decl_refs.jsonl", + help="per-decl reference list from " + "`lake exe expose_static_refs decl`. Used for " + "one-hop transitive-closure: a downstream use of " + "decl `K` propagates to mark every decl in `K`'s " + "body as also used (catches typeclass-projection " + "chains like `instLattice → instSemilatticeSup`).") + ap.add_argument("--no-transitive", action="store_true", + help="don't apply one-hop transitive closure on static refs") ap.add_argument("--out-jsonl", type=Path, default=OUTPUT_DIR / "report.jsonl") ap.add_argument("--out-tsv", type=Path, @@ -75,19 +93,69 @@ def main() -> int: r = json.loads(raw) exposed[r["name"]] = r - # Aggregate diagnostics, filtering to cross-module unfolds. + # Aggregate cross-module uses from both signals: + # diagnostics.jsonl - unfold-based use captured by `set_option diagnostics true` + # static_refs.jsonl - literal `Expr.const` references in elaborated bodies + # Both sources have the same record shape; we sum counts. usage: Counter = Counter() using_file_counts: dict[str, Counter] = defaultdict(Counter) - for raw in open(args.diagnostics): - d = json.loads(raw) - decl = d["decl"] - rec = exposed.get(decl) - if rec is None: - continue - if d["file"] == rec["file"]: - continue # same-module unfold, not a downstream signal - usage[decl] += d["count"] - using_file_counts[decl][d["file"]] += d["count"] + + def absorb(path: Path) -> int: + n = 0 + for raw in open(path): + d = json.loads(raw) + decl = d["decl"] + rec = exposed.get(decl) + if rec is None: + continue + if d["file"] == rec["file"]: + continue # same-module use, not a downstream signal + usage[decl] += d["count"] + using_file_counts[decl][d["file"]] += d["count"] + n += 1 + return n + + diag_n = absorb(args.diagnostics) + print(f"[expose_report] absorbed {diag_n} diagnostics records", + file=sys.stderr) + if not args.no_static_refs and args.static_refs.exists(): + sref_n = absorb(args.static_refs) + print(f"[expose_report] absorbed {sref_n} static-reference records", + file=sys.stderr) + elif args.no_static_refs: + print(f"[expose_report] static refs disabled by --no-static-refs", + file=sys.stderr) + else: + print(f"[expose_report] static_refs.jsonl not found; using diagnostics only", + file=sys.stderr) + + # One-hop transitive closure: if downstream module M uses decl K, also + # mark every decl K's body references as used by M. Captures cases like + # `M` uses `instLattice`, whose body anonymous-constructs from + # `instSemilatticeSup`/`instSemilatticeInf`, which then need to be exposed + # for downstream projection to find their fields. + if not args.no_transitive and args.decl_refs.exists(): + decl_refs: dict[str, list[str]] = {} + for raw in open(args.decl_refs): + d = json.loads(raw) + decl_refs[d["decl"]] = d["refs"] + # For each used (decl, file) pair, propagate to (ref, file) for ref ∈ decl_refs[decl]. + propagated = 0 + # snapshot the current using_file_counts so iteration is stable + snapshot = [(decl, dict(files)) for decl, files in using_file_counts.items()] + for decl, files in snapshot: + for ref in decl_refs.get(decl, []): + rec = exposed.get(ref) + if rec is None: + continue + for file, count in files.items(): + if file == rec["file"]: + continue # same-module + usage[ref] += count + using_file_counts[ref][file] += count + propagated += 1 + print(f"[expose_report] one-hop transitive: propagated {propagated} extra (ref,file) edges", + file=sys.stderr) # Build and sort report records. records: list[dict] = [] diff --git a/scripts/expose_static_refs.lean b/scripts/expose_static_refs.lean new file mode 100644 index 00000000000000..1db70d13963565 --- /dev/null +++ b/scripts/expose_static_refs.lean @@ -0,0 +1,144 @@ +/- +Copyright (c) 2026 Kim Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +import Mathlib.Lean.CoreM + +/-! +# expose_static_refs + +Static reference analyzer for the `@[expose]` removal pipeline. + +Walks the built Mathlib environment and, for every constant `C`, computes +the set of constants referenced in its type or value (via +`ConstantInfo.getUsedConstantsAsSet`). Aggregates by `(referenced_decl, +referencing_file)` and emits one JSONL record per pair. + +Together with the build-time `diagnostics.jsonl` produced by +`scripts/build_with_diagnostics.py`, this provides a complementary +signal: diagnostics catches *unfold-based* uses (WHNF, kernel reduction, +type-class resolution); static refs catches *literal-occurrence* uses +(any place a referenced const appears in an elaborated body), including +typeclass-projection sources that diagnostics misses. + +Output JSONL shape matches `diagnostics.jsonl` so `expose_report.py` can +merge the two: + + {"file": "Mathlib/Foo/Bar.lean", "decl": "Other.Module.name", + "count": 1, "category": "static/ref"} + +`count` is the number of constants in `file` whose body or type +literally references `decl` at least once (`getUsedConstantsAsSet` +deduplicates per-constant, so `count` is "how many decls in this file +mention `decl`"). + +Limitations: + * Only sees bodies that are actually stored in the environment. A + non-`@[expose]` def's body is replaced by an axiom in the exported + view; references inside it are invisible. Theorem proofs are + similarly unobservable in module mode. + * The reference set of a non-Mathlib constant is not emitted, but + references *to* Mathlib constants from anywhere in the loaded env + are included. + +Usage: + lake exe expose_static_refs > scripts/.expose_report/static_refs.jsonl +-/ + +open Lean Core + +namespace Mathlib.ExposeReport + +/-- Convert `Mathlib.Foo.Bar` → `"Mathlib/Foo/Bar.lean"`. -/ +def moduleToFilePath (m : Name) : String := + let parts := m.toString.splitOn "." + "/".intercalate parts ++ ".lean" + +/-- Escape a string for inclusion in a JSON string literal. -/ +def jsonEscape (s : String) : String := + s.foldl (init := "") fun acc c => acc ++ + match c with + | '"' => "\\\"" + | '\\' => "\\\\" + | '\n' => "\\n" + | '\r' => "\\r" + | '\t' => "\\t" + | c => c.toString + +/-- For each pair (referencing module, referenced const name), the count of +constants in that module whose stored body or type mentions the referenced +name. -/ +abbrev RefMap := Std.HashMap (Nat × Name) Nat + +/-- Walk every constant in the env, accumulating reference pairs. -/ +def collectRefs : CoreM RefMap := do + let env ← getEnv + let mut acc : RefMap := {} + let mut considered : Nat := 0 + for (name, info) in env.constants.toList do + -- Determine the module the referencing constant lives in. + let some refModIdx := env.getModuleIdxFor? name | continue + -- Skip compiler-generated helpers (they reflect implementation + -- details rather than user-written use). + if name.hasMacroScopes then continue + if name.isInternal then continue + considered := considered + 1 + let refs := info.getUsedConstantsAsSet + acc := refs.foldl (init := acc) fun acc referenced => + let key := (refModIdx, referenced) + acc.insert key ((acc.getD key 0) + 1) + IO.eprintln (s!"[expose_static_refs] scanned {considered} constants, " ++ + s!"recorded {acc.size} (module,decl) reference pairs") + return acc + +/-- For every constant whose stored body is non-empty, emit a +`decl_refs` JSONL line listing the constants its body/type literally +references. Used by `expose_report.py` to walk one-hop transitivity: +if a downstream module uses decl `K`, it indirectly uses every decl +referenced by `K`'s body too (relevant for typeclass-projection chains +like `instLattice → instSemilatticeSup`). -/ +def emitDeclRefs (out : IO.FS.Stream) : CoreM Unit := do + let env ← getEnv + for (name, info) in env.constants.toList do + if name.hasMacroScopes then continue + if name.isInternal then continue + -- only emit for decls declared somewhere we care about (any module); + -- the consumer filters to Mathlib decls via the enumeration anyway. + if (env.getModuleIdxFor? name).isNone then continue + let refs := info.getUsedConstantsAsSet + if refs.isEmpty then continue + let arr := refs.foldl (init := #[]) fun a n => a.push n + let body : String := ",".intercalate <| + arr.toList.map fun n => "\"" ++ jsonEscape n.toString ++ "\"" + out.putStrLn <| + "{\"decl\":\"" ++ jsonEscape name.toString ++ + "\",\"refs\":[" ++ body ++ "]}" + +unsafe def mainUnsafe (args : List String) : IO UInt32 := do + let searchPath ← addSearchPathFromEnv (← getBuiltinSearchPath (← findSysroot)) + -- args[0] = output mode: "module" (default) or "decl". + let mode := args.head?.getD "module" + CoreM.withImportModules #[`Mathlib] (searchPath := searchPath) (trustLevel := 1024) do + let stdout ← IO.getStdout + match mode with + | "decl" => + emitDeclRefs stdout + | _ => + -- module mode: aggregate by (refModule, refName) + let acc ← collectRefs + let env ← getEnv + for ((modIdx, decl), count) in acc.toList do + let some mod := env.header.moduleNames[modIdx]? | continue + let file := moduleToFilePath mod + stdout.putStrLn <| + "{\"file\":\"" ++ jsonEscape file ++ + "\",\"decl\":\"" ++ jsonEscape decl.toString ++ + "\",\"count\":" ++ toString count ++ + ",\"category\":\"static/ref\"}" + return 0 + +end Mathlib.ExposeReport + +open Mathlib.ExposeReport in +unsafe def main (args : List String) : IO UInt32 := mainUnsafe args From e8a49f7f6b706c1dccf3da18e95c20609f7d6c5e Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 9 May 2026 22:06:05 +1000 Subject: [PATCH 05/27] feat(scripts): track theorem-kind referencers + same-module rfl signal MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- scripts/expose_report.py | 27 ++++++++++++++++++++++----- scripts/expose_static_refs.lean | 24 +++++++++++++++--------- 2 files changed, 37 insertions(+), 14 deletions(-) diff --git a/scripts/expose_report.py b/scripts/expose_report.py index 2f4f59de235684..7d8ab7ce840d25 100755 --- a/scripts/expose_report.py +++ b/scripts/expose_report.py @@ -72,6 +72,12 @@ def main() -> int: "chains like `instLattice → instSemilatticeSup`).") ap.add_argument("--no-transitive", action="store_true", help="don't apply one-hop transitive closure on static refs") + ap.add_argument("--include-same-module", action="store_true", + help="count same-module references too. Same-module " + "uses (e.g. a theorem in file F whose `rfl` needs the " + "body of an instance in F) actually require the " + "instance to be `@[expose]`d; filtering them out " + "produces false-positive 'safe' verdicts.") ap.add_argument("--out-jsonl", type=Path, default=OUTPUT_DIR / "report.jsonl") ap.add_argument("--out-tsv", type=Path, @@ -108,10 +114,21 @@ def absorb(path: Path) -> int: rec = exposed.get(decl) if rec is None: continue - if d["file"] == rec["file"]: - continue # same-module use, not a downstream signal - usage[decl] += d["count"] - using_file_counts[decl][d["file"]] += d["count"] + same_module = (d["file"] == rec["file"]) + if same_module and not args.include_same_module: + # Default: skip cross-decl-but-same-module use, EXCEPT same-module + # references coming from theorems (whose `:= rfl` proofs need + # the body to defeq). `theorem_count` is set on static_refs.jsonl + # records by `expose_static_refs.lean`; absent for diagnostics + # (those are runtime unfolds, all from non-theorem code paths). + tc = d.get("theorem_count", 0) + if tc <= 0: + continue + count = tc + else: + count = d["count"] + usage[decl] += count + using_file_counts[decl][d["file"]] += count n += 1 return n @@ -149,7 +166,7 @@ def absorb(path: Path) -> int: if rec is None: continue for file, count in files.items(): - if file == rec["file"]: + if file == rec["file"] and not args.include_same_module: continue # same-module usage[ref] += count using_file_counts[ref][file] += count diff --git a/scripts/expose_static_refs.lean b/scripts/expose_static_refs.lean index 1db70d13963565..de616f54823e94 100644 --- a/scripts/expose_static_refs.lean +++ b/scripts/expose_static_refs.lean @@ -66,10 +66,16 @@ def jsonEscape (s : String) : String := | '\t' => "\\t" | c => c.toString -/-- For each pair (referencing module, referenced const name), the count of -constants in that module whose stored body or type mentions the referenced -name. -/ -abbrev RefMap := Std.HashMap (Nat × Name) Nat +/-- For each pair (referencing module, referenced const name): a tuple of +`(total_count, theorem_count)`. `total_count` is how many constants in +that module reference the decl; `theorem_count` is the subset of those +that are `theorem`s (proof-irrelevant). The split matters for +same-module use: a `theorem ... := rfl` that mentions the decl needs +its body for defeq to succeed, so even *intra-file* theorem references +are load-bearing. Other intra-file references (e.g. an `instance`'s +anonymous-constructor field `__ := X`) typically don't require the +body to be exposed. -/ +abbrev RefMap := Std.HashMap (Nat × Name) (Nat × Nat) /-- Walk every constant in the env, accumulating reference pairs. -/ def collectRefs : CoreM RefMap := do @@ -77,17 +83,16 @@ def collectRefs : CoreM RefMap := do let mut acc : RefMap := {} let mut considered : Nat := 0 for (name, info) in env.constants.toList do - -- Determine the module the referencing constant lives in. let some refModIdx := env.getModuleIdxFor? name | continue - -- Skip compiler-generated helpers (they reflect implementation - -- details rather than user-written use). if name.hasMacroScopes then continue if name.isInternal then continue considered := considered + 1 + let isThm := info matches .thmInfo _ let refs := info.getUsedConstantsAsSet acc := refs.foldl (init := acc) fun acc referenced => let key := (refModIdx, referenced) - acc.insert key ((acc.getD key 0) + 1) + let (cTot, cThm) := acc.getD key (0, 0) + acc.insert key (cTot + 1, if isThm then cThm + 1 else cThm) IO.eprintln (s!"[expose_static_refs] scanned {considered} constants, " ++ s!"recorded {acc.size} (module,decl) reference pairs") return acc @@ -128,13 +133,14 @@ unsafe def mainUnsafe (args : List String) : IO UInt32 := do -- module mode: aggregate by (refModule, refName) let acc ← collectRefs let env ← getEnv - for ((modIdx, decl), count) in acc.toList do + for ((modIdx, decl), (count, thmCount)) in acc.toList do let some mod := env.header.moduleNames[modIdx]? | continue let file := moduleToFilePath mod stdout.putStrLn <| "{\"file\":\"" ++ jsonEscape file ++ "\",\"decl\":\"" ++ jsonEscape decl.toString ++ "\",\"count\":" ++ toString count ++ + ",\"theorem_count\":" ++ toString thmCount ++ ",\"category\":\"static/ref\"}" return 0 From 87c34be9d96402ef819f2605f9bfed6e56a83a11 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 10 May 2026 13:38:30 +1000 Subject: [PATCH 06/27] feat(scripts): scaffold lake exe no_expose with working report subcommand MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- lakefile.lean | 19 ++++ scripts/NoExpose/Cli.lean | 151 +++++++++++++++++++++++++ scripts/NoExpose/Paths.lean | 88 +++++++++++++++ scripts/NoExpose/Report.lean | 213 +++++++++++++++++++++++++++++++++++ scripts/no_expose.lean | 41 +++++++ 5 files changed, 512 insertions(+) create mode 100644 scripts/NoExpose/Cli.lean create mode 100644 scripts/NoExpose/Paths.lean create mode 100644 scripts/NoExpose/Report.lean create mode 100644 scripts/no_expose.lean diff --git a/lakefile.lean b/lakefile.lean index 5e1aa2f4f61f92..f2f64c07bc61a5 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -144,6 +144,25 @@ lean_exe expose_static_refs where srcDir := "scripts" supportInterpreter := true +/-- Implementation modules for the `no_expose` exe (see below). Kept as a +lib so multiple files under `scripts/NoExpose/` can `import` each other. +The lib deliberately does NOT pull in Mathlib. -/ +lean_lib NoExpose where + srcDir := "scripts" + globs := #[`NoExpose.+] + +/-- `lake exe no_expose` is the user-facing tool for analysing and +removing unnecessary `@[expose]` attributes in Mathlib (and downstream +Mathlib-using projects). Subcommands: + * `collect` — build with diagnostics, scan env, produce report data + * `report` — render per-file recommendations (no build) + * `edit` — apply removals (with safety checks + audit trail) +The exe deliberately does NOT `import Mathlib` so that it builds in +seconds; it loads Mathlib at runtime via `Lean.withImportModules`. -/ +lean_exe no_expose where + srcDir := "scripts" + supportInterpreter := true + lean_exe mathlib_test_executable where root := `MathlibTest.MathlibTestExecutable diff --git a/scripts/NoExpose/Cli.lean b/scripts/NoExpose/Cli.lean new file mode 100644 index 00000000000000..09af9c7bd3e3e1 --- /dev/null +++ b/scripts/NoExpose/Cli.lean @@ -0,0 +1,151 @@ +/- +Copyright (c) 2026 Kim Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ + +/-! +# `NoExpose.Cli` — argument parsing for `lake exe no_expose` + +Hand-rolled argparse (no external deps). Three subcommands: `collect`, +`report`, `edit`, plus `clean` for removing the data directory. + +The flag set is small and the dispatch is shallow, so a hand-rolled +parser keeps the dependency surface minimal. +-/ + +namespace NoExpose + +/-- Format option for `report` output. -/ +inductive ReportFormat where + | text + | json + | tsv + deriving Repr, BEq + +/-- Strategy for `edit`. `auto` picks `section` if the file has +`@[expose] public section`, else `individual`. -/ +inductive EditStrategy where + | auto + | section_ + | individual + deriving Repr, BEq + +structure CollectArgs where + skipBuild : Bool := false + /-- Extra files to insert `set_option diagnostics false` into. -/ + patchFiles : Array String := #[] + +structure ReportArgs where + paths : Array String := #[] + all : Bool := false + format : ReportFormat := .text + collectOnDemand : Bool := false + +structure EditArgs where + paths : Array String := #[] + dryRun : Bool := false + verify : Bool := false + strategy : EditStrategy := .auto + forceDirty : Bool := false + forceStale : Bool := false + +inductive Subcommand where + | help + | collect (args : CollectArgs) + | report (args : ReportArgs) + | edit (args : EditArgs) + | clean + +/-- Top-level help text. -/ +def helpText : String := "\ +USAGE: + lake exe no_expose [args...] + +SUBCOMMANDS: + collect [--skip-build] [--patch-file FILE]... + Build Mathlib with `set_option diagnostics true`, walk the env, + and write report data to scripts/.no_expose/. + + report [PATH...] [--all] [--format text|json|tsv] [--collect-on-demand] + Render per-file recommendations from existing report data. + Defaults to `--format text` and to listing `safe-to-unexpose` + and `load-bearing` decls in each PATH. + + edit [PATH...] [--dry-run] [--verify] [--strategy auto|section|individual] + [--force-dirty] [--force-stale] + Apply (default) or preview (--dry-run) the un-expose edits to + each PATH. Refuses on dirty git tree or stale report unless the + corresponding --force-* flag is given. With --verify, runs + `lake build` on the touched lib after applying. + + clean + Remove scripts/.no_expose/ entirely. + + help, --help, -h + Show this message. +" + +private def parseFormat : String → Except String ReportFormat + | "text" => .ok .text + | "json" => .ok .json + | "tsv" => .ok .tsv + | s => .error s!"unknown --format value: {s} (expected text|json|tsv)" + +private def parseStrategy : String → Except String EditStrategy + | "auto" => .ok .auto + | "section" => .ok .section_ + | "individual" => .ok .individual + | s => .error s!"unknown --strategy value: {s} (expected auto|section|individual)" + +/-- Parse a `collect` argument list. -/ +private partial def parseCollect (rest : List String) : Except String CollectArgs := loop rest {} where + loop : List String → CollectArgs → Except String CollectArgs + | [], acc => .ok acc + | "--skip-build" :: rest, acc => loop rest { acc with skipBuild := true } + | "--patch-file" :: f :: rest, acc => + loop rest { acc with patchFiles := acc.patchFiles.push f } + | flag :: _, _ => .error s!"collect: unknown argument {flag}" + +/-- Parse a `report` argument list. -/ +private partial def parseReport (rest : List String) : Except String ReportArgs := loop rest {} where + loop : List String → ReportArgs → Except String ReportArgs + | [], acc => .ok acc + | "--all" :: rest, acc => loop rest { acc with all := true } + | "--collect-on-demand" :: rest, acc => loop rest { acc with collectOnDemand := true } + | "--format" :: v :: rest, acc => do + let f ← parseFormat v + loop rest { acc with format := f } + | arg :: rest, acc => + if arg.startsWith "--" then .error s!"report: unknown flag {arg}" + else loop rest { acc with paths := acc.paths.push arg } + +/-- Parse an `edit` argument list. -/ +private partial def parseEdit (rest : List String) : Except String EditArgs := loop rest {} where + loop : List String → EditArgs → Except String EditArgs + | [], acc => .ok acc + | "--dry-run" :: rest, acc => loop rest { acc with dryRun := true } + | "--verify" :: rest, acc => loop rest { acc with verify := true } + | "--force-dirty" :: rest, acc => loop rest { acc with forceDirty := true } + | "--force-stale" :: rest, acc => loop rest { acc with forceStale := true } + | "--strategy" :: v :: rest, acc => do + let s ← parseStrategy v + loop rest { acc with strategy := s } + | arg :: rest, acc => + if arg.startsWith "--" then .error s!"edit: unknown flag {arg}" + else loop rest { acc with paths := acc.paths.push arg } + +/-- Top-level dispatch. -/ +def parseArgs : List String → Except String Subcommand + | [] => .ok .help + | "help" :: _ => .ok .help + | "--help" :: _ => .ok .help + | "-h" :: _ => .ok .help + | "collect" :: rest => .collect <$> parseCollect rest + | "report" :: rest => .report <$> parseReport rest + | "edit" :: rest => .edit <$> parseEdit rest + | "clean" :: [] => .ok .clean + | "clean" :: rest => .error s!"clean: unexpected arguments: {String.intercalate " " rest}" + | sub :: _ => .error s!"unknown subcommand: {sub} (try `--help`)" + +end NoExpose diff --git a/scripts/NoExpose/Paths.lean b/scripts/NoExpose/Paths.lean new file mode 100644 index 00000000000000..34e79be2e64791 --- /dev/null +++ b/scripts/NoExpose/Paths.lean @@ -0,0 +1,88 @@ +/- +Copyright (c) 2026 Kim Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +import Lake.CLI.Main + +/-! +# `NoExpose.Paths` — data-artifact paths and project autodetect + +Centralises every filesystem path the tool reads or writes, and the +small piece of Lake-introspection that lets `no_expose` adapt to the +current package (Mathlib, or a downstream Mathlib-using project). +-/ + +open Lake System + +namespace NoExpose + +/-- Root of the data directory the tool owns. Sibling of `lakefile.lean`. -/ +def dataDir : FilePath := "scripts" / ".no_expose" + +/-- Full Mathlib build log (raw `lake build` output). Several GB on a full +collection; kept by default for debuggability. -/ +def buildLogPath : FilePath := dataDir / "build.log" + +/-- Per-file diagnostic-message records parsed from the build log. -/ +def diagnosticsPath : FilePath := dataDir / "diagnostics.jsonl" + +/-- One record per `@[expose]` def/instance the env walk found. -/ +def exposedPath : FilePath := dataDir / "exposed.jsonl" + +/-- Per-(refModule, refName) static reference counts (with theorem split). -/ +def staticRefsPath : FilePath := dataDir / "static_refs.jsonl" + +/-- Per-decl direct reference lists (used for one-hop transitive closure). -/ +def declRefsPath : FilePath := dataDir / "decl_refs.jsonl" + +/-- Joined report — the primary input to `report` and `edit`. -/ +def reportPath : FilePath := dataDir / "report.jsonl" + +/-- Audit trail for `edit` runs: unified diff of every change. -/ +def editsPatchPath : FilePath := dataDir / "edits.patch" + +/-- Where `Restore` writes original copies before patching the lakefile or +fragile source files. Detected on every startup so an interrupted run +can be recovered. -/ +def restoreDir : FilePath := dataDir / "restore" + +/-- Marker file: present iff a `collect` run is mid-flight (used by +`Restore` to recognise crash recovery). -/ +def restoreStatePath : FilePath := restoreDir / "state.json" + +/-- Information about the current Lake package needed by the tool. -/ +structure ProjectInfo where + /-- The package name, e.g. `mathlib`. -/ + name : Lean.Name + /-- The module names of the package's `lean_lib` targets that the tool + should treat as "owned by this project". For Mathlib this is + `[Mathlib, Archive, Counterexamples]` (we further filter to `Mathlib` + for normal use). For a downstream `MyProj`: `[MyProj]`. -/ + libRoots : Array Lean.Name + /-- Source root directories the libs cover, used to map decl-source-files + back to "this project's files" vs imported deps. -/ + srcDirs : Array System.FilePath + /-- The lakefile's path. May be `lakefile.lean` or `lakefile.toml`. -/ + lakefilePath : System.FilePath + +/-- Inspect the current Lake workspace and produce a `ProjectInfo`. Mirrors +`scripts/mk_all.lean:26` and `scripts/lint-style.lean:34`. -/ +def detectProjectInfo : IO ProjectInfo := do + let (elanInstall?, leanInstall?, lakeInstall?) ← Lake.findInstall? + let config ← Lake.MonadError.runEIO <| Lake.mkLoadConfig + { elanInstall?, leanInstall?, lakeInstall? } + let some ws ← (Lake.loadWorkspace config).toBaseIO + | throw <| IO.userError "NoExpose: failed to load Lake workspace" + let pkg := ws.root + let libs := pkg.leanLibs.map fun lib => lib.config.name + let srcDirs := pkg.leanLibs.map fun lib => pkg.dir / lib.config.srcDir + let lakefilePath := pkg.dir / "lakefile.lean" + return { + name := pkg.baseName + libRoots := libs + srcDirs := srcDirs + lakefilePath + } + +end NoExpose diff --git a/scripts/NoExpose/Report.lean b/scripts/NoExpose/Report.lean new file mode 100644 index 00000000000000..c697985e3f172b --- /dev/null +++ b/scripts/NoExpose/Report.lean @@ -0,0 +1,213 @@ +/- +Copyright (c) 2026 Kim Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +import Lean.Data.Json +import NoExpose.Cli +import NoExpose.Paths + +/-! +# `NoExpose.Report` — read and render the joined report + +A `report.jsonl` record (built by `collect`) carries everything `report` +and `edit` need: + +``` +{"name": "Foo.bar", "kind": "def", "effect": "exposed", + "module": "Mathlib.Foo", "file": "Mathlib/Foo.lean", + "line": 42, "col": 0, + "downstream_usage": 17, "num_using_files": 5, + "top_using_files": [{"file": "...", "count": 4}, ...]} +``` + +This module parses those records and renders per-file output in three +formats. Building `report.jsonl` from raw signals is the responsibility +of `NoExpose.Diagnostics` and the `collect` orchestrator. +-/ + +open Lean (Json) + +namespace NoExpose + +/-- A single decl's report row. -/ +structure ReportRecord where + name : String + kind : String + effect : String + module : String + file : String + line : Nat + col : Nat + downstreamUsage : Nat + numUsingFiles : Nat + topUsingFiles : Array (String × Nat) + deriving Inhabited + +/-- The ordered groups we render. -/ +inductive Verdict where + | safeToUnexpose + | loadBearing + | noopAlwaysExported + deriving BEq + +def Verdict.classify (r : ReportRecord) : Verdict := + if r.effect == "noop-always-exported" then .noopAlwaysExported + else if r.downstreamUsage == 0 then .safeToUnexpose + else .loadBearing + +private def jsonGetStr (j : Json) (field : String) : Except String String := + (j.getObjVal? field).bind (·.getStr?) + +private def jsonGetNat (j : Json) (field : String) : Except String Nat := do + let v ← j.getObjVal? field + match v with + | .num n => + -- JSON numbers can be integer-valued; reject negatives. + if n.mantissa ≥ 0 then + pure (n.mantissa.toNat * 10 ^ n.exponent) + else + .error s!"non-integer or negative count in field {field}: {n}" + | _ => .error s!"expected number for field {field}, got {v.compress}" + +private def parseTopUsing (j : Json) : Except String (Array (String × Nat)) := do + let arr ← j.getArr? + arr.mapM fun entry => do + let file ← jsonGetStr entry "file" + let count ← jsonGetNat entry "count" + pure (file, count) + +/-- Parse a single line of `report.jsonl`. -/ +def parseRecord (line : String) : Except String ReportRecord := do + let j ← Json.parse line + let topJ := j.getObjVal? "top_using_files" |>.toOption |>.getD (.arr #[]) + return { + name := ← jsonGetStr j "name" + kind := ← jsonGetStr j "kind" + effect := ← jsonGetStr j "effect" + module := ← jsonGetStr j "module" + file := ← jsonGetStr j "file" + line := ← jsonGetNat j "line" + col := ← jsonGetNat j "col" + downstreamUsage := ← jsonGetNat j "downstream_usage" + numUsingFiles := ← jsonGetNat j "num_using_files" + topUsingFiles := ← parseTopUsing topJ + } + +/-- Read all records from `report.jsonl`, accumulating any parse errors +into a separate channel rather than aborting on the first one. -/ +def readReport (path : System.FilePath) : + IO (Array ReportRecord × Array String) := do + let mut ok : Array ReportRecord := #[] + let mut errs : Array String := #[] + let lines := (← IO.FS.readFile path).splitOn "\n" + for (line, i) in lines.zip (List.range lines.length) do + if line.trimAscii.isEmpty then continue + match parseRecord line with + | .ok r => ok := ok.push r + | .error msg => errs := errs.push s!"line {i+1}: {msg}" + return (ok, errs) + +/-- Group records by their `file`. -/ +def byFile (rs : Array ReportRecord) : Std.HashMap String (Array ReportRecord) := + rs.foldl (init := {}) fun acc r => + let existing := acc.getD r.file #[] + acc.insert r.file (existing.push r) + +/-- Pad a string to at least `n` characters with trailing spaces. -/ +private def padTo (n : Nat) (s : String) : String := + if s.length ≥ n then s + else s ++ "".pushn ' ' (n - s.length) + +/-- Sort records within a file: by line first, then by name. -/ +private def sortByPosition (rs : Array ReportRecord) : Array ReportRecord := + rs.qsort fun a b => if a.line ≠ b.line then a.line < b.line else a.name < b.name + +/-- Render one file's records in text format. -/ +def renderTextFile (file : String) (rs : Array ReportRecord) : String := Id.run do + let total := rs.size + let safe := rs.filter (Verdict.classify · == .safeToUnexpose) + let load := rs.filter (Verdict.classify · == .loadBearing) + let noop := rs.filter (Verdict.classify · == .noopAlwaysExported) + let mut out := s!"{file}: {safe.size} safe-to-unexpose, " ++ + s!"{load.size} load-bearing, {noop.size} noop ({total} total)\n" + if !safe.isEmpty then + out := out ++ "\n safe-to-unexpose:\n" + for r in sortByPosition safe do + out := out ++ s!" {padTo 60 r.name} (line {r.line})\n" + if !load.isEmpty then + out := out ++ "\n load-bearing (must keep @[expose]):\n" + for r in sortByPosition load do + out := out ++ s!" {padTo 60 r.name} " ++ + s!"(line {r.line}; {r.downstreamUsage} uses across " ++ + s!"{r.numUsingFiles} files)\n" + return out + +/-- Render one file's records in TSV (no header per file; caller adds). -/ +def renderTsvFile (rs : Array ReportRecord) : String := Id.run do + let mut out := "" + for r in sortByPosition rs do + let top := String.intercalate ";" <| + r.topUsingFiles.toList.map fun (f, c) => s!"{f}:{c}" + out := out ++ s!"{r.name}\t{r.kind}\t{r.effect}\t{r.module}\t" ++ + s!"{r.file}:{r.line}\t{r.downstreamUsage}\t{r.numUsingFiles}\t{top}\n" + return out + +/-- Render one file's records in JSON (one object per file, decls grouped). -/ +def renderJsonFile (file : String) (rs : Array ReportRecord) : Json := Id.run do + let mkDecl (r : ReportRecord) : Json := Json.mkObj [ + ("name", r.name), + ("line", r.line), + ("downstream_usage", r.downstreamUsage), + ("num_using_files", r.numUsingFiles)] + let bucket (vs : Array ReportRecord) : Json := + .arr (sortByPosition vs |>.map mkDecl) + let safe := rs.filter (Verdict.classify · == .safeToUnexpose) + let load := rs.filter (Verdict.classify · == .loadBearing) + let noop := rs.filter (Verdict.classify · == .noopAlwaysExported) + return Json.mkObj [ + ("file", file), + ("safe_to_unexpose", bucket safe), + ("load_bearing", bucket load), + ("noop", bucket noop)] + +/-- Top-level `report` subcommand. -/ +def runReport (args : ReportArgs) : IO UInt32 := do + unless ← System.FilePath.pathExists reportPath do + IO.eprintln s!"no_expose: {reportPath} not found." + if args.collectOnDemand then + IO.eprintln " (would run `collect` here, but `collect` is not yet \ + implemented in the new tool — TODO)" + else + IO.eprintln " Run `lake exe no_expose collect` first, or pass \ + `--collect-on-demand`." + return 2 + let (records, errs) ← readReport reportPath + for e in errs do IO.eprintln s!"warning: {e}" + let groups := byFile records + -- Determine which files to render. + let selectedFiles : Array String := + if args.all then groups.toArray.map (·.1) + else args.paths + if selectedFiles.isEmpty then + IO.eprintln "no_expose: pass at least one PATH or --all" + return 2 + match args.format with + | .text => do + for f in selectedFiles do + let rs := groups.getD f #[] + if rs.isEmpty then + IO.println s!"{f}: no exposed decls in report" + else + IO.print (renderTextFile f rs) + | .json => do + let objs := selectedFiles.map fun f => + renderJsonFile f (groups.getD f #[]) + IO.println (Json.arr objs).pretty + | .tsv => do + IO.println "name\tkind\teffect\tmodule\tsource\tdownstream_usage\tnum_using_files\ttop_using_files" + for f in selectedFiles do + IO.print (renderTsvFile (groups.getD f #[])) + return 0 + +end NoExpose diff --git a/scripts/no_expose.lean b/scripts/no_expose.lean new file mode 100644 index 00000000000000..dc2eb9df012509 --- /dev/null +++ b/scripts/no_expose.lean @@ -0,0 +1,41 @@ +/- +Copyright (c) 2026 Kim Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +import NoExpose.Cli +import NoExpose.Paths +import NoExpose.Report + +/-! +# `lake exe no_expose` — entry point + +Tiny dispatcher. All work lives in `NoExpose.*` modules. +-/ + +open NoExpose + +unsafe def main (args : List String) : IO UInt32 := do + match parseArgs args with + | .error msg => do + IO.eprintln s!"no_expose: {msg}" + IO.eprintln "" + IO.eprintln helpText + return 2 + | .ok .help => do + IO.println helpText + return 0 + | .ok .clean => do + if ← System.FilePath.pathExists dataDir then + IO.FS.removeDirAll dataDir + IO.println s!"removed {dataDir}" + else + IO.println s!"{dataDir} does not exist; nothing to clean" + return 0 + | .ok (.collect _) => do + IO.eprintln "no_expose collect: not yet implemented" + return 1 + | .ok (.report a) => runReport a + | .ok (.edit _) => do + IO.eprintln "no_expose edit: not yet implemented" + return 1 From 71adda259a371fb03acc19c1dd1008b556a63daa Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 10 May 2026 14:35:44 +1000 Subject: [PATCH 07/27] feat(scripts): wire `lake exe no_expose collect` end-to-end MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- scripts/NoExpose/Collect.lean | 73 ++++++++++++ scripts/NoExpose/Env.lean | 204 ++++++++++++++++++++++++++++++++++ scripts/NoExpose/Report.lean | 168 +++++++++++++++++++++++++++- scripts/no_expose.lean | 5 +- 4 files changed, 445 insertions(+), 5 deletions(-) create mode 100644 scripts/NoExpose/Collect.lean create mode 100644 scripts/NoExpose/Env.lean diff --git a/scripts/NoExpose/Collect.lean b/scripts/NoExpose/Collect.lean new file mode 100644 index 00000000000000..e29ff094c510b7 --- /dev/null +++ b/scripts/NoExpose/Collect.lean @@ -0,0 +1,73 @@ +/- +Copyright (c) 2026 Kim Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +import NoExpose.Cli +import NoExpose.Env +import NoExpose.Paths +import NoExpose.Report + +/-! +# `NoExpose.Collect` — orchestrator for the `collect` subcommand + +Owns the high-level sequence: +1. (TODO) `NoExpose.Diagnostics`: patch lakefile, run `lake build`, parse log. +2. `NoExpose.Env`: open env via `withImportModules`; emit + `exposed.jsonl`, `static_refs.jsonl`, `decl_refs.jsonl`. +3. `NoExpose.Report.build`: join everything into `report.jsonl`. + +For now only step 2 + 3 are implemented (i.e. `--skip-build` mode). +-/ + +open Lean + +namespace NoExpose + +/-- Run the env-scan portion of `collect`: opens the env once via +`withImportModules`, then writes all three JSONLs. Defaults to +importing the project's lib roots. -/ +unsafe def runEnvScan (project : ProjectInfo) (modules : Array Name) + (scopePrefix : Array Name) : IO Unit := do + IO.FS.createDirAll dataDir + let searchPath ← addSearchPathFromEnv (← getBuiltinSearchPath (← findSysroot)) + withImportModules modules (searchPath := searchPath) (trustLevel := 1024) do + let env ← getEnv + -- 1. Enumeration → exposed.jsonl + let recs ← enumerate scopePrefix + IO.FS.withFile exposedPath .write fun h => do + for r in recs do h.putStrLn r.toJsonLine + IO.eprintln s!"[no_expose collect] wrote {recs.size} exposed records to {exposedPath}" + -- 2. Static refs → static_refs.jsonl + let refs ← collectStaticRefs + IO.FS.withFile staticRefsPath .write fun h => writeStaticRefs env refs h + IO.eprintln s!"[no_expose collect] wrote {refs.size} static-refs pairs to {staticRefsPath}" + -- 3. Per-decl refs → decl_refs.jsonl + IO.FS.withFile declRefsPath .write fun h => writeDeclRefs env h + IO.eprintln s!"[no_expose collect] wrote per-decl refs to {declRefsPath}" + -- Mark unused + let _ := project + +/-- Run the `collect` subcommand. -/ +unsafe def runCollect (args : CollectArgs) : IO UInt32 := do + let project ← detectProjectInfo + IO.eprintln s!"[no_expose collect] project: {project.name} \ + (libs: {project.libRoots})" + unless args.skipBuild do + IO.eprintln "no_expose collect: full build mode not yet implemented; \ + pass --skip-build to use existing oleans + diagnostics.jsonl." + return 1 + -- For Mathlib, the canonical target is just `Mathlib` (the union module). + -- For downstream projects, pick the first lib root. + let modules : Array Name := + if project.libRoots.contains `Mathlib then #[`Mathlib] + else project.libRoots.take 1 + let scopePrefix : Array Name := + if project.libRoots.contains `Mathlib then #[`Mathlib] + else project.libRoots + runEnvScan project modules scopePrefix + -- Now build report.jsonl by joining everything. + build exposedPath diagnosticsPath staticRefsPath declRefsPath reportPath + return 0 + +end NoExpose diff --git a/scripts/NoExpose/Env.lean b/scripts/NoExpose/Env.lean new file mode 100644 index 00000000000000..5752e4edfa5b2a --- /dev/null +++ b/scripts/NoExpose/Env.lean @@ -0,0 +1,204 @@ +/- +Copyright (c) 2026 Kim Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +import Lean + +/-! +# `NoExpose.Env` — env-walk pieces (enumeration + static refs) + +Three responsibilities, all running inside a `Lean.withImportModules` +block opened by the `collect` orchestrator: + +* **enumerate**: emit one record per "candidate" decl in the project's + scope (a def whose body is in the exported view, isn't a compiler + helper, isn't an instance whose exposure is automatic). +* **staticRefs**: per-(refModule, refName) cross-reference counts, with + a `theorem_count` split for same-module rfl detection. +* **declRefs**: per-decl direct reference list, used downstream by + `Report` for one-hop transitive closure. + +This module does NOT `import Mathlib`. The +`CoreM.withImportModules` helper is inlined from `Mathlib.Lean.CoreM` +(11 lines, MIT-licensed) so the exe links against just Lean core + +Lake. +-/ + +open Lean Core + +namespace NoExpose + +/-- Inlined from `Mathlib/Lean/CoreM.lean`: run a `CoreM α` against a +fresh `Environment` populated by importing `modules`. Mathlib import +removed; depends only on Lean core APIs. -/ +def withImportModules {α : Type} (modules : Array Name) (run : CoreM α) + (searchPath : Option SearchPath := none) (options : Options := {}) + (trustLevel : UInt32 := 0) (fileName := "") : + IO α := unsafe do + if let some sp := searchPath then searchPathRef.set sp + Lean.withImportModules (modules.map ({ module := · })) options + (trustLevel := trustLevel) fun env => do + let ctx : Core.Context := { fileName, options, fileMap := default } + let state : Core.State := { env } + let (a, _) ← Core.CoreM.toIO run ctx state + pure a + +/-! ## Enumeration -/ + +/-- One row of the eventual `exposed.jsonl`. -/ +structure DeclRecord where + name : Name + kind : String + «module» : Name + file : String + line : Nat + col : Nat + «effect» : String + +/-- Suffixes Lean uses for compiler-generated structure/inductive +helpers; we exclude them since they aren't user-written `@[expose]` +candidates. -/ +private def autoGenSuffixes : Array String := #[ + "recOn", "casesOn", "brecOn", "binductionOn", "below", "ibelow", "ndrec", + "ndrecOn", "recAux", "rec", "noConfusion", "noConfusionType", "sizeOf", + "sizeOf_spec", "injEq" +] + +/-- True if `name` is a compiler helper we should exclude from +enumeration. Mirrors the predicate in the legacy `expose_enumerate`. -/ +def isAutoGen (env : Environment) (name : Name) : CoreM Bool := do + if Lean.isAuxRecursor env name then return true + if Lean.isNoConfusion env name then return true + if (env.getProjectionFnInfo? name).isSome then return true + if ← Lean.Meta.isMatcher name then return true + if let .str _ last := name then + if autoGenSuffixes.contains last then return true + return false + +/-- True if `name`'s body is in the *exported* view of `env`. -/ +def isBodyExported (env : Environment) (name : Name) : Bool := + match (env.setExporting true).find? name with + | some info => info.hasValue + | none => false + +/-- Map `Mathlib.Foo.Bar` → `"Mathlib/Foo/Bar.lean"`. -/ +def moduleToPath (m : Name) : String := + String.intercalate "/" (m.toString.splitOn ".") ++ ".lean" + +/-- Constant `name` lives in one of the project's modules — i.e. the +declaring module's name has one of `scopePrefix` as a `Name`-prefix. -/ +private def isInScope (env : Environment) (scopePrefix : Array Name) (name : Name) : + Option Name := do + let idx ← env.getModuleIdxFor? name + let mod := env.header.moduleNames[idx]! + if scopePrefix.any fun p => p.isPrefixOf mod || p == mod then + some mod + else + none + +/-- Collect the enumeration records. -/ +def enumerate (scopePrefix : Array Name) : CoreM (Array DeclRecord) := do + let env ← getEnv + let instSet := (Lean.Meta.instanceExtension.getState env).instanceNames + let mut out : Array DeclRecord := #[] + let mut instSkipped : Nat := 0 + for (name, info) in env.constants.toList do + let .defnInfo defnVal := info | continue + let some mod := isInScope env scopePrefix name | continue + if name.hasMacroScopes then continue + if name.isInternal then continue + if ← isAutoGen env name then continue + unless isBodyExported env name do continue + if instSet.contains name then + instSkipped := instSkipped + 1 + continue + let isAbbrev := defnVal.hints.isAbbrev + let kind := "def" + let «effect» := if isAbbrev then "noop-always-exported" else "exposed" + let some ranges ← Lean.findDeclarationRanges? name | continue + let pos := ranges.range.pos + out := out.push { + name + kind + «module» := mod + file := moduleToPath mod + line := pos.line + col := pos.column + «effect» + } + IO.eprintln s!"[no_expose enumerate] excluded {instSkipped} instances (expose is a no-op)" + return out + +/-! ## Static references -/ + +/-- Mirrors the legacy `expose_static_refs.lean`: for each +(referencing module, referenced name), `(total_count, theorem_count)`. -/ +abbrev RefMap := Std.HashMap (Nat × Name) (Nat × Nat) + +/-- Walk every constant in env; aggregate by (refModule, refName). -/ +def collectStaticRefs : CoreM RefMap := do + let env ← getEnv + let mut acc : RefMap := {} + for (name, info) in env.constants.toList do + let some refModIdx := env.getModuleIdxFor? name | continue + if name.hasMacroScopes then continue + if name.isInternal then continue + let isThm := info matches .thmInfo _ + let refs := info.getUsedConstantsAsSet + acc := refs.foldl (init := acc) fun acc referenced => + let key := (refModIdx, referenced) + let (cTot, cThm) := acc.getD key (0, 0) + acc.insert key (cTot + 1, if isThm then cThm + 1 else cThm) + return acc + +/-! ## JSON serialisation -/ + +/-- JSON-string-escape `s`. -/ +private def jsonEscape (s : String) : String := + s.foldl (init := "") fun acc c => acc ++ + match c with + | '"' => "\\\"" + | '\\' => "\\\\" + | '\n' => "\\n" + | '\r' => "\\r" + | '\t' => "\\t" + | c => c.toString + +def DeclRecord.toJsonLine (d : DeclRecord) : String := + "{\"name\":\"" ++ jsonEscape d.name.toString ++ + "\",\"kind\":\"" ++ d.kind ++ + "\",\"module\":\"" ++ jsonEscape d.module.toString ++ + "\",\"file\":\"" ++ jsonEscape d.file ++ + "\",\"line\":" ++ toString d.line ++ + ",\"col\":" ++ toString d.col ++ + ",\"effect\":\"" ++ d.effect ++ "\"}" + +/-- Write a `RefMap` aggregation as one JSONL record per pair. -/ +def writeStaticRefs (env : Environment) (acc : RefMap) + (h : IO.FS.Handle) : IO Unit := do + for ((modIdx, decl), (count, thmCount)) in acc.toList do + let some mod := env.header.moduleNames[modIdx]? | continue + let file := moduleToPath mod + h.putStrLn <| + "{\"file\":\"" ++ jsonEscape file ++ + "\",\"decl\":\"" ++ jsonEscape decl.toString ++ + "\",\"count\":" ++ toString count ++ + ",\"theorem_count\":" ++ toString thmCount ++ + ",\"category\":\"static/ref\"}" + +/-- Write per-decl direct reference lists for transitive closure. -/ +def writeDeclRefs (env : Environment) (h : IO.FS.Handle) : IO Unit := do + for (name, info) in env.constants.toList do + if name.hasMacroScopes then continue + if name.isInternal then continue + if (env.getModuleIdxFor? name).isNone then continue + let refs := info.getUsedConstantsAsSet + if refs.isEmpty then continue + let body : String := String.intercalate "," <| + refs.foldl (init := []) (fun acc n => ("\"" ++ jsonEscape n.toString ++ "\"") :: acc) + h.putStrLn <| + "{\"decl\":\"" ++ jsonEscape name.toString ++ + "\",\"refs\":[" ++ body ++ "]}" + +end NoExpose diff --git a/scripts/NoExpose/Report.lean b/scripts/NoExpose/Report.lean index c697985e3f172b..de79efa1e876f6 100644 --- a/scripts/NoExpose/Report.lean +++ b/scripts/NoExpose/Report.lean @@ -17,8 +17,8 @@ and `edit` need: {"name": "Foo.bar", "kind": "def", "effect": "exposed", "module": "Mathlib.Foo", "file": "Mathlib/Foo.lean", "line": 42, "col": 0, - "downstream_usage": 17, "num_using_files": 5, - "top_using_files": [{"file": "...", "count": 4}, ...]} + "downstream_usage": 17, "num_usingMap_files": 5, + "top_usingMap_files": [{"file": "...", "count": 4}, ...]} ``` This module parses those records and renders per-file output in three @@ -210,4 +210,168 @@ def runReport (args : ReportArgs) : IO UInt32 := do IO.print (renderTsvFile (groups.getD f #[])) return 0 +/-! ## Build side: join raw signals into `report.jsonl` -/ + +/-- Decl key + originating file. `Std.HashMap` lacks structural keys +of arbitrary nested type, so we use a `String × String` here. -/ +private abbrev UseKey := String × String + +/-- Parse one line of `diagnostics.jsonl` or `static_refs.jsonl`. Returns +`(decl, file, count, theoremCount)`. `theoremCount = 0` when the field +is absent (diagnostics records). -/ +private def parseSignalLine (line : String) : + Except String (String × String × Nat × Nat) := do + let j ← Json.parse line + let decl ← jsonGetStr j "decl" + let file ← jsonGetStr j "file" + let count ← jsonGetNat j "count" + let thm := j.getObjVal? "theorem_count" |>.toOption + |>.bind (·.getNat?.toOption) |>.getD 0 + return (decl, file, count, thm) + +/-- Parse one line of `decl_refs.jsonl`: `{decl: ..., refs: [...]}`. -/ +private def parseDeclRefsLine (line : String) : + Except String (String × Array String) := do + let j ← Json.parse line + let decl ← jsonGetStr j "decl" + let refsJ ← j.getObjVal? "refs" + let refsArr ← refsJ.getArr? + let refs ← refsArr.mapM (·.getStr?) + return (decl, refs) + +/-- Read `exposed.jsonl` into a map keyed by decl name. -/ +private def readExposed (path : System.FilePath) : IO (Std.HashMap String Json) := do + let mut acc : Std.HashMap String Json := {} + for line in (← IO.FS.readFile path).splitOn "\n" do + if line.trimAscii.isEmpty then continue + match Json.parse line with + | .ok j => + match jsonGetStr j "name" with + | .ok name => acc := acc.insert name j + | .error _ => pure () + | .error _ => pure () + return acc + +/-- Same-module-but-from-theorem references count; other same-module +refs are skipped. Mirrors `expose_report.py:117`. -/ +private def shouldCount (sameModule : Bool) (count theoremCount : Nat) : Option Nat := + if sameModule then + if theoremCount > 0 then some theoremCount else none + else + some count + +/-- Absorb one signal file into the running usage map. Returns the +number of records actually counted (skipping any that don't match an +exposed decl or are filtered out). -/ +private def absorbSignal (exposed : Std.HashMap String Json) + (path : System.FilePath) + (usage : Std.HashMap String Nat) + (usingMap : Std.HashMap UseKey Nat) : + IO (Std.HashMap String Nat × Std.HashMap UseKey Nat × Nat) := do + let mut usage := usage + let mut usingMap := usingMap + let mut absorbed := 0 + for line in (← IO.FS.readFile path).splitOn "\n" do + if line.trimAscii.isEmpty then continue + match parseSignalLine line with + | .error _ => continue + | .ok (decl, file, count, thm) => + let some rec := exposed[decl]? | continue + let recFile := (rec.getObjVal? "file" |>.bind (·.getStr?)).toOption.getD "" + let some delta := shouldCount (file == recFile) count thm | continue + usage := usage.insert decl ((usage.getD decl 0) + delta) + let key : UseKey := (decl, file) + usingMap := usingMap.insert key ((usingMap.getD key 0) + delta) + absorbed := absorbed + 1 + return (usage, usingMap, absorbed) + +/-- One-hop transitive closure: a downstream use of decl `K` propagates +to every decl in `K`'s body. Mirrors `expose_report.py:154`. -/ +private def applyTransitiveClosure (exposed : Std.HashMap String Json) + (declRefsPath : System.FilePath) + (usage : Std.HashMap String Nat) + (usingMap : Std.HashMap UseKey Nat) : + IO (Std.HashMap String Nat × Std.HashMap UseKey Nat × Nat) := do + -- Load decl_refs into a map. + let mut refsMap : Std.HashMap String (Array String) := {} + for line in (← IO.FS.readFile declRefsPath).splitOn "\n" do + if line.trimAscii.isEmpty then continue + if let .ok (decl, refs) := parseDeclRefsLine line then + refsMap := refsMap.insert decl refs + -- Snapshot usingMap to avoid iterating while mutating. + let snapshot := usingMap.toArray + let mut usage := usage + let mut usingMap := usingMap + let mut propagated := 0 + for ((decl, file), count) in snapshot do + let some refs := refsMap[decl]? | continue + for ref in refs do + let some refRec := exposed[ref]? | continue + let recFile := (refRec.getObjVal? "file" |>.bind (·.getStr?)).toOption.getD "" + if file == recFile then continue -- same-module + usage := usage.insert ref ((usage.getD ref 0) + count) + let key : UseKey := (ref, file) + usingMap := usingMap.insert key ((usingMap.getD key 0) + count) + propagated := propagated + 1 + return (usage, usingMap, propagated) + +/-- JSON-string-escape `s` (duplicate of `Env.jsonEscape` to keep this +module standalone). -/ +private def jsonEscape (s : String) : String := + s.foldl (init := "") fun acc c => acc ++ + match c with + | '"' => "\\\"" + | '\\' => "\\\\" + | '\n' => "\\n" + | '\r' => "\\r" + | '\t' => "\\t" + | c => c.toString + +/-- Build `report.jsonl` by joining the four input files. -/ +def build (exposedPath diagnosticsPath staticRefsPath declRefsPath : System.FilePath) + (outPath : System.FilePath) : IO Unit := do + let exposed ← readExposed exposedPath + IO.eprintln s!"[no_expose report] loaded {exposed.size} exposed decls" + + let mut usage : Std.HashMap String Nat := {} + let mut usingMap : Std.HashMap UseKey Nat := {} + if ← System.FilePath.pathExists diagnosticsPath then + let (u, uf, n) ← absorbSignal exposed diagnosticsPath usage usingMap + usage := u; usingMap := uf + IO.eprintln s!"[no_expose report] absorbed {n} diagnostics records" + if ← System.FilePath.pathExists staticRefsPath then + let (u, uf, n) ← absorbSignal exposed staticRefsPath usage usingMap + usage := u; usingMap := uf + IO.eprintln s!"[no_expose report] absorbed {n} static-reference records" + if ← System.FilePath.pathExists declRefsPath then + let (u, uf, n) ← applyTransitiveClosure exposed declRefsPath usage usingMap + usage := u; usingMap := uf + IO.eprintln s!"[no_expose report] one-hop transitive: propagated {n} extra (ref,file) edges" + + -- Build per-decl `top_usingMap_files` from `usingMap`. + let mut perDecl : Std.HashMap String (Array (String × Nat)) := {} + for ((decl, file), count) in usingMap.toArray do + let cur := perDecl.getD decl #[] + perDecl := perDecl.insert decl (cur.push (file, count)) + + IO.FS.writeFile outPath "" + IO.FS.withFile outPath .append fun h => do + for (name, exposedRec) in exposed.toArray do + let u := usage.getD name 0 + let top := perDecl.getD name #[] + let topSorted := top.qsort fun a b => a.2 > b.2 + let topNFiles := top.size + let top5 := topSorted.take 5 + let topJson := "[" ++ String.intercalate "," (top5.toList.map fun (f, c) => + "{\"file\":\"" ++ jsonEscape f ++ "\",\"count\":" ++ toString c ++ "}") ++ "]" + -- Re-emit the original exposed record's fields plus our additions. + let baseStr := exposedRec.compress + -- Drop the trailing `}` and append our fields. + let baseStripped := baseStr.dropRight 1 + h.putStrLn (baseStripped ++ + ",\"downstream_usage\":" ++ toString u ++ + ",\"num_using_files\":" ++ toString topNFiles ++ + ",\"top_using_files\":" ++ topJson ++ "}") + IO.eprintln s!"[no_expose report] wrote {exposed.size} report rows to {outPath}" + end NoExpose diff --git a/scripts/no_expose.lean b/scripts/no_expose.lean index dc2eb9df012509..2f37a9745694ad 100644 --- a/scripts/no_expose.lean +++ b/scripts/no_expose.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison -/ import NoExpose.Cli +import NoExpose.Collect import NoExpose.Paths import NoExpose.Report @@ -32,9 +33,7 @@ unsafe def main (args : List String) : IO UInt32 := do else IO.println s!"{dataDir} does not exist; nothing to clean" return 0 - | .ok (.collect _) => do - IO.eprintln "no_expose collect: not yet implemented" - return 1 + | .ok (.collect a) => runCollect a | .ok (.report a) => runReport a | .ok (.edit _) => do IO.eprintln "no_expose edit: not yet implemented" From 94911297d2ef1796b65e656d98de4fff7ad602fd Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 10 May 2026 14:46:27 +1000 Subject: [PATCH 08/27] feat(scripts): add Restore, Diagnostics, Edit modules to no_expose MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- scripts/NoExpose/Diagnostics.lean | 278 +++++++++++++++++++++++++++++ scripts/NoExpose/Edit.lean | 286 ++++++++++++++++++++++++++++++ scripts/NoExpose/Restore.lean | 117 ++++++++++++ scripts/no_expose.lean | 5 +- 4 files changed, 683 insertions(+), 3 deletions(-) create mode 100644 scripts/NoExpose/Diagnostics.lean create mode 100644 scripts/NoExpose/Edit.lean create mode 100644 scripts/NoExpose/Restore.lean diff --git a/scripts/NoExpose/Diagnostics.lean b/scripts/NoExpose/Diagnostics.lean new file mode 100644 index 00000000000000..7105ee49d3da07 --- /dev/null +++ b/scripts/NoExpose/Diagnostics.lean @@ -0,0 +1,278 @@ +/- +Copyright (c) 2026 Kim Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +import NoExpose.Paths +import NoExpose.Restore + +/-! +# `NoExpose.Diagnostics` — lakefile patch + lake build + log parser + +Ports the responsibilities of `scripts/build_with_diagnostics.py` into +Lean. Three pieces: + +* **patchLakefile**: insert two `mathlibLeanOptions` entries + (`diagnostics=true`, `diagnostics.threshold=0`). v1 is Mathlib-only: + recognises the existing `mathlibLeanOptions` `abbrev`. Anything else + errors out. +* **patchDiagnosticsOffFiles**: 5-file hardcoded list of source files + that fail to elaborate under global `diagnostics=true`; we splice in + `set_option diagnostics false` after the last import. +* **parseLog**: scan `build.log` line-by-line, emit one JSONL record + per (file, decl, count, category) tuple. + +The build itself is `lake build Mathlib`, run as a child process. +Hours of CPU; gated on `--full-build` (default off — `--skip-build` +remains the working mode). +-/ + +open System + +namespace NoExpose + +/-! ## Lakefile patching -/ + +private def patchMarkerBegin : String := + " -- BEGIN no_expose diagnostics patch" +private def patchMarkerEnd : String := + " -- END no_expose diagnostics patch" + +private def patchAnchor : String := " ⟨`autoImplicit, false⟩,\n" + +private def patchBlock : String := + patchMarkerBegin ++ "\n" ++ + " ⟨`diagnostics, true⟩,\n" ++ + " ⟨`diagnostics.threshold, (0 : Nat)⟩,\n" ++ + patchMarkerEnd ++ "\n" + +/-- Insert the diagnostics options into Mathlib's `mathlibLeanOptions`. +Aborts (with a clear error) for any non-Mathlib lakefile shape. -/ +def patchLakefile (lakefilePath : FilePath) : IO Unit := do + let original ← IO.FS.readFile lakefilePath + let markerHits := (original.splitOn patchMarkerBegin).length + if markerHits > 1 then + throw <| IO.userError s!"{lakefilePath} already contains no_expose patch markers; \ + restore it manually before re-running." + let anchorHits := (original.splitOn patchAnchor).length + unless anchorHits > 1 do + throw <| IO.userError s!"could not find insertion anchor in {lakefilePath}; \ + v1 supports Mathlib-shaped lakefiles only. \ + Pass --skip-build and enable diagnostics yourself, or run on Mathlib." + -- Replace first occurrence only. + let parts := original.splitOn patchAnchor + let patched := parts[0]! ++ patchAnchor ++ patchBlock ++ + String.intercalate patchAnchor (parts.drop 1) + -- Back up before writing. + backup lakefilePath + IO.FS.writeFile lakefilePath patched + +/-! ## Per-file diagnostics-off patches + +Five Mathlib files fail under global `diagnostics=true`. Splice +`set_option diagnostics false` after the last `import` line. -/ + +/-- Mathlib's hardcoded fragile-files list. Override via +`patchDiagnosticsOffFiles extra` to add downstream files. -/ +def diagnosticsOffFiles : Array FilePath := #[ + "Mathlib/Tactic/Linter/ValidatePRTitle.lean", + "Mathlib/Order/Interval/Lex.lean", + "Mathlib/Tactic/NormNum/Ordinal.lean", + "Mathlib/Probability/ConditionalProbability.lean", + "Mathlib/CategoryTheory/Discrete/Basic.lean"] + +private def filePatchLine : String := + "-- no_expose: locally disable diagnostics so this file builds " ++ + "under global `diagnostics=true`\nset_option diagnostics false\n" + +/-- Insert `set_option diagnostics false` after the last +`import` / `public import` line. Idempotent: re-applying is a no-op. -/ +def patchOneFile (path : FilePath) : IO Unit := do + unless ← System.FilePath.pathExists path do + IO.eprintln s!"[no_expose diagnostics] skipping non-existent {path}" + return + let text ← IO.FS.readFile path + let alreadyPatched := (text.splitOn filePatchLine).length > 1 + if alreadyPatched then return + let lines : List String := text.splitOn "\n" + let mut lastImport : Int := -1 + for h : i in [:lines.length] do + let line : String := lines[i] + let stripped : String := line.trimAscii.toString + if stripped.startsWith "import " || stripped.startsWith "public import " then + lastImport := i + if lastImport < 0 then + throw <| IO.userError s!"no import line in {path}; can't insert set_option" + let i := lastImport.toNat + 1 + let prefixLines := lines.take i + let suffixLines := lines.drop i + let patched := String.intercalate "\n" + (prefixLines ++ ["", filePatchLine.trimAsciiEnd.toString] ++ suffixLines) + backup path + IO.FS.writeFile path patched + +/-- Patch all `diagnosticsOffFiles ++ extra`. -/ +def patchDiagnosticsOffFiles (extra : Array FilePath := #[]) : IO Unit := do + for p in diagnosticsOffFiles ++ extra do patchOneFile p + +/-! ## Build-log parser -/ + +structure DiagRecord where + file : String + decl : String + count : Nat + category : String + deriving Inhabited + +private def diagToJsonLine (r : DiagRecord) : String := + "{\"file\":\"" ++ r.file ++ "\",\"decl\":\"" ++ r.decl ++ + "\",\"count\":" ++ toString r.count ++ + ",\"category\":\"" ++ r.category ++ "\"}" + +private def categoryShort (tag label : String) : Option String := + match tag, label with + | "reduction", "unfolded declarations" => some "reduction/unfolded" + | "reduction", "unfolded instances" => some "reduction/instances" + | "reduction", "unfolded reducible declarations" => some "reduction/reducible" + | "kernel", "unfolded declarations" => some "kernel/unfolded" + | "type_class","used instances" => some "type_class/used" + | _, _ => none + +private def targetToFile (target : String) : Option String := + if target.contains ':' then none + else some (target.replace "." "/" ++ ".lean") + +/-- Match `✔ [N/M] Built Mathlib.Foo.Bar` and friends; return the target. -/ +private def parseBuiltLine (line : String) : Option String := Id.run do + -- Accept any of ✔ ℹ ⚠ ✖ as the leading bullet. Cheap precheck. + unless line.startsWith "✔" || line.startsWith "ℹ" || + line.startsWith "⚠" || line.startsWith "✖" do return none + let parts : List String := line.splitOn "Built " + unless parts.length ≥ 2 do return none + let after : String := parts[1]! + -- `Mathlib.Foo` then optional whitespace; take up to first space. + let target : String := + (after.takeWhile (fun c => c != ' ' && c != '\t' && c != '\n')).toString + return some target + +/-- Strip a literal `[tag] ` prefix; on success return `(tag, rest)`. -/ +private def stripTagPrefix (s : String) : Option (String × String) := Id.run do + unless s.startsWith "[" do return none + for tag in ["reduction", "kernel", "type_class"] do + let p := "[" ++ tag ++ "] " + if s.startsWith p then + let rest : String := s.drop p.length |>.toString + return some (tag, rest) + return none + +/-- `[reduction] unfolded declarations (max: N, num: M):` -/ +private def parseCategoryHeader (line : String) : Option (String × String) := Id.run do + let trimmed : String := line.trimAscii.toString + let some (tag, rest) := stripTagPrefix trimmed | none + unless line.endsWith ":" do return none + -- `rest` is `