|
| 1 | +#!/usr/bin/env python3 |
| 2 | +""" |
| 3 | +Part of the `@[expose]` removal-candidate reporting pipeline |
| 4 | +(see `scripts/expose_enumerate.lean` and `scripts/expose_report.py`). |
| 5 | +
|
| 6 | +Runs a full `lake build Mathlib` with `diagnostics=true` and |
| 7 | +`diagnostics.threshold=0` enabled, captures per-file diagnostic output, and |
| 8 | +emits one JSONL record per unfold event observed during elaboration. |
| 9 | +
|
| 10 | +Workflow: |
| 11 | + 1. Patch `lakefile.lean` to append the diagnostics options to |
| 12 | + `mathlibLeanOptions` (this *does* affect the olean hash; a full local |
| 13 | + rebuild is expected). |
| 14 | + 2. Run `lake build Mathlib`, streaming and teeing output to |
| 15 | + `scripts/.expose_report/build.log`. |
| 16 | + 3. Parse the captured log into per-file unfold records. |
| 17 | + 4. Emit `scripts/.expose_report/diagnostics.jsonl` — one record per |
| 18 | + (file, decl, category) triple. |
| 19 | + 5. Restore `lakefile.lean` (always; even on failure / Ctrl-C). |
| 20 | +
|
| 21 | +Expected runtime: several hours for a full Mathlib rebuild with diagnostics. |
| 22 | +Kim signed off on this cost: this is a one-off / occasional report. |
| 23 | +
|
| 24 | +Usage: |
| 25 | + python3 scripts/build_with_diagnostics.py |
| 26 | + python3 scripts/build_with_diagnostics.py --skip-build # re-parse existing log |
| 27 | + python3 scripts/build_with_diagnostics.py --log PATH # use alt log path |
| 28 | +
|
| 29 | +Output records: |
| 30 | + { |
| 31 | + "file": "Mathlib/Foo/Bar.lean", |
| 32 | + "decl": "Other.Module.name", |
| 33 | + "count": 3, |
| 34 | + "category": "reduction/unfolded" | "reduction/instances" |
| 35 | + | "reduction/reducible" | "kernel/unfolded" |
| 36 | + } |
| 37 | +
|
| 38 | +Limitations: |
| 39 | + * Signal is unfold-based; metaprograms that inspect `ConstantInfo.value?` |
| 40 | + without triggering a WHNF unfold don't appear here. A decl absent from |
| 41 | + this output may still be load-bearing downstream via metaprogramming. |
| 42 | + * `diagnostics.threshold` is set to `0`: every unfold appears in the |
| 43 | + report (counts > 0, since the threshold check is strictly-greater-than). |
| 44 | + A "never unfolded downstream" verdict means absence from the per-file |
| 45 | + diagnostic output — Lean does not emit zero-count rows. Un-exposure |
| 46 | + candidates should still be verified by trying the change and |
| 47 | + re-building, since metaprograms that inspect `ConstantInfo.value?` |
| 48 | + without a WHNF unfold won't appear here either. |
| 49 | +
|
| 50 | + Note: low thresholds previously triggered |
| 51 | + https://github.com/leanprover/lean4/issues/13581 (private-helper |
| 52 | + rendering crash) on `nightly-2026-05-06` and earlier. Fixed by |
| 53 | + https://github.com/leanprover/lean4/pull/13630 (in |
| 54 | + `nightly-2026-05-07` and later). |
| 55 | +""" |
| 56 | + |
| 57 | +import argparse |
| 58 | +import json |
| 59 | +import os |
| 60 | +import re |
| 61 | +import shutil |
| 62 | +import signal |
| 63 | +import subprocess |
| 64 | +import sys |
| 65 | +from pathlib import Path |
| 66 | + |
| 67 | + |
| 68 | +REPO_ROOT = Path(__file__).resolve().parent.parent |
| 69 | +LAKEFILE = REPO_ROOT / "lakefile.lean" |
| 70 | +OUTPUT_DIR = REPO_ROOT / "scripts" / ".expose_report" |
| 71 | +DEFAULT_LOG = OUTPUT_DIR / "build.log" |
| 72 | +DEFAULT_JSONL = OUTPUT_DIR / "diagnostics.jsonl" |
| 73 | + |
| 74 | +PATCH_MARKER_BEGIN = "-- BEGIN expose_report diagnostics patch" |
| 75 | +PATCH_MARKER_END = "-- END expose_report diagnostics patch" |
| 76 | + |
| 77 | +# The extra LeanOptions lines inserted into `mathlibLeanOptions`. |
| 78 | +PATCH_BLOCK = f""" {PATCH_MARKER_BEGIN} |
| 79 | + ⟨`diagnostics, true⟩, |
| 80 | + ⟨`diagnostics.threshold, (0 : Nat)⟩, |
| 81 | + {PATCH_MARKER_END} |
| 82 | +""" |
| 83 | + |
| 84 | +# Insertion anchor inside `mathlibLeanOptions := #[ ... ]`. We insert *after* |
| 85 | +# this line (which has no trailing comment, so preserving trailing text is |
| 86 | +# not an issue). |
| 87 | +ANCHOR = " ⟨`autoImplicit, false⟩,\n" |
| 88 | + |
| 89 | + |
| 90 | +def patch_lakefile() -> str: |
| 91 | + """Insert the diagnostics options into mathlibLeanOptions. Returns the |
| 92 | + original contents (for restoration).""" |
| 93 | + original = LAKEFILE.read_text() |
| 94 | + if PATCH_MARKER_BEGIN in original: |
| 95 | + raise RuntimeError( |
| 96 | + "lakefile.lean already contains expose_report patch markers; " |
| 97 | + "restore it manually before running again." |
| 98 | + ) |
| 99 | + if ANCHOR not in original: |
| 100 | + raise RuntimeError( |
| 101 | + f"Could not find insertion anchor in lakefile.lean:\n {ANCHOR!r}" |
| 102 | + ) |
| 103 | + patched = original.replace(ANCHOR, ANCHOR + PATCH_BLOCK, 1) |
| 104 | + LAKEFILE.write_text(patched) |
| 105 | + return original |
| 106 | + |
| 107 | + |
| 108 | +def restore_lakefile(original: str) -> None: |
| 109 | + LAKEFILE.write_text(original) |
| 110 | + |
| 111 | + |
| 112 | +def run_build(log_path: Path) -> int: |
| 113 | + """Stream `lake build Mathlib` to stdout and to `log_path`. Returns exit.""" |
| 114 | + log_path.parent.mkdir(parents=True, exist_ok=True) |
| 115 | + cmd = ["lake", "build", "Mathlib"] |
| 116 | + print(f"[build_with_diagnostics] running: {' '.join(cmd)}", flush=True) |
| 117 | + with open(log_path, "w") as log: |
| 118 | + proc = subprocess.Popen( |
| 119 | + cmd, |
| 120 | + cwd=str(REPO_ROOT), |
| 121 | + stdout=subprocess.PIPE, |
| 122 | + stderr=subprocess.STDOUT, |
| 123 | + text=True, |
| 124 | + bufsize=1, |
| 125 | + ) |
| 126 | + assert proc.stdout is not None |
| 127 | + try: |
| 128 | + for line in proc.stdout: |
| 129 | + sys.stdout.write(line) |
| 130 | + sys.stdout.flush() |
| 131 | + log.write(line) |
| 132 | + except KeyboardInterrupt: |
| 133 | + proc.send_signal(signal.SIGINT) |
| 134 | + raise |
| 135 | + proc.wait() |
| 136 | + return proc.returncode |
| 137 | + |
| 138 | + |
| 139 | +# --- log parsing -------------------------------------------------------- |
| 140 | + |
| 141 | +# Build-progress line: "✔ [N/M] Built Mathlib.Foo.Bar" or "ℹ [N/M] Built …" |
| 142 | +# File attribution is driven entirely off this line: lake prints a file's |
| 143 | +# info/trace/warning output immediately after its `Built` header, so the |
| 144 | +# current-file cursor is unambiguous within a block. |
| 145 | +BUILT_RE = re.compile( |
| 146 | + r"^[\u2714\u2139\u26A0\u2716]\s+\[\d+/\d+\]\s+Built\s+(\S+)" |
| 147 | +) |
| 148 | +# Header: ` [reduction] unfolded declarations (max: N, num: M):` |
| 149 | +CATEGORY_HEADER_RE = re.compile( |
| 150 | + r"^\s*\[(reduction|kernel)\]\s+(unfolded declarations|" |
| 151 | + r"unfolded instances|unfolded reducible declarations)\s*" |
| 152 | + r"\(max: \d+, num: \d+\):\s*$" |
| 153 | +) |
| 154 | +# Entry: ` [reduction] Foo.bar ↦ 3` |
| 155 | +ENTRY_RE = re.compile( |
| 156 | + r"^\s*\[(reduction|kernel)\]\s+(\S.*?)\s+↦\s+(\d+)\s*$" |
| 157 | +) |
| 158 | + |
| 159 | +CATEGORY_SHORT = { |
| 160 | + ("reduction", "unfolded declarations"): "reduction/unfolded", |
| 161 | + ("reduction", "unfolded instances"): "reduction/instances", |
| 162 | + ("reduction", "unfolded reducible declarations"): "reduction/reducible", |
| 163 | + ("kernel", "unfolded declarations"): "kernel/unfolded", |
| 164 | +} |
| 165 | + |
| 166 | + |
| 167 | +def target_to_file(target: str) -> str | None: |
| 168 | + """Convert `Mathlib.Foo.Bar` → `Mathlib/Foo/Bar.lean`. Non-file targets |
| 169 | + (those containing ':') return None.""" |
| 170 | + if ":" in target: |
| 171 | + return None |
| 172 | + return target.replace(".", "/") + ".lean" |
| 173 | + |
| 174 | + |
| 175 | +def parse_log(log_path: Path, out_path: Path) -> dict: |
| 176 | + """Parse `log_path` and write per-unfold JSONL records to `out_path`. |
| 177 | + Returns a summary dict.""" |
| 178 | + out_path.parent.mkdir(parents=True, exist_ok=True) |
| 179 | + |
| 180 | + current_file: str | None = None |
| 181 | + current_category: str | None = None |
| 182 | + records_written = 0 |
| 183 | + decls_seen: set[str] = set() |
| 184 | + files_seen: set[str] = set() |
| 185 | + |
| 186 | + with open(log_path) as log, open(out_path, "w") as out: |
| 187 | + for raw in log: |
| 188 | + line = raw.rstrip("\n") |
| 189 | + |
| 190 | + # 1. Update current-file context from the progress header. |
| 191 | + m = BUILT_RE.match(line) |
| 192 | + if m: |
| 193 | + current_file = target_to_file(m.group(1)) |
| 194 | + current_category = None |
| 195 | + continue |
| 196 | + |
| 197 | + # 2. Diagnostic subcategory header. |
| 198 | + m = CATEGORY_HEADER_RE.match(line) |
| 199 | + if m: |
| 200 | + tag, label = m.group(1), m.group(2) |
| 201 | + current_category = CATEGORY_SHORT.get((tag, label)) |
| 202 | + continue |
| 203 | + |
| 204 | + # 3. Entry line, only valid inside a known category and with a |
| 205 | + # known current file. |
| 206 | + m = ENTRY_RE.match(line) |
| 207 | + if m and current_category is not None and current_file is not None: |
| 208 | + tag, decl, count = m.group(1), m.group(2), int(m.group(3)) |
| 209 | + # The entry's tag should match the header's tag; if not, we |
| 210 | + # likely left the category silently. Reset and skip. |
| 211 | + if not current_category.startswith(tag): |
| 212 | + current_category = None |
| 213 | + continue |
| 214 | + record = { |
| 215 | + "file": current_file, |
| 216 | + "decl": decl, |
| 217 | + "count": count, |
| 218 | + "category": current_category, |
| 219 | + } |
| 220 | + out.write(json.dumps(record, separators=(",", ":")) + "\n") |
| 221 | + records_written += 1 |
| 222 | + decls_seen.add(decl) |
| 223 | + files_seen.add(current_file) |
| 224 | + continue |
| 225 | + |
| 226 | + # 4. Any other non-entry line ends a category block. |
| 227 | + if line and not line.startswith(" "): |
| 228 | + current_category = None |
| 229 | + |
| 230 | + return { |
| 231 | + "records": records_written, |
| 232 | + "unique_decls": len(decls_seen), |
| 233 | + "files_with_diagnostics": len(files_seen), |
| 234 | + } |
| 235 | + |
| 236 | + |
| 237 | +def main() -> int: |
| 238 | + ap = argparse.ArgumentParser(description=__doc__) |
| 239 | + ap.add_argument("--skip-build", action="store_true", |
| 240 | + help="don't run lake build; parse existing log only") |
| 241 | + ap.add_argument("--log", type=Path, default=DEFAULT_LOG, |
| 242 | + help=f"build log path (default: {DEFAULT_LOG})") |
| 243 | + ap.add_argument("--out", type=Path, default=DEFAULT_JSONL, |
| 244 | + help=f"output JSONL path (default: {DEFAULT_JSONL})") |
| 245 | + args = ap.parse_args() |
| 246 | + |
| 247 | + OUTPUT_DIR.mkdir(parents=True, exist_ok=True) |
| 248 | + |
| 249 | + rc = 0 |
| 250 | + if not args.skip_build: |
| 251 | + original = patch_lakefile() |
| 252 | + try: |
| 253 | + rc = run_build(args.log) |
| 254 | + finally: |
| 255 | + restore_lakefile(original) |
| 256 | + if rc != 0: |
| 257 | + print(f"[build_with_diagnostics] lake build exited {rc}; " |
| 258 | + f"log preserved at {args.log}. " |
| 259 | + f"Re-run with --skip-build --log to reparse.", |
| 260 | + file=sys.stderr) |
| 261 | + # Still parse: partial output is useful. |
| 262 | + |
| 263 | + if not args.log.exists(): |
| 264 | + print(f"error: log not found: {args.log}", file=sys.stderr) |
| 265 | + return 2 |
| 266 | + |
| 267 | + summary = parse_log(args.log, args.out) |
| 268 | + print(f"[build_with_diagnostics] wrote {summary['records']} records " |
| 269 | + f"({summary['unique_decls']} unique decls, " |
| 270 | + f"{summary['files_with_diagnostics']} files with diagnostics) " |
| 271 | + f"to {args.out}", file=sys.stderr) |
| 272 | + return rc |
| 273 | + |
| 274 | + |
| 275 | +if __name__ == "__main__": |
| 276 | + sys.exit(main()) |
0 commit comments