From 7ceda9b6b6a65b343531753c053703a65310f5cb Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 22:23:47 -0400 Subject: [PATCH 1/2] chore(scripts): retire the quality report, keeping the build-output reader and audit queries Delete scripts/quality_report.py's report and metrics: the per-area and per-directory tables, never-referenced shares, undocumented counts, module-doc drift counts, privatization candidates, hub fan-out, proof-length outliers, and the Markdown and JSON output. The Lean reader drops the docstring and same-module-use fields that only the report read. Keep what other tools use: - scripts/lean_outputs.py: build-output reading (Library, load_ileans, glob-built libraries, freshness checks, load_constants, Source, collect_declarations), read by the tidy ratchet, the tidy-usage report, tidy_sweep.py, check_changed_files.py and the audit queries; - scripts/LeanOutputs.lean: the renamed Lean reader; - scripts/audit_queries.py: on-demand `references` and `duplicates` queries for audits, never run in CI, printing declarations rather than counts. The tidy-usage report moves into check_tidy_usage.py, the doc-list parser into check_changed_files.py, #587's area table into tidy_sweep.py and transitive_importers into list_split_fanout.py, their only users. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- CONTRIBUTING.md | 7 +- .../{QualityReport.lean => LeanOutputs.lean} | 42 +- scripts/audit_queries.py | 363 +++++ scripts/check_changed_files.py | 45 +- scripts/check_tidy_surface.py | 12 +- scripts/check_tidy_usage.py | 211 ++- scripts/lean_outputs.py | 286 ++++ scripts/list_split_fanout.py | 23 +- scripts/quality_report.py | 1234 ----------------- scripts/test_audit_queries.py | 150 ++ scripts/test_check_changed_files.py | 24 + scripts/test_check_tidy_surface.py | 14 +- scripts/test_lean_outputs.py | 112 ++ scripts/test_list_split_fanout.py | 9 +- scripts/test_quality_report.py | 246 ---- scripts/test_tidy_sweep.py | 47 +- scripts/test_tidy_usage.py | 45 +- scripts/tidy_sweep.py | 127 +- 18 files changed, 1375 insertions(+), 1622 deletions(-) rename scripts/{QualityReport.lean => LeanOutputs.lean} (87%) create mode 100644 scripts/audit_queries.py create mode 100644 scripts/lean_outputs.py delete mode 100644 scripts/quality_report.py create mode 100644 scripts/test_audit_queries.py create mode 100644 scripts/test_lean_outputs.py delete mode 100644 scripts/test_quality_report.py diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 50524494cf..bb518ddd1a 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -91,9 +91,10 @@ also loads private information, so such edits do reach its clients. instances stay local. - Ordinary imports cannot name private declarations. When privatizing, update the tests and abstracts that name them in the same PR, or give a companion module `import all`. -- `scripts/quality_report.py` records where each declaration is referenced and where other modules - unfold a definition by name. Reduction by `rfl` or `decide` is not recorded, and its counts are - review signals, not rules. +- For an audit, `python3 scripts/audit_queries.py references PREFIX` lists where each declaration + under a source path is referenced, and `duplicates` lists declarations with alpha-equivalent + statements in different modules. Uses through `rfl`, `decide`, simp sets or instances leave no + reference. It is an on-demand helper, never run in CI. Tidy computability (`ComputableTidily…`, `ComputesTidily…`, `IsTidy…`) may appear anywhere inside proofs, through `.tidy`, `.of_tidy`, a proof-local `attribute [local fun_prop] … in` or a tidy diff --git a/scripts/QualityReport.lean b/scripts/LeanOutputs.lean similarity index 87% rename from scripts/QualityReport.lean rename to scripts/LeanOutputs.lean index 3fcc44182a..6af84a270c 100644 --- a/scripts/QualityReport.lean +++ b/scripts/LeanOutputs.lean @@ -7,9 +7,9 @@ Authors: Samuel Schlesinger import Lean /-! -# Declaration data for `scripts/quality_report.py` +# Declaration data for `scripts/lean_outputs.py` -Run as `lake env lean --run scripts/QualityReport.lean [] < modules.txt`, with one +Run as `lake env lean --run scripts/LeanOutputs.lean [] < modules.txt`, with one module name per line on standard input. For every module it reads the three parts of the built `.olean` (exported, server and private) without importing them, and prints one JSON line per constant: @@ -19,15 +19,12 @@ constant: `axiom`); `e`: its kind in the exported part, or `""` when it is not exported. Under the module system a public theorem is exported as an `axiom` (statement only), a definition whose body is not exposed as an `axiom`, and an exposed definition as a `def`; -* `doc`: whether it has a docstring (Markdown, Verso or `@[inherit_doc]`); * `tidy`: the constants named `ComputableTidily…`, `ComputesTidily…` or `IsTidy…` in its type; `tb`: for an exported definition, those in its exposed body outside proofs. Proofs are the subterms whose type is a proposition, together with the statements of proof-local `have`s (a `let` whose type is a proposition): tidy computability is allowed there (#456). Telling them apart needs types, so the modules of the definitions whose body mentions a tidy constant are imported (at the exported level) for this, and their rows are printed last; -* `u`: for an exported constant, the other constants of the same module that its exported - statement or exposed body mentions (these cannot become private while it stays public); * `r`: its declaration range `[line, column, endLine, endColumn, selLine, selColumn, selEndLine, selEndColumn]`, with 1-based lines and code-point columns, when one is recorded. @@ -40,7 +37,7 @@ the conclusion, with binder info `0` explicit, `1` implicit, `2` strict implicit flag `1` when the type is an application of a listed tidy predicate, `2` when it mentions a tidy constant otherwise, and `0` when it mentions none. -Run as `lake env lean --run scripts/QualityReport.lean --names ...`, it instead prints +Run as `lake env lean --run scripts/LeanOutputs.lean --names ...`, it instead prints every name the given modules and their transitive imports export (constants and `export` aliases), one per line, then a line `--tokens--` and the parser tokens they declare (global and scoped notations, syntax and macros), for the name resolution of `scripts/tidy_sweep.py`. @@ -52,7 +49,7 @@ whose types are alpha-equivalent (`k = "thm"`), or whose types and exposed bodie open Lean -namespace ComplexityScripts.QualityReport +namespace ComplexityScripts.LeanOutputs def kindOf : ConstantInfo → String | .defnInfo _ => "def" @@ -101,7 +98,7 @@ unsafe def tidyBodies (libDir : System.FilePath) (modules : Array Name) (names : if names.isEmpty then return {} initSearchPath (← findSysroot) [libDir] let env ← importModules (modules.map ({ module := · })) {} (level := .exported) - let ctx : Core.Context := { fileName := "", fileMap := default } + let ctx : Core.Context := { fileName := "", fileMap := default } let mut result : NameMap (Array String) := {} for n in names do let some (.defnInfo v) := env.find? n @@ -111,18 +108,6 @@ unsafe def tidyBodies (libDir : System.FilePath) (modules : Array Name) (names : result := result.insert n ((← found.get).toArray.map toString) return result -/-- The declarations named by entries of the extensions whose names end in one of `suffixes`. -Every such extension is a `MapDeclarationExtension`, whose entries are pairs headed by a name. -/ -unsafe def entryNames (entries : Array (Name × Array EnvExtensionEntry)) (suffixes : List String) : - NameSet := Id.run do - let mut names : NameSet := {} - for (ext, es) in entries do - if let .str _ s := ext then - if suffixes.contains s then - for e in es do - names := names.insert (unsafeCast e : Name × Unit).1 - return names - unsafe def declRanges (entries : Array (Name × Array EnvExtensionEntry)) : NameMap DeclarationRanges := Id.run do let mut ranges : NameMap DeclarationRanges := {} @@ -216,22 +201,13 @@ unsafe def run (libDir : System.FilePath) (pairs : Option String := none) : IO U let mut exported : Std.HashMap Name ConstantInfo := {} for c in exportedData.constants do exported := exported.insert c.name c - let docs := entryNames fullData.entries - ["docStringExt", "versoDocStringExt", "inheritDocStringExt"] let ranges := declRanges fullData.entries - let sameModule : NameSet := fullData.constNames.foldl (·.insert ·) {} for c in fullData.constants do let e := exported[c.name]? let tidy := c.type.getUsedConstants.filter isTidy |>.map (·.toString) - let uses := match e with - | some (.defnInfo v) => v.type.getUsedConstants ++ v.value.getUsedConstants - | some ec => ec.type.getUsedConstants - | none => #[] - let uses := uses.filter (fun n => n != c.name && sameModule.contains n) |>.toList.eraseDups let mut row : List (String × Json) := [ ("n", c.name.toString), ("m", mod), ("k", kindOf c), ("e", (e.map kindOf).getD ""), - ("doc", docs.contains c.name), ("tidy", toJson tidy), - ("u", toJson (uses.map (·.toString))), + ("tidy", toJson tidy), ("r", (ranges.find? c.name).map rangeJson |>.getD .null)] if pairs.isSome then if let some ec := e then @@ -306,10 +282,10 @@ unsafe def names (roots : List Name) : IO Unit := do for t in tokens do stdout.putStrLn t if regions.isEmpty then stdout.flush -end ComplexityScripts.QualityReport +end ComplexityScripts.LeanOutputs unsafe def main (args : List String) : IO Unit := if args.head? == some "--names" then - ComplexityScripts.QualityReport.names (args.drop 1 |>.map String.toName) + ComplexityScripts.LeanOutputs.names (args.drop 1 |>.map String.toName) else - ComplexityScripts.QualityReport.run (args.headD ".lake/build/lib/lean") args[1]? + ComplexityScripts.LeanOutputs.run (args.headD ".lake/build/lib/lean") args[1]? diff --git a/scripts/audit_queries.py b/scripts/audit_queries.py new file mode 100644 index 0000000000..128384d8ce --- /dev/null +++ b/scripts/audit_queries.py @@ -0,0 +1,363 @@ +#!/usr/bin/env python3 +"""On-demand queries for audits: where declarations are referenced, and duplicate statements. + +Usage: python3 scripts/audit_queries.py references [--unused] PREFIX... + python3 scripts/audit_queries.py duplicates [PREFIX...] + (either with [--build-dir DIR] [--no-build-check]) + +PREFIX is a repository-relative source path prefix, such as `Complexity/Computability/Circuit/`. + +* `references` lists each public declaration written under the prefixes with the other modules + that refer to it: library modules, tests and abstracts. `--unused` keeps only those no other + module refers to. Declarations with an attribute through which they are used without being + named (`simp`, `fun_prop`, `aesop`, instances, notation, …) are marked, since such uses leave + no reference; definitional unfolding by `rfl` or `decide` leaves none either. +* `duplicates` lists groups of declarations in different modules whose statements are + alpha-equivalent (theorems), or whose types and exposed bodies are (definitions), other than + deprecated aliases. With prefixes, only groups with a member under one of them. + +This is a tool for audits, such as finding a duplicate to delete or checking who uses an API +before changing it. It reads the build outputs through `scripts/lean_outputs.py`, refusing stale +ones unless `--no-build-check` is given. It is never run in CI and prints declarations to look at, +not counts: a declaration nobody refers to may still be wanted API. +""" + +from __future__ import annotations + +import argparse +import re +import sys +from collections import defaultdict +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +sys.path.insert(0, str(ROOT / "scripts")) +import lean_outputs as lo # noqa: E402 +from lean_outputs import ATTR_BLOCK, ATTRIBUTE_COMMAND, COMMAND_START, IDENT # noqa: E402 + +# Constants generated from a declaration; a reference to one counts as a reference to its owner. +GENERATED = { + "eq_def", "eq_unfold", "induct", "induct_unfolding", "mutual_induct", "fun_cases", + "fun_cases_unfolding", "rec", "recOn", "casesOn", "brecOn", "binductionOn", "below", "ibelow", + "noConfusion", "noConfusionType", "ctorIdx", "ctorElim", "ctorElimType", "toCtorIdx", "ofNat", + "ofNat_ctorIdx", "injEq", "inj", "sizeOf_spec", "mk", "congr_simp", "ext", "ext_iff", "elim", + "proxyType", "proxyTypeEquiv", "decEq", "repr", "go", +} +# Generated constants whose use unfolds the owner's body. +UNFOLDING = {"eq_def", "eq_unfold", "induct", "induct_unfolding", "mutual_induct", "fun_cases", + "fun_cases_unfolding"} +# Attributes through which a declaration can be used without being named. +IMPLICIT_ATTRS = { + "simp", "simps", "fun_prop", "aesop", "instance", "ext", "refl", "trans", "symm", "csimp", + "program_certificate", "fo_realize", "elab_as_elim", "induction_eliminator", + "cases_eliminator", "default_instance", "coe", "gcongr", "positivity", "norm_num", "bound", + "grind", "simproc", "congr", "mono", "continuity", "measurability", "app_unexpander", +} +KEYWORD = re.compile( + r"\b(theorem|lemma|def|abbrev|instance|structure|class|inductive|opaque|alias|axiom|" + r"irreducible_def)\b") +NOTATION_COMMAND = re.compile( + r"^(?:@\[[^\]\n]*\]\s*)?(?:(?:scoped|local)\s+)?" + r"(?:notation3?|infixl?|infixr|prefix|postfix|macro|macro_rules|syntax|elab|elab_rules)\b", + re.M) +UNFOLD_TACTIC = re.compile(r"\b(?:unfold|delta|unfold_let)\b(?:\s+[^\s;⟨(\[\],]+)*\s+$") +REWRITE_HEAD = re.compile( + r"\b(?:simp|simp_all|dsimp|simp_rw|rw|rwa|rewrite|erw|nth_rewrite|nth_rw|simpa|simp_arith|" + r"field_simp|norm_num|grind|unfold)\b[^\[\]\n]*$") +LIST_ELEMENT = re.compile(r"\s*(?:←|<-)?\s*") + + +# --- Pure helpers (unit-tested in scripts/test_audit_queries.py) -------------------------------- + +def owner_of(name: str, owners: dict[str, str]) -> str | None: + """The user declaration that `name` is, belongs to, or was generated from.""" + if name in owners: + return owners[name] + parts = name.split(".") + for i in range(len(parts) - 1, 0, -1): + if not (parts[i] in GENERATED or lo.is_internal(parts[i])): + return None + prefix = ".".join(parts[:i]) + if prefix in owners: + return owners[prefix] + return None + + +def unfolds_by_name(name: str, owner: str) -> bool: + """Whether referring to `name` unfolds the body of `owner` (an equation lemma, say).""" + if name == owner or not name.startswith(owner + "."): + return False + first = name[len(owner) + 1:].split(".")[0] + return first in UNFOLDING or re.fullmatch(r"eq_\d+", first) is not None + + +def utf16_index(line: str, column: int) -> int: + """The code-point index of a UTF-16 column, as LSP positions in `.ilean` files count.""" + if line.isascii(): + return column + units = 0 + for i, char in enumerate(line): + if units >= column: + return i + units += 2 if ord(char) > 0xFFFF else 1 + return len(line) + + +def unfolds_at(lines: list[str], line: int, index: int) -> bool: + """Whether the identifier at `lines[line][index]` (masked code) is an argument of `unfold` or + `delta`, or an element of the lemma list of a rewriting or simplifying tactic.""" + before = lines[line][:index] + if UNFOLD_TACTIC.search(before): + return True + text = "\n".join(lines[max(0, line - 8):line] + [before]) + depth, element = 0, None + for i in range(len(text) - 1, -1, -1): + char = text[i] + if char in ")]}⟩": + depth += 1 + elif char in "([{⟨": + if depth: + depth -= 1 + continue + if char != "[" or not LIST_ELEMENT.fullmatch(text[i + 1:] if element is None + else element): + return False + return REWRITE_HEAD.search(text[text.rfind("\n", 0, i) + 1:i]) is not None + elif char == "," and not depth and element is None: + element = text[i + 1:] + if not LIST_ELEMENT.fullmatch(element): + return False + return False + + +def split_top_level(text: str) -> list[str]: + items, depth, start = [], 0, 0 + for i, char in enumerate(text): + if char in "([{": + depth += 1 + elif char in ")]}": + depth -= 1 + elif char == "," and not depth: + items.append(text[start:i]) + start = i + 1 + items.append(text[start:]) + return [item.strip() for item in items if item.strip()] + + +def attribute_names(attrs: str) -> set[str]: + """Attribute names in the body of `@[…]` or `attribute […]`, without `local` ones.""" + names = set() + for item in split_top_level(attrs): + words = item.split() + if words[0] == "local": + continue + if words[0] == "scoped" and len(words) > 1: + words = words[1:] + names.add(words[0].rstrip("!?")) + return names + + +def header_info(header: str) -> tuple[str | None, set[str]]: + """The declaration keyword and attributes in a masked declaration header.""" + attrs = set() + for block in ATTR_BLOCK.findall(header): + attrs |= attribute_names(block) + keywords = KEYWORD.findall(ATTR_BLOCK.sub(" ", header)) + return (keywords[-1] if keywords else None), attrs + + +def matches(name: str, token: str) -> bool: + """Whether `token` denotes `name`: the name or one of its suffixes on a component boundary, + ignoring a private prefix.""" + plain = re.sub(r"^_private\.[^0-9]*\.0\.", "", name) + return plain == token or plain.endswith("." + token) + + +def command_spans(code: str, command: re.Pattern) -> list[tuple[int, int, str]]: + """`(start, end, header)` of each command matching `command`, up to the next command.""" + spans = [] + for match in command.finditer(code): + end = next((m.start() for m in COMMAND_START.finditer(code, match.end())), len(code)) + spans.append((match.start(), end, match[1] if command.groups else match[0])) + return spans + + +# --- Analysis ----------------------------------------------------------------------------------- + +def annotate_headers(lib: lo.Library, decls: dict[str, dict]) -> None: + """Declaration keywords and attributes, including `notation` for declarations named in + notation, macro and syntax commands, whose uses leave no references.""" + for decl in decls.values(): + keyword, attrs = None, set() + if decl["range"]: + line, col, _, _, sel_line, sel_col, sel_end_line, sel_end_col = decl["range"] + src = lib.source(decl["module"]) + keyword, attrs = header_info(src.span(line, col, sel_line, sel_col)) + if keyword is None: # the selection is the keyword, as for anonymous instances + keyword, attrs = header_info(src.span(line, col, sel_end_line, sel_end_col)) + decl["keyword"], decl["attrs"] = keyword, attrs + for decl in decls.values(): + if decl["role"] == "generated" and decl["parent"] in decls: + decls[decl["parent"]]["attrs"].add("simps") + by_last: dict[str, list[str]] = defaultdict(list) + for name in decls: + by_last[name.rsplit(".", 1)[-1]].append(name) + for module in lib.modules: + code = lib.source(module).code + for start, end, _ in command_spans(code, NOTATION_COMMAND): + for token in set(IDENT.findall(code, start, end)): + token = token.rstrip(".") + for name in by_last.get(token.rsplit(".", 1)[-1], ()): + if matches(name, token) and ("." in token or decls[name]["module"] == module): + decls[name]["attrs"].add("notation") + + +def collect_references(lib: lo.Library, decls: dict[str, dict], owners: dict[str, str]) -> None: + """Record, for each declaration, the other modules that refer to it, its uses inside its own + module, `attribute […]` commands there, and the library modules that unfold it by name.""" + attribute_spans = {m: [(start, end, attribute_names(attrs)) for start, end, attrs in + command_spans(lib.source(m).code, ATTRIBUTE_COMMAND)] + for m in lib.modules} + for module in lib.ileans: + if module in lo.ROOTS: + continue + role = lo.module_role(module) + for name, _, info in lib.references(module): + owner = owner_of(name, owners) + if owner not in decls or not info["usages"]: + continue + decl = decls[owner] + if module != decl["module"]: + decl[f"{role}_refs"].add(module) + if role == "lib" and decl["exported"] == "def": + src = lib.source(module) + if unfolds_by_name(name, owner) or any( + unfolds_at(src.lines, u[0], utf16_index(src.raw_lines[u[0]], u[1])) + for u in info["usages"]): + decl["unfolded_by"].add(module) + continue + for usage in info["usages"]: + if len(usage) == 5: + decl["local_uses"] += owner_of(usage[4], owners) != owner + continue + src = lib.source(module) + offset = src.offset(usage[0], utf16_index(src.raw_lines[usage[0]], usage[1])) + for start, end, attrs in attribute_spans[module]: + if start <= offset < end: + decl["attrs"] |= attrs + + +def classify(decls: dict[str, dict]) -> None: + """Where each declaration is referenced (`category`), what it is (`sort`), and the attributes + through which it can be used without being named (`implicit`).""" + for decl in decls.values(): + if decl["lib_refs"]: + category = "outside" + elif decl["test_refs"] or decl["abstract_refs"]: + category = "tests_only" + elif decl["local_uses"]: + category = "module_only" + else: + category = "unreferenced" + keyword = decl["keyword"] + if "deprecated" in decl["attrs"]: + sort = "deprecated" + elif keyword == "alias": + sort = "alias" + elif keyword == "instance" or "instance" in decl["attrs"]: + sort = "instance" + elif decl["kind"] == "thm": + sort = "theorem" + elif decl["kind"] == "induct" or keyword in ("structure", "class", "inductive"): + sort = "type" + else: + sort = "definition" + decl["category"], decl["sort"] = category, sort + decl["implicit"] = sorted(decl["attrs"] & (IMPLICIT_ATTRS | {"notation"})) + if sort == "instance" and "instance" not in decl["attrs"]: + decl["implicit"].append("instance") + + +def find_duplicates(lib: lo.Library, decls: dict[str, dict]) -> list[dict]: + """Groups of declarations, other than deprecated ones and aliases, in different modules.""" + duplicates = [] + for row in lib.duplicate_rows: + members = [(m, n) for m, n in row["dup"] if n in decls and decls[n]["role"] == "decl" + and decls[n]["sort"] not in ("deprecated", "alias")] + if len({m for m, _ in members}) > 1: + duplicates.append({"kind": row["k"], "members": sorted(members)}) + return duplicates + + +# --- Queries ------------------------------------------------------------------------------------ + +def location(decl: dict) -> str: + line = decl["range"][0] if decl["range"] else 0 + return f"Complexity/{decl['path']}:{line}" + + +def under(path: str, prefixes: list[str]) -> bool: + return not prefixes or path.startswith(tuple(prefixes)) + + +def reference_lines(decls: dict[str, dict], prefixes: list[str], unused: bool) -> list[str]: + """One line per public declaration under the prefixes: where it is referenced.""" + out = [] + selected = [d for d in decls.values() if d["role"] == "decl" + and under(f"Complexity/{d['path']}", prefixes) + and not (unused and d["category"] in ("outside", "tests_only"))] + for decl in sorted(selected, key=lambda d: (d["path"], d["range"] or [0])): + users = [f"{label} {', '.join(sorted(decl[key]))}" for label, key in + (("library", "lib_refs"), ("tests", "test_refs"), ("abstracts", "abstract_refs")) + if decl[key]] + where = "; ".join(users) or ("only its own module" if decl["local_uses"] else "nowhere") + implicit = f" [used implicitly through {', '.join(decl['implicit'])}?]" \ + if decl["implicit"] else "" + out.append(f"{location(decl)}: {decl['name']} ({decl['sort']}): {where}{implicit}") + return out + + +def duplicate_lines(groups: list[dict], decls: dict[str, dict], prefixes: list[str]) -> list[str]: + """One block per group of duplicates with a member under the prefixes.""" + out = [] + what = {"thm": "alpha-equivalent statements", "def": "alpha-equivalent types and bodies"} + for group in groups: + members = [decls[name] for _, name in group["members"]] + if not any(under(f"Complexity/{d['path']}", prefixes) for d in members): + continue + out.append(f"{what.get(group['kind'], group['kind'])}:") + out += [f" {location(d)}: {d['name']}" for d in members] + return out + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__, + formatter_class=argparse.RawDescriptionHelpFormatter) + parser.add_argument("query", choices=("references", "duplicates")) + parser.add_argument("prefixes", nargs="*", metavar="PREFIX", + help="repository-relative source path prefixes") + parser.add_argument("--unused", action="store_true", + help="with `references`, only declarations no other module refers to") + parser.add_argument("--build-dir", type=Path, default=lo.DEFAULT_BUILD_DIR) + parser.add_argument("--no-build-check", action="store_true", + help="do not check that the build outputs are current") + args = parser.parse_intermixed_args(argv) + if args.query == "references" and not args.prefixes: + parser.error("`references` needs at least one PREFIX") + if args.unused and args.query != "references": + parser.error("--unused applies to `references` only") + lo.check_outputs(args.build_dir, args.no_build_check) + lib = lo.Library(args.build_dir) + decls, owners = lo.collect_declarations(lib) + annotate_headers(lib, decls) + if args.query == "references": + collect_references(lib, decls, owners) + classify(decls) + lines = (reference_lines(decls, args.prefixes, args.unused) if args.query == "references" + else duplicate_lines(find_duplicates(lib, decls), decls, args.prefixes)) + print("\n".join(lines) if lines else "No matching declarations.") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/check_changed_files.py b/scripts/check_changed_files.py index 8bfd1058aa..cd248e9493 100644 --- a/scripts/check_changed_files.py +++ b/scripts/check_changed_files.py @@ -36,7 +36,7 @@ ROOT = Path(__file__).resolve().parents[1] sys.path.insert(0, str(ROOT / "scripts")) -import quality_report as qr # noqa: E402 +import lean_outputs as lo # noqa: E402 from proof_lengths import command_starts, masks, signature_end # noqa: E402 # Lean's identifiers (`Lean.isIdFirst`, `Lean.isIdRest`), with `«…»` escapes; dot-separated. @@ -95,6 +95,43 @@ def changed_files(root: Path, ref: str) -> tuple[list[str], list[str]]: # --- Module-doc names --------------------------------------------------------------------------- +MAIN_SECTION = re.compile(r"^##\s+Main\b", re.M) +BULLET = re.compile(r"^(\s*)[*-]\s+") +DOC_NAME = re.compile(r"@?[^\s`()\[\]{},;:]*[A-Za-z][^\s`()\[\]{},;:]*") + + +def doc_blocks(text: str) -> list[str]: + return re.findall(r"/-!(.*?)-/", text, re.S) + + +def listed_names(doc: str) -> list[str]: + """Names listed in the "Main …" sections of a module docstring: the backquoted names before + the first colon (outside backquotes) of each bullet.""" + names = [] + for section in re.split(r"^(?=#)", doc, flags=re.M): + if not MAIN_SECTION.match(section): + continue + items: list[str | None] = [] + for line in section.splitlines()[1:]: + if BULLET.match(line): + items.append(BULLET.sub("", line, count=1)) + elif items and items[-1] is not None and line.startswith(" ") and line.strip(): + items[-1] += " " + line.strip() + else: + items.append(None) + for item in filter(None, items): + head, inside = item, False + for i, char in enumerate(item): + if char == "`": + inside = not inside + elif char == ":" and not inside: + head = item[:i] + break + names += [token.lstrip("@.") for token in re.findall(r"`([^`]*)`", head) + if DOC_NAME.fullmatch(token)] + return names + + def syntax_names(text: str) -> set[str]: """Names of the tactics, attributes, rule sets and simp sets a source file declares.""" names = {atom.strip() for atom in SYNTAX_ATOM.findall(text)} @@ -128,7 +165,7 @@ def resolves(token: str, by_last: dict[str, set[str]]) -> bool: def listed_identifiers(text: str) -> list[str]: """The identifiers listed in the "Main …" sections of a source file's module docstrings.""" - return [token for doc in qr.doc_blocks(text) for token in qr.listed_names(doc) + return [token for doc in doc_blocks(text) for token in listed_names(doc) if NAME.fullmatch(token)] @@ -208,8 +245,8 @@ def main(argv: list[str] | None = None, root: Path = ROOT) -> int: if rel.startswith("Complexity/") and rel.endswith(".lean")] def load_ileans() -> dict[str, dict]: - qr.check_outputs(qr.DEFAULT_BUILD_DIR, args.no_build_check) - return qr.load_ileans(qr.DEFAULT_BUILD_DIR) + lo.check_outputs(lo.DEFAULT_BUILD_DIR, args.no_build_check) + return lo.load_ileans(lo.DEFAULT_BUILD_DIR) errors = check_new_tests(root, added) + check_doc_names(root, sorted(modules), load_ileans) for error in errors: diff --git a/scripts/check_tidy_surface.py b/scripts/check_tidy_surface.py index 8e3f095822..5c5fb1212c 100644 --- a/scripts/check_tidy_surface.py +++ b/scripts/check_tidy_surface.py @@ -20,7 +20,7 @@ statements is moved. Declarations written in source come from the `.ilean` files and statements from the `.olean` -files, read by `scripts/quality_report.py` and `scripts/QualityReport.lean`. The check needs the +files, read by `scripts/lean_outputs.py` and `scripts/LeanOutputs.lean`. The check needs the build outputs of `lake build Complexity ComplexityTests ComplexityAbstracts` (`lake build` and `lake test`), and refuses stale ones unless `--no-build-check` is given. """ @@ -35,7 +35,7 @@ ROOT = Path(__file__).resolve().parents[1] sys.path.insert(0, str(ROOT / "scripts")) -import quality_report as qr # noqa: E402 +import lean_outputs as lo # noqa: E402 ALLOWLIST = ROOT / "scripts/tidy_allowlist.txt" BASELINE = ROOT / "scripts/tidy_surface_baseline.json" @@ -50,11 +50,11 @@ def load_allowlist(path: Path) -> set[str]: return {line.split("#", 1)[0].strip() for line in path.read_text().splitlines()} - {""} -def tidy_statements(lib: qr.Library, allowlist: set[str]) -> dict[str, list[Statement]]: +def tidy_statements(lib: lo.Library, allowlist: set[str]) -> dict[str, list[Statement]]: """The tidy statements of each module outside the allowlist, by source path. Declarations written in source count, structure fields included; constants generated from them (`simps` lemmas, equation lemmas, recursors) do not.""" - decls, _, _ = qr.collect_declarations(lib) + decls, _ = lo.collect_declarations(lib) found: dict[str, list[Statement]] = defaultdict(list) for name, decl in decls.items(): if decl["role"] == "generated": @@ -118,8 +118,8 @@ def main(argv: list[str] | None = None) -> int: args = parser.parse_args(argv) if args.allow_increase and not args.update: parser.error("--allow-increase needs --update") - qr.check_outputs(qr.DEFAULT_BUILD_DIR, args.no_build_check) - found = tidy_statements(qr.Library(qr.DEFAULT_BUILD_DIR), load_allowlist(args.allowlist)) + lo.check_outputs(lo.DEFAULT_BUILD_DIR, args.no_build_check) + found = tidy_statements(lo.Library(lo.DEFAULT_BUILD_DIR), load_allowlist(args.allowlist)) counts = {path: len(rows) for path, rows in found.items()} baseline = load_baseline(args.baseline) if args.baseline.exists() else {} over, under = compare(counts, baseline) diff --git a/scripts/check_tidy_usage.py b/scripts/check_tidy_usage.py index d7ff29d227..bf52e18410 100644 --- a/scripts/check_tidy_usage.py +++ b/scripts/check_tidy_usage.py @@ -2,8 +2,9 @@ """Report proof-internal tidy usage outside a stated measurement boundary (#862). This never compares or writes a baseline, rejects a count, or changes S3's allowlist. It reuses -quality_report's declaration metadata, freshness checks and source masks. Counts are report-only; -the proposed Internal/** prefixes are measurement parameters, not approved exemptions. +the declaration metadata and freshness checks of `scripts/lean_outputs.py` and the source masks of +`scripts/proof_lengths.py`. Counts are report-only; the proposed Internal/** prefixes are +measurement parameters, not approved exemptions. Usage: python3 scripts/check_tidy_usage.py --json /tmp/tidy-usage.json To reproduce the issue's older broad Machines measurement boundary, pass @@ -15,10 +16,204 @@ from __future__ import annotations import argparse +import hashlib import json +import re +import sys +from collections import Counter, defaultdict from pathlib import Path -import quality_report as qr +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from lean_outputs import ( # noqa: E402 + ATTR_BLOCK, ATTRIBUTE_COMMAND, COMMAND_START, DEFAULT_BUILD_DIR, GLOB_ROOTS, IDENT, ROOT, ROOTS, + Library, check_outputs, collect_declarations, is_internal, load_constants, module_role, run, + source_path, +) +from proof_lengths import masks # noqa: E402 + + +# Report-only S4 measurement. These prefixes describe the proposed target, not an exemption +# from S3 or an assertion that the boundary migration has already happened. +TIDY_INTERNAL_PREFIXES = ( + "Complexity/Computability/Machines/Turing/MultiTape/Internal/", + "ComplexityTests/Machines/Turing/MultiTape/Internal/", +) +BRIDGE_TOKEN = re.compile(r"\.(?:tidy|of_tidy)(?![\w'!?])") +LOCAL_FUN_PROP = re.compile(r"(?:^|,)\s*local\s+fun_prop\s*(?:,|$)") + + +def tidy_source_signals(text: str, tidy_names: set[str], known_names: set[str] | None = None + ) -> dict: + """Lexical bridge occurrences and local registrations of known tidy-typed constants. + + Reuse the comment/string/character masks and attribute parser. Name suffix matching is + conservative: an ambiguous suffix counts if any candidate has a tidy type. Unresolved + local registrations are retained for review, not silently called plain. This does not + expand macros, resolve local notation, or count semantic pairs of bridge applications. + """ + code = masks(text)[1] + bridges = [{"line": code.count("\n", 0, m.start()) + 1, + "bridge": m[0][1:]} for m in BRIDGE_TOKEN.finditer(code)] + local, unresolved = [], [] + blocks = [(m, False) for m in ATTR_BLOCK.finditer(code)] + blocks += [(m, True) for m in ATTRIBUTE_COMMAND.finditer(code)] + for block, command in sorted(blocks, key=lambda x: x[0].start()): + if not LOCAL_FUN_PROP.search(block[1]): + continue + after = code[block.end():] + # An attribute command names one or more targets; an inline attribute precedes a decl. + if command: + following = next(COMMAND_START.finditer(code, block.end()), None) + target_text = code[block.end():following.start() if following else len(code)] + targets = IDENT.findall(target_text) + targets = targets[:targets.index("in")] if "in" in targets else targets + else: + decl = re.match(r"\s*(?:(?:public|private|protected|noncomputable|unsafe|partial|" + r"nonrec|meta)\s+)*(?:theorem|lemma|def|abbrev|instance|opaque)\s+", + after) + target = IDENT.match(after, decl.end()) if decl else None + targets = [target[0]] if target else [] + line = code.count("\n", 0, block.start()) + 1 + if not targets: + unresolved.append({"line": line, "target": None}) + for target in targets: + row = {"line": line, "target": target} + candidates = [n for n in tidy_names if n == target or n.endswith("." + target)] + if candidates: + local.append({**row, "candidates": sorted(candidates)}) + elif target not in (known_names or set()): + unresolved.append(row) + return {"bridges": bridges, "local_tidy_fun_prop": local, + "unresolved_local_fun_prop": unresolved} + + +def private_tidy_declarations(constants: dict[str, dict], source) -> dict[str, list[dict]]: + """Private source declarations with tidy in their type, excluding generated children.""" + found: dict[str, list[dict]] = defaultdict(list) + by_range: dict[tuple, set[str]] = defaultdict(set) + for name, c in constants.items(): + if c["r"]: + by_range[c["m"], tuple(c["r"])].add(name) + for name, c in constants.items(): + if not (name.startswith("_private.") and c["tidy"] and c["r"]): + continue + r = c["r"] + selected = source(c["m"]).span(*r[4:]).strip() + # An authored anonymous instance selects the keyword, not its auto-generated name. + # Its auxiliary constants can inherit that same range; retain only the source owner, + # considering *all* types so a plain owner cannot leave a tidy generated child behind. + anonymous_instance = selected == "instance" and not is_internal(name.rsplit(".", 1)[-1]) \ + and not any(name.startswith(other + ".") for other in by_range[c["m"], tuple(r)] + if other != name) + if selected and (name.endswith("." + selected) or anonymous_instance): + found[c["m"]].append({"name": name, "line": r[4], "mentions": c["tidy"]}) + return found + + +def tidy_usage_report(lib: Library, prefixes: tuple[str, ...] = TIDY_INTERNAL_PREFIXES) -> dict: + """Per-module report of the S4 boundary, with no baseline comparison or enforcement. + + Public statement counts use exactly S3's source-declaration/type rule. Private counts + require a source declaration range and a tidy constant in its elaborated type; generated + constants sharing the owner's range are excluded by matching the selected source name. + Tests/abstracts use their own metadata. Guide files have source-only signals and explicitly + unknown statement counts, since the root build does not elaborate the separate guide. + """ + modules = sorted(m for m in lib.ileans if m.startswith( + ("Complexity.", "ComplexityTests.", "ComplexityAbstracts."))) + extra = [m for m in modules if m not in lib.modules] + constants = dict(lib.constants) + if extra: + more, _ = load_constants(lib.build_dir, extra) + constants.update(more) + tidy_names = {n for n, c in constants.items() if c["tidy"]} + # Known suffixes distinguish resolved plain targets from unknown ones without rescanning + # the entire constant inventory for every source attribute. + known_suffixes = {".".join(parts[i:]) for n in constants + for parts in [n.split(".")] for i in range(len(parts))} + public_tidy_names = {n for n in tidy_names if not n.startswith("_private.")} + private_tidy_names: dict[str, set[str]] = defaultdict(set) + for n in tidy_names - public_tidy_names: + private_tidy_names[constants[n]["m"]].add(n) + public, _ = collect_declarations(lib) + public_by_module = Counter(d["module"] for n, d in public.items() + if d["role"] != "generated" and + (constants[n]["tidy"] or constants[n].get("tb"))) + private_by_module = private_tidy_declarations(constants, lib.source) + rows = [] + sources = [(m, source_path(m), True) for m in modules] + sources += [(str(p.relative_to(ROOT)), p, False) for p in sorted( + (ROOT / "guide").rglob("*.lean")) if ".lake" not in p.parts] + for module, path, metadata in sources: + rel = path.relative_to(ROOT).as_posix() + if any(rel.startswith(p) for p in prefixes): + continue + text = path.read_text() + signals = tidy_source_signals(text, + public_tidy_names | private_tidy_names[module], + known_suffixes) + private = private_by_module[module] if metadata else None + counts = {"public_tidy_statements": public_by_module[module] + if module.startswith("Complexity.") else None, + "private_tidy_declarations": len(private) if metadata else None, + "local_tidy_fun_prop": len(signals["local_tidy_fun_prop"]), + "bridge_occurrences": len(signals["bridges"])} + rows.append({"module": module, "path": rel, + "role": module_role(module) if metadata else "guide", "counts": counts, + "mentions_tidy": bool(re.search(r"Tidily|IsTidy|\.(?:of_)?tidy\b", + masks(text)[1])), + "private_tidy_declarations": private, **signals}) + keys = ("public_tidy_statements", "private_tidy_declarations", + "local_tidy_fun_prop", "bridge_occurrences") + source_hash = hashlib.sha256() + for path in ([source_path(root) for root in ROOTS if root not in GLOB_ROOTS] + + [p for _, p, _ in sources]): + source_hash.update(path.relative_to(ROOT).as_posix().encode() + b"\0") + source_hash.update(path.read_bytes() + b"\0") + provenance = {"revision": run(["git", "rev-parse", "HEAD"], capture_output=True).stdout.strip(), + "tree": run(["git", "rev-parse", "HEAD^{tree}"], capture_output=True).stdout.strip(), + "dirty": bool(run(["git", "status", "--porcelain"], + capture_output=True).stdout.strip()), + "source_dirty": bool(run(["git", "status", "--porcelain", "--", + "Complexity", "ComplexityTests", "abstracts", "guide", + "Complexity.lean"], + capture_output=True).stdout.strip()), + "scanned_source_sha256": source_hash.hexdigest(), + "scanned_files": len(sources), "build_dir": str(lib.build_dir)} + return {"provenance": provenance, "internal_prefixes": list(prefixes), "report_only": True, + "totals": {k: sum(r["counts"][k] or 0 for r in rows) for k in keys}, + "files_mentioning_tidy": sum(r["mentions_tidy"] for r in rows), + "modules": rows, + "notes": ["The prefixes are a proposed measurement boundary, not S3 exemptions.", + "Public counts use S3's declaration/type rule only for library modules, but " + "this report's stated boundary replaces S3's allowlist. Null is not zero.", + "Private counts inspect elaborated types, not names or proof bodies; generated " + "constants are excluded by source selection. Type aliases are not unfolded. " + "Guide metadata is unavailable.", + "Bridge counts are lexical occurrences, not semantic round-trip pairs; comments " + "and literals are masked. Other named erasure APIs are not included.", + "Local registration targets use conservative suffix matching, without elaborated " + "name resolution; unresolved targets are listed, not assumed plain."]} + + +def tidy_usage_markdown(report: dict, top: int = 20) -> str: + """Human view of the same report-only per-module data, with full detail in JSON.""" + out = ["### Proof-internal tidy usage (S4, report only)", "", + "Measurement excludes: " + ", ".join(f"`{p}`" for p in report["internal_prefixes"]), + "", "| Module | Public tidy statements | Private tidy declarations | Local tidy " + "fun_prop targets | Bridge occurrences |", "|---|---:|---:|---:|---:|"] + rows = sorted(report["modules"], key=lambda r: ( + -sum(v or 0 for v in r["counts"].values()), r["path"])) + for row in [r for r in rows if any(r["counts"].values())][:top]: + values = ["unknown" if v is None else str(v) for v in row["counts"].values()] + out.append(f"| `{row['path']}` | " + " | ".join(values) + " |") + out += ["| Total (known counts) | " + " | ".join(map(str, report["totals"].values())) + " |", + "", f"{report['files_mentioning_tidy']} files mention tidy outside the measurement " + "boundary. Full per-module locations and unresolved targets are in the JSON report.", + "", *["- " + note for note in report["notes"]]] + return "\n".join(out) + "\n" + + def main(argv: list[str] | None = None) -> int: @@ -26,21 +221,21 @@ def main(argv: list[str] | None = None) -> int: parser.add_argument("--json", type=Path, help="write every module and occurrence") parser.add_argument("--markdown", type=Path, help="write the human-readable summary") parser.add_argument("--top", type=int, default=20) - parser.add_argument("--build-dir", type=Path, default=qr.DEFAULT_BUILD_DIR) + parser.add_argument("--build-dir", type=Path, default=DEFAULT_BUILD_DIR) parser.add_argument("--no-build-check", action="store_true", help="label outputs unchecked instead of requiring source freshness") parser.add_argument("--internal-prefix", action="append", help="replace default prefixes with these repo-relative directories; " "repeat for multiple directories (measurement only)") args = parser.parse_args(argv) - prefixes = tuple(args.internal_prefix or qr.TIDY_INTERNAL_PREFIXES) + prefixes = tuple(args.internal_prefix or TIDY_INTERNAL_PREFIXES) if any(not p.endswith("/") or p.startswith("/") or ".." in Path(p).parts for p in prefixes): parser.error("internal prefixes must be repo-relative directories ending in /") - outputs = qr.check_outputs(args.build_dir, args.no_build_check) - report = qr.tidy_usage_report(qr.Library(args.build_dir), prefixes) + outputs = check_outputs(args.build_dir, args.no_build_check) + report = tidy_usage_report(Library(args.build_dir), prefixes) report["provenance"]["outputs"] = outputs text = (f"Revision `{report['provenance']['revision']}`; outputs {outputs}.\n\n" - + qr.tidy_usage_markdown(report, args.top)) + + tidy_usage_markdown(report, args.top)) if args.json: args.json.write_text(json.dumps(report, indent=1, ensure_ascii=False) + "\n") if args.markdown: diff --git a/scripts/lean_outputs.py b/scripts/lean_outputs.py new file mode 100644 index 0000000000..d51e9f4dbf --- /dev/null +++ b/scripts/lean_outputs.py @@ -0,0 +1,286 @@ +#!/usr/bin/env python3 +"""Read the build outputs of the three libraries, and the sources they come from. + +`lake build Complexity ComplexityTests ComplexityAbstracts` (`lake build` and `lake test`) writes +an `.ilean` file beside each `.olean`. It records every identifier that occurs in the module's +source, including in proofs, with the declarations the module defines. `scripts/LeanOutputs.lean` +reads the `.olean` parts for each constant's kind, export status, statement and declaration range. +This module loads both and refuses stale outputs. `scripts/check_tidy_surface.py`, +`scripts/check_tidy_usage.py`, `scripts/tidy_sweep.py`, `scripts/check_changed_files.py` and +`scripts/audit_queries.py` build on it. +""" + +from __future__ import annotations + +import filecmp +import json +import re +import subprocess +import sys +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +sys.path.insert(0, str(ROOT / "scripts")) +from proof_lengths import masks # noqa: E402 + +ROOTS = ("Complexity", "ComplexityTests", "ComplexityAbstracts") +# Libraries that Lake builds from a glob (`lakefile.toml`) have no root aggregator file: their +# modules are exactly the source files under their directory. +GLOB_ROOTS = ("ComplexityTests",) +DEFAULT_BUILD_DIR = ROOT / ".lake/build/lib/lean" +# The build outputs read here. +OUTPUT_SUFFIXES = (".ilean", ".olean", ".olean.server", ".olean.private") + +# Lean source syntax shared by the tools that read declarations. +ATTR_BLOCK = re.compile(r"@\[((?:[^\[\]]|\[(?:[^\[\]]|\[[^\[\]]*\])*\])*)\]") +ATTRIBUTE_COMMAND = re.compile( + r"^attribute\s*\[((?:[^\[\]]|\[(?:[^\[\]]|\[[^\[\]]*\])*\])*)\]", re.M) +COMMAND_START = re.compile( + r"^(?:@\[|/--|/-!|#|(?:(?:public|private|protected|noncomputable|unsafe|partial|nonrec|" + r"scoped|local|meta)\s+)*(?:theorem|lemma|def|abbrev|opaque|axiom|instance|structure|class|" + r"inductive|example|namespace|section|end|open|universe|variable|include|omit|attribute|" + r"set_option|syntax|macro|macro_rules|elab|elab_rules|notation|notation3|infixl|infixr|infix|" + r"prefix|postfix|initialize|mutual|export|alias|register_simp_attr|declare_aesop_rule_sets|" + r"add_decl_doc|deriving)\b)", re.M) +IDENT = re.compile(r"[A-Za-z_À-ɏͰ-Ͽᴀ-ᶿ℀-⅏]" + r"[\w'!?₀-ₜᵢ-ᵪ.]*") + + +def glob_modules(root: str) -> list[str]: + """The modules of a glob-built library, from its source files.""" + return sorted(".".join(p.relative_to(ROOT).with_suffix("").parts) + for p in (ROOT / root).rglob("*.lean")) + + +def root_modules(glob=glob_modules) -> list[str]: + """Modules whose imports cover all three libraries: the aggregator roots and every module + of a glob-built library.""" + return [m for root in ROOTS + for m in (glob(root) if root in GLOB_ROOTS else [root])] + + +def module_role(module: str) -> str: + """`lib`, `test` or `abstract` for a module of one of the three libraries.""" + if module.startswith("ComplexityAbstracts.") or module.startswith("ComplexityTests.Abstracts."): + return "abstract" + if module.startswith("ComplexityTests."): + return "test" + return "lib" + + +def source_path(module: str) -> Path: + rel = module.replace(".", "/") + ".lean" + return ROOT / ("abstracts/" + rel if module.startswith("ComplexityAbstracts") else rel) + + +def is_internal(component: str) -> bool: + """Whether a name component is one Lean generates, such as `_proof_1` or `match_2`.""" + return (component.startswith("_") or component.isdigit() + or re.fullmatch(r"(?:eq|match|proof|omega)_[\d_]+", component) is not None) + + +def run(cmd: list[str], **kwargs) -> subprocess.CompletedProcess: + return subprocess.run(cmd, cwd=ROOT, text=True, check=True, **kwargs) + + +# --- Freshness ---------------------------------------------------------------------------------- + +def lake_outputs_current() -> bool: + """Whether Lake finds the default build outputs of the three libraries current.""" + return subprocess.run(["lake", "build", "--no-build", *ROOTS], cwd=ROOT, + capture_output=True).returncode == 0 + + +def output_differences(build_dir: Path, reference: Path) -> list[str]: + """Report inputs that are missing, extra or different in `build_dir` compared to + `reference`, as paths relative to them.""" + def inputs(directory: Path) -> set[Path]: + # The roots' own outputs (`Complexity.ilean`, …) sit beside their directories, and the + # module inventory comes from their imports. + files = [p for root in ROOTS + for p in [*(directory / root).rglob("*"), *directory.glob(f"{root}.*")]] + return {p.relative_to(directory) for p in files + if p.name.endswith(OUTPUT_SUFFIXES) and p.is_file()} + ours, theirs = inputs(build_dir), inputs(reference) + changed = {p for p in ours & theirs + if not filecmp.cmp(build_dir / p, reference / p, shallow=False)} + return sorted(map(str, (ours ^ theirs) | changed)) + + +def check_outputs(build_dir: Path, skip: bool, current=lake_outputs_current, + reference: Path = DEFAULT_BUILD_DIR) -> str: + """How the build outputs were checked, or exit when they are not current. + + Lake checks only the default build directory, so another directory must hold exactly the + same outputs as the checked default ones.""" + if skip: + return "not checked against the sources" + if not current(): + sys.exit("build outputs are missing or stale; run `lake build " + " ".join(ROOTS) + + "` (or pass --no-build-check)") + if build_dir.resolve() == reference.resolve(): + return "checked current by `lake build --no-build`" + differences = output_differences(build_dir, reference) + if differences: + sys.exit(f"{build_dir} differs from the current build outputs in {len(differences)} " + f"file(s) (e.g. {', '.join(differences[:3])}); pass --no-build-check to " + "use it anyway") + return "checked identical to the current outputs of `lake build --no-build`" + + +# --- Loading ------------------------------------------------------------------------------------ + +ROOT_IMPORT = re.compile(r"^(?:public\s+)?(?:meta\s+)?import\s+(\S+)", re.M) + + +def listed_modules(text: str) -> list[str]: + """The modules a root source file imports.""" + return ROOT_IMPORT.findall(text) + + +def load_ileans(build_dir: Path, missing: list[str] | None = None, + glob=glob_modules) -> dict[str, dict]: + """The `.ilean` data of the modules the three libraries' roots import, by module name. + + A long-lived build directory keeps the outputs of modules that were since deleted or moved, + and `lake build --no-build` does not notice them, so modules are found by following imports + from the roots rather than by listing files. A glob-built library (`GLOB_ROOTS`) has no root + file, so its source files are the starting points instead. Every starting point and every + module they import must have one; a missing file means the build is incomplete. The aggregator + roots themselves are left out. + + Given a list `missing`, the build may be partial instead (for a tree that does not build + completely): the modules are those the roots' source files import, and the ones without an + `.ilean` file are appended to `missing`.""" + if missing is not None: + ileans = {} + for root in ROOTS: + modules = (glob(root) if root in GLOB_ROOTS + else listed_modules(source_path(root).read_text())) + for module in modules: + path = build_dir / (module.replace(".", "/") + ".ilean") + if path.is_file(): + ileans[module] = json.loads(path.read_text()) + else: + missing.append(module) + return ileans + ileans, todo = {}, [(module, None) for module in root_modules(glob)] + while todo: + module, importer = todo.pop() + if module in ileans: + continue + path = build_dir / (module.replace(".", "/") + ".ilean") + if not path.is_file(): + sys.exit(f"{path} is missing ({'imported by ' + importer if importer else 'a root'}); " + "run `lake build " + " ".join(ROOTS) + "` first") + ileans[module] = json.loads(path.read_text()) + todo.extend((i[0], module) for i in ileans[module]["directImports"] + if i[0].split(".")[0] in ROOTS) + for root in ROOTS: + if root not in GLOB_ROOTS: + del ileans[root] + return ileans + + +def load_constants(build_dir: Path, modules: list[str], pairs: str | None = None + ) -> tuple[dict[str, dict], list[dict]]: + """Constants of `modules`, and the groups of constants with alpha-equivalent statements; + `pairs` (`tidy=plain,…`) adds the fields that `scripts/tidy_sweep.py` reads (see + `scripts/LeanOutputs.lean`).""" + out = run(["lake", "env", "lean", "--run", "scripts/LeanOutputs.lean", str(build_dir)] + + ([pairs] if pairs else []), + input="\n".join(modules) + "\n", capture_output=True).stdout + constants, duplicates = {}, [] + for line in out.splitlines(): + row = json.loads(line) + if "dup" in row: + duplicates.append(row) + else: + constants[row["n"]] = row + return constants, duplicates + + +class Source: + """A source file with its masked code split into lines.""" + + def __init__(self, path: Path): + self.text = path.read_text(encoding="utf-8") + self.code = masks(self.text)[0] + self.raw_lines = self.text.split("\n") + self.lines = self.code.split("\n") + self.starts = [0] + for raw in self.raw_lines: + self.starts.append(self.starts[-1] + len(raw) + 1) + + def span(self, line: int, col: int, end_line: int, end_col: int) -> str: + """Masked code between 1-based lines and code-point columns.""" + if line == end_line: + return self.lines[line - 1][col:end_col] + return "\n".join([self.lines[line - 1][col:]] + self.lines[line:end_line - 1] + + [self.lines[end_line - 1][:end_col]]) + + def offset(self, line0: int, index: int) -> int: + return self.starts[line0] + index + + +class Library: + """Build outputs and sources of the three libraries, loaded lazily where possible.""" + + def __init__(self, build_dir: Path, pairs: str | None = None, + missing: list[str] | None = None): + self.build_dir = build_dir + self.ileans = load_ileans(build_dir, missing) + self.modules = sorted(m for m in self.ileans if m.startswith("Complexity.")) + self.constants, self.duplicate_rows = load_constants(build_dir, self.modules, pairs) + self.sources: dict[str, Source] = {} + + def source(self, module: str) -> Source: + if module not in self.sources: + self.sources[module] = Source(source_path(module)) + return self.sources[module] + + def references(self, module: str): + """`(name, defining module, info)` for each constant referenced in `module`.""" + for key, info in self.ileans[module]["references"].items(): + ident = json.loads(key).get("c") + if ident: + yield ident["n"], ident["m"], info + + +def collect_declarations(lib: Library) -> tuple[dict[str, dict], dict[str, str]]: + """Public declarations written in library sources (the binders recorded in `.ilean` files), + and the owner of every such name: a structure for its fields and constructors, a definition + for the lemmas `@[simps]` generates, and the declaration itself otherwise.""" + decls: dict[str, dict] = {} + owners: dict[str, str] = {} + for module in lib.modules: + rel = module.removeprefix("Complexity.").replace(".", "/") + ".lean" + for name, defined_in, info in lib.references(module): + if defined_in != module or not info["definition"]: + continue + if name.startswith("_private."): + owners[name] = name + continue + const = lib.constants.get(name) + if not const or not const["e"]: + continue + parent = info["definition"][4] if len(info["definition"]) == 5 else None + role = "decl" + if const["k"] == "ctor": + role = "member" + elif parent and parent != name: + if not name.startswith(parent + "."): + role = "generated" + elif lib.constants.get(parent, {}).get("k") == "induct": + role = "member" + decls[name] = { + "name": name, "module": module, "path": rel, + "role": role, "kind": const["k"], "exported": const["e"], + "tidy": const["tidy"], "range": const["r"], "parent": parent, + "lib_refs": set(), "test_refs": set(), "abstract_refs": set(), "local_uses": 0, + "unfolded_by": set(), + } + for name, decl in decls.items(): + owned = decl["role"] != "decl" and decl["parent"] in decls + owners[name] = decl["parent"] if owned else name + return decls, owners diff --git a/scripts/list_split_fanout.py b/scripts/list_split_fanout.py index 5753b35b59..9208bd6372 100644 --- a/scripts/list_split_fanout.py +++ b/scripts/list_split_fanout.py @@ -1,18 +1,18 @@ #!/usr/bin/env python3 """Compare #573's list-topic transitive importers over the base's fixed library universe. -Uses the existing native Lean header parser and shared quality-report graph calculation. -Counts source-import reach, not actual rebuilds, cache hits or elapsed build time. +Uses the existing native Lean header parser. Counts source-import reach, not actual rebuilds, +cache hits or elapsed build time. """ import argparse +from collections import defaultdict import io from pathlib import Path import subprocess import tarfile import tempfile -from quality_report import transitive_importers from quick_check import imports_from_lean ROOT = Path(__file__).resolve().parents[1] @@ -20,6 +20,23 @@ TOPICS = ("Append", "Counting", "Fold", "Lookup") +def transitive_importers(imports: dict[str, list[tuple[str, bool]]]) -> dict[str, set[str]]: + importers: dict[str, set[str]] = defaultdict(set) + for module, deps in imports.items(): + for dep, _ in deps: + importers[dep].add(module) + result = {} + for module in imports: + seen, stack = set(), [module] + while stack: + for importer in importers[stack.pop()]: + if importer not in seen: + seen.add(importer) + stack.append(importer) + result[module] = seen + return result + + def snapshot(ref: str, destination: Path) -> dict[str, list[tuple[str, bool]]]: archive = subprocess.check_output(["git", "archive", ref, "Complexity"], cwd=ROOT) sources = {} diff --git a/scripts/quality_report.py b/scripts/quality_report.py deleted file mode 100644 index 63fe5e80e4..0000000000 --- a/scripts/quality_report.py +++ /dev/null @@ -1,1234 +0,0 @@ -#!/usr/bin/env python3 -"""Report review signals for the library's public surface, statements, docs, placement and proofs. - -Usage: python3 scripts/quality_report.py [--json OUTPUT] [--markdown OUTPUT] [--top N] - [--build-dir DIR] [--no-build-check] - -Reads the build outputs of `lake build Complexity ComplexityTests ComplexityAbstracts` (it refuses -stale outputs unless `--no-build-check` is given) and reports, per area of the quality program -(#587) and per top-level directory: - -* where public declarations are referenced: by other library modules, only by tests or - abstracts, or never outside their own module; -* exposed definition bodies with no evidence of being unfolded by another library module; -* tidy predicates (`ComputableTidily…`) in public statements, outside the machine combinators; -* public definitions, and theorems listed in module docstrings or used by abstracts, without - docstrings; -* drift between module docstrings' "Main definitions/results" and the public API; -* declarations in different modules with alpha-equivalent statements (or definitions with - alpha-equivalent types and bodies); -* hub fan-out: transitive importers of each module; -* proof-length outliers, measured by `scripts/proof_lengths.py`. - -References come from the `.ilean` files Lake writes beside each `.olean`; they record every -identifier that occurs in the source, including in proofs. Declarations, kinds, export status, -docstrings, statement types and declaration ranges come from the `.olean` parts, read by -`scripts/QualityReport.lean`. These are review signals, not rules: an identifier that is only -used implicitly (simp sets, instances, `fun_prop`, Aesop rules, notation, macros) leaves no -reference, and zero in-repository references does not mean an API is unwanted. -""" - -from __future__ import annotations - -import argparse -import datetime -import filecmp -import hashlib -import json -import re -import subprocess -import sys -from collections import Counter, defaultdict -from pathlib import Path - -ROOT = Path(__file__).resolve().parents[1] -sys.path.insert(0, str(ROOT / "scripts")) -from proof_lengths import masks, scan as scan_proofs # noqa: E402 - -ROOTS = ("Complexity", "ComplexityTests", "ComplexityAbstracts") -# Libraries that Lake builds from a glob (`lakefile.toml`) have no root aggregator file: their -# modules are exactly the source files under their directory. -GLOB_ROOTS = ("ComplexityTests",) - - -def glob_modules(root: str) -> list[str]: - """The modules of a glob-built library, from its source files.""" - return sorted(".".join(p.relative_to(ROOT).with_suffix("").parts) - for p in (ROOT / root).rglob("*.lean")) - - -def root_modules(glob=glob_modules) -> list[str]: - """Modules whose imports cover all three libraries: the aggregator roots and every module - of a glob-built library.""" - return [m for root in ROOTS - for m in (glob(root) if root in GLOB_ROOTS else [root])] -# Documents outside module docstrings whose backquoted names count as intended API. -EXTERNAL_DOCS = ("README.md", "abstracts/README.md") -# The areas of #587: its table, completed by its assignment of the remaining paths -# (https://github.com/cslib-community/complexitylib/issues/587#issuecomment-6376302681). -AREAS = [ - ("Foundations", "Foundations, Probability, Languages, Computability/BitString", - ("Foundations/", "Probability/", "Languages/", "Computability/BitString/")), - ("Machines", "Computability/Machines, Probabilistic, RAM, GenericRAM; Tactic", - ("Computability/Machines/", "Computability/Probabilistic/", "Computability/RAM/", - "Computability/GenericRAM/", "Tactic/")), - ("Classes", "Computability/Complexity, PCP, Communication, DecisionTree, QueryComplexity, " - "TreeEval, Kolmogorov, MCSP, USTCON, Languages; MachineLearning", - ("Computability/Complexity/", "Computability/PCP/", "Computability/Communication/", - "Computability/DecisionTree/", "Computability/QueryComplexity/", "Computability/TreeEval/", - "Computability/Kolmogorov/", "Computability/MCSP/", "Computability/USTCON/", - "Computability/Languages/", "MachineLearning/")), - ("Circuit", "Computability/Circuit, BranchingProgram", - ("Computability/Circuit/", "Computability/BranchingProgram/")), - ("Crypto", "Crypto", ("Crypto/",)), - ("Logics", "Logics", ("Logics/",)), - ("WordRAM", "Computability/WordRAM, Algorithms", ("Computability/WordRAM/", "Algorithms/")), -] -OTHER_AREA = "Other" # `Init.lean`, held jointly by the program leads, and unassigned paths -TIDY_EXEMPT = "Computability/Machines/Turing/MultiTape/Combinators/" - -# Constants generated from a declaration; a reference to one counts as a reference to its owner. -GENERATED = { - "eq_def", "eq_unfold", "induct", "induct_unfolding", "mutual_induct", "fun_cases", - "fun_cases_unfolding", "rec", "recOn", "casesOn", "brecOn", "binductionOn", "below", "ibelow", - "noConfusion", "noConfusionType", "ctorIdx", "ctorElim", "ctorElimType", "toCtorIdx", "ofNat", - "ofNat_ctorIdx", "injEq", "inj", "sizeOf_spec", "mk", "congr_simp", "ext", "ext_iff", "elim", - "proxyType", "proxyTypeEquiv", "decEq", "repr", "go", -} -# Generated constants whose use unfolds the owner's body. -UNFOLDING = {"eq_def", "eq_unfold", "induct", "induct_unfolding", "mutual_induct", "fun_cases", - "fun_cases_unfolding"} -# Attributes through which a declaration can be used without being named. -IMPLICIT_ATTRS = { - "simp", "simps", "fun_prop", "aesop", "instance", "ext", "refl", "trans", "symm", "csimp", - "program_certificate", "fo_realize", "elab_as_elim", "induction_eliminator", - "cases_eliminator", "default_instance", "coe", "gcongr", "positivity", "norm_num", "bound", - "grind", "simproc", "congr", "mono", "continuity", "measurability", "app_unexpander", -} -DEFINITION_KEYWORDS = {"def", "abbrev", "structure", "class", "inductive", "opaque", - "irreducible_def"} -KEYWORD = re.compile( - r"\b(theorem|lemma|def|abbrev|instance|structure|class|inductive|opaque|alias|axiom|" - r"irreducible_def)\b") -ATTR_BLOCK = re.compile(r"@\[((?:[^\[\]]|\[(?:[^\[\]]|\[[^\[\]]*\])*\])*)\]") -ATTRIBUTE_COMMAND = re.compile( - r"^attribute\s*\[((?:[^\[\]]|\[(?:[^\[\]]|\[[^\[\]]*\])*\])*)\]", re.M) -NOTATION_COMMAND = re.compile( - r"^(?:@\[[^\]\n]*\]\s*)?(?:(?:scoped|local)\s+)?" - r"(?:notation3?|infixl?|infixr|prefix|postfix|macro|macro_rules|syntax|elab|elab_rules)\b", - re.M) -COMMAND_START = re.compile( - r"^(?:@\[|/--|/-!|#|(?:(?:public|private|protected|noncomputable|unsafe|partial|nonrec|" - r"scoped|local|meta)\s+)*(?:theorem|lemma|def|abbrev|opaque|axiom|instance|structure|class|" - r"inductive|example|namespace|section|end|open|universe|variable|include|omit|attribute|" - r"set_option|syntax|macro|macro_rules|elab|elab_rules|notation|notation3|infixl|infixr|infix|" - r"prefix|postfix|initialize|mutual|export|alias|register_simp_attr|declare_aesop_rule_sets|" - r"add_decl_doc|deriving)\b)", re.M) -IDENT = re.compile(r"[A-Za-z_À-ɏͰ-Ͽᴀ-ᶿ℀-⅏]" - r"[\w'!?₀-ₜᵢ-ᵪ.]*") -UNFOLD_TACTIC = re.compile(r"\b(?:unfold|delta|unfold_let)\b(?:\s+[^\s;⟨(\[\],]+)*\s+$") -REWRITE_HEAD = re.compile( - r"\b(?:simp|simp_all|dsimp|simp_rw|rw|rwa|rewrite|erw|nth_rewrite|nth_rw|simpa|simp_arith|" - r"field_simp|norm_num|grind|unfold)\b[^\[\]\n]*$") -LIST_ELEMENT = re.compile(r"\s*(?:←|<-)?\s*") -MAIN_SECTION = re.compile(r"^##\s+Main\b", re.M) -BULLET = re.compile(r"^(\s*)[*-]\s+") -DOC_NAME = re.compile(r"@?[^\s`()\[\]{},;:]*[A-Za-z][^\s`()\[\]{},;:]*") - - -# --- Pure helpers (unit-tested in scripts/test_quality_report.py) ------------------------------- - -def area_of(path: str) -> str: - """The #587 area of a library source path relative to `Complexity/`.""" - for name, _, prefixes in AREAS: - if path.startswith(prefixes): - return name - return OTHER_AREA - - -def top_dir(path: str) -> str: - return path.split("/", 1)[0] if "/" in path else "(root)" - - -def module_role(module: str) -> str: - """`lib`, `test` or `abstract` for a module of one of the three libraries.""" - if module.startswith("ComplexityAbstracts.") or module.startswith("ComplexityTests.Abstracts."): - return "abstract" - if module.startswith("ComplexityTests."): - return "test" - return "lib" - - -def source_path(module: str) -> Path: - rel = module.replace(".", "/") + ".lean" - return ROOT / ("abstracts/" + rel if module.startswith("ComplexityAbstracts") else rel) - - -def is_internal(component: str) -> bool: - return (component.startswith("_") or component.isdigit() - or re.fullmatch(r"(?:eq|match|proof|omega)_[\d_]+", component) is not None) - - -def owner_of(name: str, owners: dict[str, str]) -> str | None: - """The user declaration that `name` is, belongs to, or was generated from.""" - if name in owners: - return owners[name] - parts = name.split(".") - for i in range(len(parts) - 1, 0, -1): - if not (parts[i] in GENERATED or is_internal(parts[i])): - return None - prefix = ".".join(parts[:i]) - if prefix in owners: - return owners[prefix] - return None - - -def unfolds_by_name(name: str, owner: str) -> bool: - """Whether referring to `name` unfolds the body of `owner` (an equation lemma, say).""" - if name == owner or not name.startswith(owner + "."): - return False - first = name[len(owner) + 1:].split(".")[0] - return first in UNFOLDING or re.fullmatch(r"eq_\d+", first) is not None - - -def utf16_index(line: str, column: int) -> int: - """The code-point index of a UTF-16 column, as LSP positions in `.ilean` files count.""" - if line.isascii(): - return column - units = 0 - for i, char in enumerate(line): - if units >= column: - return i - units += 2 if ord(char) > 0xFFFF else 1 - return len(line) - - -def unfolds_at(lines: list[str], line: int, index: int) -> bool: - """Whether the identifier at `lines[line][index]` (masked code) is an argument of `unfold` or - `delta`, or an element of the lemma list of a rewriting or simplifying tactic.""" - before = lines[line][:index] - if UNFOLD_TACTIC.search(before): - return True - text = "\n".join(lines[max(0, line - 8):line] + [before]) - depth, element = 0, None - for i in range(len(text) - 1, -1, -1): - char = text[i] - if char in ")]}⟩": - depth += 1 - elif char in "([{⟨": - if depth: - depth -= 1 - continue - if char != "[" or not LIST_ELEMENT.fullmatch(text[i + 1:] if element is None - else element): - return False - return REWRITE_HEAD.search(text[text.rfind("\n", 0, i) + 1:i]) is not None - elif char == "," and not depth and element is None: - element = text[i + 1:] - if not LIST_ELEMENT.fullmatch(element): - return False - return False - - -def split_top_level(text: str) -> list[str]: - items, depth, start = [], 0, 0 - for i, char in enumerate(text): - if char in "([{": - depth += 1 - elif char in ")]}": - depth -= 1 - elif char == "," and not depth: - items.append(text[start:i]) - start = i + 1 - items.append(text[start:]) - return [item.strip() for item in items if item.strip()] - - -def attribute_names(attrs: str) -> set[str]: - """Attribute names in the body of `@[…]` or `attribute […]`, without `local` ones.""" - names = set() - for item in split_top_level(attrs): - words = item.split() - if words[0] == "local": - continue - if words[0] == "scoped" and len(words) > 1: - words = words[1:] - names.add(words[0].rstrip("!?")) - return names - - -def header_info(header: str) -> tuple[str | None, set[str]]: - """The declaration keyword and attributes in a masked declaration header.""" - attrs = set() - for block in ATTR_BLOCK.findall(header): - attrs |= attribute_names(block) - keywords = KEYWORD.findall(ATTR_BLOCK.sub(" ", header)) - return (keywords[-1] if keywords else None), attrs - - -def doc_blocks(text: str) -> list[str]: - return re.findall(r"/-!(.*?)-/", text, re.S) - - -def listed_names(doc: str) -> list[str]: - """Names listed in the "Main …" sections of a module docstring: the backquoted names before - the first colon (outside backquotes) of each bullet.""" - names = [] - for section in re.split(r"^(?=#)", doc, flags=re.M): - if not MAIN_SECTION.match(section): - continue - items: list[str | None] = [] - for line in section.splitlines()[1:]: - if BULLET.match(line): - items.append(BULLET.sub("", line, count=1)) - elif items and items[-1] is not None and line.startswith(" ") and line.strip(): - items[-1] += " " + line.strip() - else: - items.append(None) - for item in filter(None, items): - head, inside = item, False - for i, char in enumerate(item): - if char == "`": - inside = not inside - elif char == ":" and not inside: - head = item[:i] - break - names += [token.lstrip("@.") for token in re.findall(r"`([^`]*)`", head) - if DOC_NAME.fullmatch(token)] - return names - - -def doc_named(names: list[str], tokens: set[str]) -> set[str]: - """The names that some documentation token could denote: the token is the name or one of its - suffixes on a component boundary. An ambiguous token, such as a short name, protects every - declaration it could denote.""" - by_last: dict[str, list[str]] = defaultdict(list) - for name in names: - by_last[name.rsplit(".", 1)[-1]].append(name) - return {name for token in tokens for name in by_last.get(token.rsplit(".", 1)[-1], ()) - if matches(name, token)} - - -def doc_tokens(text: str) -> set[str]: - """The backquoted tokens of a docstring or Markdown text.""" - return {t.lstrip("@.") for t in re.findall(r"`([^`\s]+)`", text)} - {""} - - -def mentioned(doc_tokens: set[str], name: str) -> bool: - return any(name == t or name.endswith("." + t) for t in doc_tokens) - - -def matches(name: str, token: str) -> bool: - plain = re.sub(r"^_private\.[^0-9]*\.0\.", "", name) - return plain == token or plain.endswith("." + token) - - -def rebuild_fanout(imports: dict[str, list[tuple[str, bool]]]) -> dict[str, set[str]]: - """Modules that Lake rebuilds when a module's exported interface changes. - - `imports[m]` lists `(dependency, is_public)` pairs. A module depends on the exported `.olean` - of each direct import and of everything those reexport through chains of `public import`s; - it does not depend on what they import privately.""" - reexporters: dict[str, set[str]] = defaultdict(set) - importers: dict[str, set[str]] = defaultdict(set) - for module, deps in imports.items(): - for dep, public in deps: - importers[dep].add(module) - if public: - reexporters[dep].add(module) - result = {} - for module in imports: - seen, stack = {module}, [module] - while stack: - for parent in reexporters[stack.pop()]: - if parent not in seen: - seen.add(parent) - stack.append(parent) - result[module] = set().union(*(importers[m] for m in seen)) - {module} - return result - - -def transitive_importers(imports: dict[str, list[tuple[str, bool]]]) -> dict[str, set[str]]: - importers: dict[str, set[str]] = defaultdict(set) - for module, deps in imports.items(): - for dep, _ in deps: - importers[dep].add(module) - result = {} - for module in imports: - seen, stack = set(), [module] - while stack: - for importer in importers[stack.pop()]: - if importer not in seen: - seen.add(importer) - stack.append(importer) - result[module] = seen - return result - - -# --- Data loading ------------------------------------------------------------------------------- - -def run(cmd: list[str], **kwargs) -> subprocess.CompletedProcess: - return subprocess.run(cmd, cwd=ROOT, text=True, check=True, **kwargs) - - -DEFAULT_BUILD_DIR = ROOT / ".lake/build/lib/lean" -# The build outputs the report reads. -REPORT_INPUTS = (".ilean", ".olean", ".olean.server", ".olean.private") - - -def lake_outputs_current() -> bool: - """Whether Lake finds the default build outputs of the three libraries current.""" - return subprocess.run(["lake", "build", "--no-build", *ROOTS], cwd=ROOT, - capture_output=True).returncode == 0 - - -def output_differences(build_dir: Path, reference: Path) -> list[str]: - """Report inputs that are missing, extra or different in `build_dir` compared to - `reference`, as paths relative to them.""" - def inputs(directory: Path) -> set[Path]: - # The roots' own outputs (`Complexity.ilean`, …) sit beside their directories, and the - # report takes its module inventory from their imports. - files = [p for root in ROOTS - for p in [*(directory / root).rglob("*"), *directory.glob(f"{root}.*")]] - return {p.relative_to(directory) for p in files - if p.name.endswith(REPORT_INPUTS) and p.is_file()} - ours, theirs = inputs(build_dir), inputs(reference) - changed = {p for p in ours & theirs - if not filecmp.cmp(build_dir / p, reference / p, shallow=False)} - return sorted(map(str, (ours ^ theirs) | changed)) - - -def check_outputs(build_dir: Path, skip: bool, current=lake_outputs_current, - reference: Path = DEFAULT_BUILD_DIR) -> str: - """How the build outputs were checked, or exit when they are not current. - - Lake checks only the default build directory, so another directory must hold exactly the - same report inputs as the checked default outputs.""" - if skip: - return "not checked against the sources" - if not current(): - sys.exit("build outputs are missing or stale; run `lake build " + " ".join(ROOTS) - + "` (or pass --no-build-check)") - if build_dir.resolve() == reference.resolve(): - return "checked current by `lake build --no-build`" - differences = output_differences(build_dir, reference) - if differences: - sys.exit(f"{build_dir} differs from the current build outputs in {len(differences)} " - f"file(s) (e.g. {', '.join(differences[:3])}); pass --no-build-check to " - "report on it anyway") - return "checked identical to the current outputs of `lake build --no-build`" - - -ROOT_IMPORT = re.compile(r"^(?:public\s+)?(?:meta\s+)?import\s+(\S+)", re.M) - - -def listed_modules(text: str) -> list[str]: - """The modules a root source file imports.""" - return ROOT_IMPORT.findall(text) - - -def load_ileans(build_dir: Path, missing: list[str] | None = None, - glob=glob_modules) -> dict[str, dict]: - """The `.ilean` data of the modules the three libraries' roots import, by module name. - - A long-lived build directory keeps the outputs of modules that were since deleted or moved, - and `lake build --no-build` does not notice them, so modules are found by following imports - from the roots rather than by listing files. A glob-built library (`GLOB_ROOTS`) has no root - file, so its source files are the starting points instead. Every starting point and every - module they import must have one; a missing file means the build is incomplete. The aggregator - roots themselves are left out. - - Given a list `missing`, the build may be partial instead (for a tree that does not build - completely): the modules are those the roots' source files import, and the ones without an - `.ilean` file are appended to `missing`.""" - if missing is not None: - ileans = {} - for root in ROOTS: - modules = (glob(root) if root in GLOB_ROOTS - else listed_modules(source_path(root).read_text())) - for module in modules: - path = build_dir / (module.replace(".", "/") + ".ilean") - if path.is_file(): - ileans[module] = json.loads(path.read_text()) - else: - missing.append(module) - return ileans - ileans, todo = {}, [(module, None) for module in root_modules(glob)] - while todo: - module, importer = todo.pop() - if module in ileans: - continue - path = build_dir / (module.replace(".", "/") + ".ilean") - if not path.is_file(): - sys.exit(f"{path} is missing ({'imported by ' + importer if importer else 'a root'}); " - "run `lake build " + " ".join(ROOTS) + "` first") - ileans[module] = json.loads(path.read_text()) - todo.extend((i[0], module) for i in ileans[module]["directImports"] - if i[0].split(".")[0] in ROOTS) - for root in ROOTS: - if root not in GLOB_ROOTS: - del ileans[root] - return ileans - - -def load_constants(build_dir: Path, modules: list[str], pairs: str | None = None - ) -> tuple[dict[str, dict], list[dict]]: - """Constants of `modules`; `pairs` (`tidy=plain,…`) adds the fields that - `scripts/tidy_sweep.py` reads (see `scripts/QualityReport.lean`).""" - out = run(["lake", "env", "lean", "--run", "scripts/QualityReport.lean", str(build_dir)] - + ([pairs] if pairs else []), - input="\n".join(modules) + "\n", capture_output=True).stdout - constants, duplicates = {}, [] - for line in out.splitlines(): - row = json.loads(line) - if "dup" in row: - duplicates.append(row) - else: - constants[row["n"]] = row - return constants, duplicates - - -class Source: - """A source file with its masked code split into lines.""" - - def __init__(self, path: Path): - self.text = path.read_text(encoding="utf-8") - self.code = masks(self.text)[0] - self.raw_lines = self.text.split("\n") - self.lines = self.code.split("\n") - self.starts = [0] - for raw in self.raw_lines: - self.starts.append(self.starts[-1] + len(raw) + 1) - - def span(self, line: int, col: int, end_line: int, end_col: int) -> str: - """Masked code between 1-based lines and code-point columns.""" - if line == end_line: - return self.lines[line - 1][col:end_col] - return "\n".join([self.lines[line - 1][col:]] + self.lines[line:end_line - 1] - + [self.lines[end_line - 1][:end_col]]) - - def offset(self, line0: int, index: int) -> int: - return self.starts[line0] + index - - -# --- Analysis ----------------------------------------------------------------------------------- - -class Library: - """Build outputs and sources of the three libraries, loaded lazily where possible.""" - - def __init__(self, build_dir: Path, pairs: str | None = None, - missing: list[str] | None = None): - self.build_dir = build_dir - self.ileans = load_ileans(build_dir, missing) - self.modules = sorted(m for m in self.ileans if m.startswith("Complexity.")) - self.constants, self.duplicate_rows = load_constants(build_dir, self.modules, pairs) - self.sources: dict[str, Source] = {} - - def source(self, module: str) -> Source: - if module not in self.sources: - self.sources[module] = Source(source_path(module)) - return self.sources[module] - - def references(self, module: str): - """`(name, defining module, info)` for each constant referenced in `module`.""" - for key, info in self.ileans[module]["references"].items(): - ident = json.loads(key).get("c") - if ident: - yield ident["n"], ident["m"], info - - -def collect_declarations(lib: Library) -> tuple[dict[str, dict], dict[str, str], Counter]: - """Public declarations written in library sources (the binders recorded in `.ilean` files), - and the owner of every such name: a structure for its fields and constructors, a definition - for the lemmas `@[simps]` generates, and the declaration itself otherwise.""" - decls: dict[str, dict] = {} - owners: dict[str, str] = {} - private_count: Counter = Counter() - for module in lib.modules: - rel = module.removeprefix("Complexity.").replace(".", "/") + ".lean" - for name, defined_in, info in lib.references(module): - if defined_in != module or not info["definition"]: - continue - if name.startswith("_private."): - private_count[module] += 1 - owners[name] = name - continue - const = lib.constants.get(name) - if not const or not const["e"]: - continue - parent = info["definition"][4] if len(info["definition"]) == 5 else None - role = "decl" - if const["k"] == "ctor": - role = "member" - elif parent and parent != name: - if not name.startswith(parent + "."): - role = "generated" - elif lib.constants.get(parent, {}).get("k") == "induct": - role = "member" - decls[name] = { - "name": name, "module": module, "path": rel, "area": area_of(rel[:-5] + "/"), - "role": role, "kind": const["k"], "exported": const["e"], "doc": const["doc"], - "tidy": const["tidy"], "range": const["r"], "parent": parent, - "lib_refs": set(), "test_refs": set(), "abstract_refs": set(), "local_uses": 0, - "unfolded_by": set(), - } - for name, decl in decls.items(): - owned = decl["role"] != "decl" and decl["parent"] in decls - owners[name] = decl["parent"] if owned else name - return decls, owners, private_count - - -def command_spans(code: str, command: re.Pattern) -> list[tuple[int, int, str]]: - """`(start, end, header)` of each command matching `command`, up to the next command.""" - spans = [] - for match in command.finditer(code): - end = next((m.start() for m in COMMAND_START.finditer(code, match.end())), len(code)) - spans.append((match.start(), end, match[1] if command.groups else match[0])) - return spans - - -# Report-only S4 measurement. These prefixes describe the proposed target, not an exemption -# from S3 or an assertion that the boundary migration has already happened. -TIDY_INTERNAL_PREFIXES = ( - "Complexity/Computability/Machines/Turing/MultiTape/Internal/", - "ComplexityTests/Machines/Turing/MultiTape/Internal/", -) -BRIDGE_TOKEN = re.compile(r"\.(?:tidy|of_tidy)(?![\w'!?])") -LOCAL_FUN_PROP = re.compile(r"(?:^|,)\s*local\s+fun_prop\s*(?:,|$)") - - -def tidy_source_signals(text: str, tidy_names: set[str], known_names: set[str] | None = None - ) -> dict: - """Lexical bridge occurrences and local registrations of known tidy-typed constants. - - Reuse the comment/string/character masks and attribute parser. Name suffix matching is - conservative: an ambiguous suffix counts if any candidate has a tidy type. Unresolved - local registrations are retained for review, not silently called plain. This does not - expand macros, resolve local notation, or count semantic pairs of bridge applications. - """ - code = masks(text)[1] - bridges = [{"line": code.count("\n", 0, m.start()) + 1, - "bridge": m[0][1:]} for m in BRIDGE_TOKEN.finditer(code)] - local, unresolved = [], [] - blocks = [(m, False) for m in ATTR_BLOCK.finditer(code)] - blocks += [(m, True) for m in ATTRIBUTE_COMMAND.finditer(code)] - for block, command in sorted(blocks, key=lambda x: x[0].start()): - if not LOCAL_FUN_PROP.search(block[1]): - continue - after = code[block.end():] - # An attribute command names one or more targets; an inline attribute precedes a decl. - if command: - following = next(COMMAND_START.finditer(code, block.end()), None) - target_text = code[block.end():following.start() if following else len(code)] - targets = IDENT.findall(target_text) - targets = targets[:targets.index("in")] if "in" in targets else targets - else: - decl = re.match(r"\s*(?:(?:public|private|protected|noncomputable|unsafe|partial|" - r"nonrec|meta)\s+)*(?:theorem|lemma|def|abbrev|instance|opaque)\s+", - after) - target = IDENT.match(after, decl.end()) if decl else None - targets = [target[0]] if target else [] - line = code.count("\n", 0, block.start()) + 1 - if not targets: - unresolved.append({"line": line, "target": None}) - for target in targets: - row = {"line": line, "target": target} - candidates = [n for n in tidy_names if n == target or n.endswith("." + target)] - if candidates: - local.append({**row, "candidates": sorted(candidates)}) - elif target not in (known_names or set()): - unresolved.append(row) - return {"bridges": bridges, "local_tidy_fun_prop": local, - "unresolved_local_fun_prop": unresolved} - - -def private_tidy_declarations(constants: dict[str, dict], source) -> dict[str, list[dict]]: - """Private source declarations with tidy in their type, excluding generated children.""" - found: dict[str, list[dict]] = defaultdict(list) - by_range: dict[tuple, set[str]] = defaultdict(set) - for name, c in constants.items(): - if c["r"]: - by_range[c["m"], tuple(c["r"])].add(name) - for name, c in constants.items(): - if not (name.startswith("_private.") and c["tidy"] and c["r"]): - continue - r = c["r"] - selected = source(c["m"]).span(*r[4:]).strip() - # An authored anonymous instance selects the keyword, not its auto-generated name. - # Its auxiliary constants can inherit that same range; retain only the source owner, - # considering *all* types so a plain owner cannot leave a tidy generated child behind. - anonymous_instance = selected == "instance" and not is_internal(name.rsplit(".", 1)[-1]) \ - and not any(name.startswith(other + ".") for other in by_range[c["m"], tuple(r)] - if other != name) - if selected and (name.endswith("." + selected) or anonymous_instance): - found[c["m"]].append({"name": name, "line": r[4], "mentions": c["tidy"]}) - return found - - -def tidy_usage_report(lib: Library, prefixes: tuple[str, ...] = TIDY_INTERNAL_PREFIXES) -> dict: - """Per-module report of the S4 boundary, with no baseline comparison or enforcement. - - Public statement counts use exactly S3's source-declaration/type rule. Private counts - require a source declaration range and a tidy constant in its elaborated type; generated - constants sharing the owner's range are excluded by matching the selected source name. - Tests/abstracts use their own metadata. Guide files have source-only signals and explicitly - unknown statement counts, since the root build does not elaborate the separate guide. - """ - modules = sorted(m for m in lib.ileans if m.startswith( - ("Complexity.", "ComplexityTests.", "ComplexityAbstracts."))) - extra = [m for m in modules if m not in lib.modules] - constants = dict(lib.constants) - if extra: - more, _ = load_constants(lib.build_dir, extra) - constants.update(more) - tidy_names = {n for n, c in constants.items() if c["tidy"]} - # Known suffixes distinguish resolved plain targets from unknown ones without rescanning - # the entire constant inventory for every source attribute. - known_suffixes = {".".join(parts[i:]) for n in constants - for parts in [n.split(".")] for i in range(len(parts))} - public_tidy_names = {n for n in tidy_names if not n.startswith("_private.")} - private_tidy_names: dict[str, set[str]] = defaultdict(set) - for n in tidy_names - public_tidy_names: - private_tidy_names[constants[n]["m"]].add(n) - public, _, _ = collect_declarations(lib) - public_by_module = Counter(d["module"] for n, d in public.items() - if d["role"] != "generated" and - (constants[n]["tidy"] or constants[n].get("tb"))) - private_by_module = private_tidy_declarations(constants, lib.source) - rows = [] - sources = [(m, source_path(m), True) for m in modules] - sources += [(str(p.relative_to(ROOT)), p, False) for p in sorted( - (ROOT / "guide").rglob("*.lean")) if ".lake" not in p.parts] - for module, path, metadata in sources: - rel = path.relative_to(ROOT).as_posix() - if any(rel.startswith(p) for p in prefixes): - continue - text = path.read_text() - signals = tidy_source_signals(text, - public_tidy_names | private_tidy_names[module], - known_suffixes) - private = private_by_module[module] if metadata else None - counts = {"public_tidy_statements": public_by_module[module] - if module.startswith("Complexity.") else None, - "private_tidy_declarations": len(private) if metadata else None, - "local_tidy_fun_prop": len(signals["local_tidy_fun_prop"]), - "bridge_occurrences": len(signals["bridges"])} - rows.append({"module": module, "path": rel, - "role": module_role(module) if metadata else "guide", "counts": counts, - "mentions_tidy": bool(re.search(r"Tidily|IsTidy|\.(?:of_)?tidy\b", - masks(text)[1])), - "private_tidy_declarations": private, **signals}) - keys = ("public_tidy_statements", "private_tidy_declarations", - "local_tidy_fun_prop", "bridge_occurrences") - source_hash = hashlib.sha256() - for path in ([source_path(root) for root in ROOTS if root not in GLOB_ROOTS] - + [p for _, p, _ in sources]): - source_hash.update(path.relative_to(ROOT).as_posix().encode() + b"\0") - source_hash.update(path.read_bytes() + b"\0") - provenance = {"revision": run(["git", "rev-parse", "HEAD"], capture_output=True).stdout.strip(), - "tree": run(["git", "rev-parse", "HEAD^{tree}"], capture_output=True).stdout.strip(), - "dirty": bool(run(["git", "status", "--porcelain"], - capture_output=True).stdout.strip()), - "source_dirty": bool(run(["git", "status", "--porcelain", "--", - "Complexity", "ComplexityTests", "abstracts", "guide", - "Complexity.lean"], - capture_output=True).stdout.strip()), - "scanned_source_sha256": source_hash.hexdigest(), - "scanned_files": len(sources), "build_dir": str(lib.build_dir)} - return {"provenance": provenance, "internal_prefixes": list(prefixes), "report_only": True, - "totals": {k: sum(r["counts"][k] or 0 for r in rows) for k in keys}, - "files_mentioning_tidy": sum(r["mentions_tidy"] for r in rows), - "modules": rows, - "notes": ["The prefixes are a proposed measurement boundary, not S3 exemptions.", - "Public counts use S3's declaration/type rule only for library modules, but " - "this report's stated boundary replaces S3's allowlist. Null is not zero.", - "Private counts inspect elaborated types, not names or proof bodies; generated " - "constants are excluded by source selection. Type aliases are not unfolded. " - "Guide metadata is unavailable.", - "Bridge counts are lexical occurrences, not semantic round-trip pairs; comments " - "and literals are masked. Other named erasure APIs are not included.", - "Local registration targets use conservative suffix matching, without elaborated " - "name resolution; unresolved targets are listed, not assumed plain."]} - - -def tidy_usage_markdown(report: dict, top: int = 20) -> str: - """Human view of the same report-only per-module data, with full detail in JSON.""" - out = ["### Proof-internal tidy usage (S4, report only)", "", - "Measurement excludes: " + ", ".join(f"`{p}`" for p in report["internal_prefixes"]), - "", "| Module | Public tidy statements | Private tidy declarations | Local tidy " - "fun_prop targets | Bridge occurrences |", "|---|---:|---:|---:|---:|"] - rows = sorted(report["modules"], key=lambda r: ( - -sum(v or 0 for v in r["counts"].values()), r["path"])) - for row in [r for r in rows if any(r["counts"].values())][:top]: - values = ["unknown" if v is None else str(v) for v in row["counts"].values()] - out.append(f"| `{row['path']}` | " + " | ".join(values) + " |") - out += ["| Total (known counts) | " + " | ".join(map(str, report["totals"].values())) + " |", - "", f"{report['files_mentioning_tidy']} files mention tidy outside the measurement " - "boundary. Full per-module locations and unresolved targets are in the JSON report.", - "", *["- " + note for note in report["notes"]]] - return "\n".join(out) + "\n" - - -def annotate_headers(lib: Library, decls: dict[str, dict]) -> None: - """Declaration keywords and attributes, including `notation` for declarations named in - notation, macro and syntax commands, whose uses leave no references.""" - for decl in decls.values(): - keyword, attrs = None, set() - if decl["range"]: - line, col, _, _, sel_line, sel_col, sel_end_line, sel_end_col = decl["range"] - src = lib.source(decl["module"]) - keyword, attrs = header_info(src.span(line, col, sel_line, sel_col)) - if keyword is None: # the selection is the keyword, as for anonymous instances - keyword, attrs = header_info(src.span(line, col, sel_end_line, sel_end_col)) - decl["keyword"], decl["attrs"] = keyword, attrs - for decl in decls.values(): - if decl["role"] == "generated" and decl["parent"] in decls: - decls[decl["parent"]]["attrs"].add("simps") - by_last: dict[str, list[str]] = defaultdict(list) - for name in decls: - by_last[name.rsplit(".", 1)[-1]].append(name) - for module in lib.modules: - code = lib.source(module).code - for start, end, _ in command_spans(code, NOTATION_COMMAND): - for token in set(IDENT.findall(code, start, end)): - token = token.rstrip(".") - for name in by_last.get(token.rsplit(".", 1)[-1], ()): - if matches(name, token) and ("." in token or decls[name]["module"] == module): - decls[name]["attrs"].add("notation") - - -def collect_references(lib: Library, decls: dict[str, dict], owners: dict[str, str]) -> None: - """Record, for each declaration, the other modules that refer to it, its uses inside its own - module, `attribute […]` commands there, and the library modules that unfold it by name.""" - attribute_spans = {m: [(start, end, attribute_names(attrs)) for start, end, attrs in - command_spans(lib.source(m).code, ATTRIBUTE_COMMAND)] - for m in lib.modules} - for module in lib.ileans: - if module in ROOTS: - continue - role = module_role(module) - for name, _, info in lib.references(module): - owner = owner_of(name, owners) - if owner not in decls or not info["usages"]: - continue - decl = decls[owner] - if module != decl["module"]: - decl[f"{role}_refs"].add(module) - if role == "lib" and decl["exported"] == "def": - src = lib.source(module) - if unfolds_by_name(name, owner) or any( - unfolds_at(src.lines, u[0], utf16_index(src.raw_lines[u[0]], u[1])) - for u in info["usages"]): - decl["unfolded_by"].add(module) - continue - for usage in info["usages"]: - if len(usage) == 5: - decl["local_uses"] += owner_of(usage[4], owners) != owner - continue - src = lib.source(module) - offset = src.offset(usage[0], utf16_index(src.raw_lines[usage[0]], usage[1])) - for start, end, attrs in attribute_spans[module]: - if start <= offset < end: - decl["attrs"] |= attrs - - -def check_module_docs(lib: Library, decls: dict[str, dict], owners: dict[str, str]) -> dict: - """Compare each module docstring's "Main …" lists with the module's declarations, and mark - declarations named in module docstrings or the README files.""" - names_by_module: dict[str, list[str]] = defaultdict(list) - for name in owners: - if name.startswith("_private."): - names_by_module[name.removeprefix("_private.").split(".0.", 1)[0]].append(name) - for name, decl in decls.items(): - names_by_module[decl["module"]].append(name) - by_last: dict[str, list[str]] = defaultdict(list) - for name in decls: - by_last[name.rsplit(".", 1)[-1]].append(name) - const_by_last: dict[str, list[str]] = defaultdict(list) - for name in lib.constants: - const_by_last[name.rsplit(".", 1)[-1]].append(name) - all_tokens = set().union(*(doc_tokens((ROOT / path).read_text()) for path in EXTERNAL_DOCS)) - drift_by_module = {} - for module in lib.modules: - docs = doc_blocks(lib.source(module).text) - tokens = set().union(*map(doc_tokens, docs)) - all_tokens |= tokens - in_module = names_by_module[module] - upstream = [name for name, defined_in, _ in lib.references(module) - if not defined_in.startswith("Complexity")] - listed = [name for doc in docs for name in listed_names(doc)] - drift = {"listed": len(listed), "missing": [], "private": [], "elsewhere": [], - "unlisted": [], "has_main": any(MAIN_SECTION.search(d) for d in docs)} - for token in listed: - last = token.rsplit(".", 1)[-1] - here = [n for n in in_module if matches(n, token)] - if any(not n.startswith("_private.") for n in here): - for name in here: - if name in decls: - decls[name]["listed"] = True - elif here: - drift["private"].append(token) - elif any(matches(n, token) for n in by_last.get(last, ())): - drift["elsewhere"].append(token) - elif not any(matches(n, token) for n in upstream + const_by_last.get(last, [])): - drift["missing"].append(token) - for name in in_module: - decl = decls.get(name) - if decl is None: - continue - if (decl["role"] == "decl" and decl["keyword"] in DEFINITION_KEYWORDS - and "deprecated" not in decl["attrs"] and not mentioned(tokens, name)): - drift["unlisted"].append(name) - drift_by_module[module] = drift - named = doc_named(list(decls), all_tokens) - for name, decl in decls.items(): - decl["doc_named"] = name in named - return drift_by_module - - -def classify(decls: dict[str, dict]) -> None: - for decl in decls.values(): - if decl["lib_refs"]: - category = "outside" - elif decl["test_refs"] or decl["abstract_refs"]: - category = "tests_only" - elif decl["local_uses"]: - category = "module_only" - else: - category = "unreferenced" - keyword = decl["keyword"] - if "deprecated" in decl["attrs"]: - sort = "deprecated" - elif keyword == "alias": - sort = "alias" - elif keyword == "instance" or "instance" in decl["attrs"]: - sort = "instance" - elif decl["kind"] == "thm": - sort = "theorem" - elif decl["kind"] == "induct" or keyword in ("structure", "class", "inductive"): - sort = "type" - else: - sort = "definition" - decl["category"], decl["sort"] = category, sort - decl["implicit"] = sorted(decl["attrs"] & (IMPLICIT_ATTRS | {"notation"})) - if sort == "instance" and "instance" not in decl["attrs"]: - decl["implicit"].append("instance") - decl["listed"] = decl.get("listed", False) - decl["headline"] = decl["listed"] or bool(decl["abstract_refs"]) - - -def find_candidates(lib: Library, decls: dict[str, dict], owners: dict[str, str]) -> None: - """Privatization candidates: never referenced outside their module, without implicit uses, - not named in documentation, not deprecated, and not mentioned by the exported statement or - exposed body of a declaration that stays public (a fixed point, since candidates in the same - module can become private together).""" - pins: dict[str, set[str]] = defaultdict(set) - for name, const in lib.constants.items(): - if const["e"]: - holder = owner_of(name, owners) or name - for used in const["u"]: - target = owner_of(used, owners) - if target in decls and target != holder: - pins[target].add(holder) - candidates = {n for n, d in decls.items() if d["role"] == "decl" and d["category"] in - ("module_only", "unreferenced") and d["sort"] != "deprecated" - and not d["implicit"] and not d["doc_named"]} - while pinned := {n for n in candidates if pins[n] - candidates}: - candidates -= pinned - for name, decl in decls.items(): - decl["candidate"] = name in candidates - decl["pinned_by"] = sorted(pins[name] - candidates) - - -def find_duplicates(lib: Library, decls: dict[str, dict]) -> list[dict]: - """Groups of declarations, other than deprecated ones and aliases, in different modules.""" - duplicates = [] - for row in lib.duplicate_rows: - members = [(m, n) for m, n in row["dup"] if n in decls and decls[n]["role"] == "decl" - and decls[n]["sort"] not in ("deprecated", "alias")] - if len({m for m, _ in members}) > 1: - duplicates.append({"kind": row["k"], "members": sorted(members)}) - for _, n in members: - decls[n]["duplicate"] = row["k"] - return duplicates - - -def analyse(build_dir: Path) -> dict: - lib = Library(build_dir) - decls, owners, private_count = collect_declarations(lib) - generated_public = sum(1 for name, const in lib.constants.items() if const["e"] - and name not in decls and not any(map(is_internal, name.split(".")))) - annotate_headers(lib, decls) - collect_references(lib, decls, owners) - doc_drift = check_module_docs(lib, decls, owners) - classify(decls) - find_candidates(lib, decls, owners) - duplicates = find_duplicates(lib, decls) - imports = {m: [(i[0], not i[1]) for i in lib.ileans[m]["directImports"] - if i[0].startswith("Complexity.") and i[0] in lib.ileans] for m in lib.modules} - proofs, unparsed = {}, [] - for m in lib.modules: - try: - proofs[m] = scan_proofs(lib.source(m).text, str(source_path(m).relative_to(ROOT))) - except ValueError as error: # keep the other signals when one module defeats the scanner - proofs[m] = [] - unparsed.append(f"{m}: {error}") - return { - "decls": decls, "doc_drift": doc_drift, "duplicates": duplicates, "proofs": proofs, - "fanout": rebuild_fanout(imports), "importers": transitive_importers(imports), - "private_count": sum(private_count.values()), "generated_public": generated_public, - "lib_modules": lib.modules, "proofs_unparsed": unparsed, - "tidy_usage": tidy_usage_report(lib), - } - - -# --- Reporting ---------------------------------------------------------------------------------- - -def surface_counts(decls: list[dict]) -> Counter: - counts = Counter({"public": 0, "never_outside": 0, "candidates": 0}) - for d in decls: - counts["public"] += 1 - counts[d["category"]] += 1 - if d["category"] in ("module_only", "unreferenced"): - counts["never_outside"] += 1 - if d["sort"] == "deprecated": - counts["never_outside_deprecated"] += 1 - elif d["implicit"]: - counts["never_outside_implicit"] += 1 - elif d["doc_named"]: - counts["never_outside_doc_named"] += 1 - elif not d["candidate"]: - counts["never_outside_pinned"] += 1 - else: - counts["candidates"] += 1 - kind = "theorems" if d["sort"] == "theorem" else "definitions" - counts["candidate_" + kind] += 1 - if d["category"] == "tests_only": - counts["tests_only_" + ("both" if d["test_refs"] and d["abstract_refs"] else - "abstracts" if d["abstract_refs"] else "tests")] += 1 - return counts - - -def group_metrics(decls: list[dict], modules: list[str], result: dict) -> dict: - surface = surface_counts(decls) - live = [d for d in decls if d["sort"] not in ("deprecated", "alias")] - tidy = [d for d in live if d["tidy"] and not d["path"].startswith(TIDY_EXEMPT)] - defs = [d for d in live if d["sort"] in ("definition", "type")] - thms = [d for d in live if d["sort"] == "theorem"] - heads = [d for d in thms if d["headline"]] - drift = [result["doc_drift"][m] for m in modules] - exposed = [d for d in live if d["exported"] == "def" and d["sort"] == "definition" - and d["keyword"] not in ("abbrev", "instance")] - proofs = [p for m in modules for p in result["proofs"][m]] - hubs = sorted(modules, key=lambda m: -len(result["importers"][m])) - return { - "modules": len(modules), "surface": dict(surface), - "tidy_statements": len(tidy), - "tidy_statements_used_outside": sum(d["category"] == "outside" for d in tidy), - "definitions": len(defs), "definitions_undocumented": sum(not d["doc"] for d in defs), - "theorems": len(thms), "theorems_undocumented": sum(not d["doc"] for d in thms), - "listed_theorems": len(heads), - "listed_theorems_undocumented": sum(not d["doc"] for d in heads), - "doc_listed": sum(x["listed"] for x in drift), - "doc_listed_missing": sum(len(x["missing"]) for x in drift), - "doc_listed_private": sum(len(x["private"]) for x in drift), - "doc_listed_elsewhere": sum(len(x["elsewhere"]) for x in drift), - "doc_unlisted_definitions": sum(len(x["unlisted"]) for x in drift), - "modules_without_main_section": sum(not x["has_main"] for x in drift), - "duplicate_theorems": sum(d.get("duplicate") == "thm" for d in decls), - "duplicate_definitions": sum(d.get("duplicate") == "def" for d in decls), - "exposed_definitions": len(exposed), - "exposed_unreferenced_elsewhere": sum(not d["lib_refs"] for d in exposed), - "exposed_not_unfolded_elsewhere": sum(bool(d["lib_refs"]) and not d["unfolded_by"] - and "simp" not in d["attrs"] for d in exposed), - "top_hubs": [(m, len(result["importers"][m]), len(result["fanout"][m])) for m in hubs[:5]], - "proofs": len(proofs), "proofs_at_least_40": sum(p["body_lines"] >= 40 for p in proofs), - "proofs_at_least_100": sum(p["body_lines"] >= 100 for p in proofs), - "longest_proofs": [(p["name"], p["file"], p["body_lines"]) for p in - sorted(proofs, key=lambda p: -p["body_lines"])[:3]], - } - - -def pct(part: int, whole: int) -> str: - return f"{part:,} ({100 * part / whole:.0f}%)" if whole else "0" - - -def area_table(report: dict) -> list[str]: - out = ["| Area | Modules | Public | (a) Never referenced outside module | (b) Tests or " - "abstracts only | (c) Tidy in statements | (d) Undocumented defs · listed thms · all " - "thms | (e) Doc drift: listed missing · unlisted defs | (f) Duplicates: thms · defs | " - "(g) Top hub: importers (rebuild fan-out) | (h) Proofs ≥100 (≥40) lines |", - "|---|--:|--:|--:|--:|--:|--:|--:|--:|--:|--:|"] - for name, g in list(report["areas"].items()) + [("Total", report["totals"])]: - s = g["surface"] - hub = g["top_hubs"][0] if g["top_hubs"] else ("", 0, 0) - out.append( - f"| {name} | {g['modules']:,} | {s['public']:,} | " - f"{pct(s['never_outside'], s['public'])} | {s.get('tests_only', 0):,} | " - f"{g['tidy_statements']:,} | {g['definitions_undocumented']:,} · " - f"{g['listed_theorems_undocumented']:,} / {g['listed_theorems']:,} · " - f"{g['theorems_undocumented']:,} / {g['theorems']:,} | " - f"{g['doc_listed_missing'] + g['doc_listed_private']:,} · " - f"{g['doc_unlisted_definitions']:,} | {g['duplicate_theorems']:,} · " - f"{g['duplicate_definitions']:,} | " - f"{hub[1]:,} ({hub[2]:,}) | {g['proofs_at_least_100']:,} " - f"({g['proofs_at_least_40']:,}) |") - return out - - -def surface_table(groups: dict) -> list[str]: - out = ["| Directory | Public | Used by other library modules | Tests or abstracts only | " - "Never referenced outside module | … used in own module | … implicit-use attribute | " - "… named in docs | … deprecated | … in a public statement | Privatization candidates " - "(thm / def) |", - "|---|--:|--:|--:|--:|--:|--:|--:|--:|--:|--:|"] - for name, g in groups.items(): - s = g["surface"] - out.append( - f"| {name} | {s['public']:,} | {s.get('outside', 0):,} | {s.get('tests_only', 0):,} | " - f"{pct(s['never_outside'], s['public'])} | {s.get('module_only', 0):,} | " - f"{s.get('never_outside_implicit', 0):,} | {s.get('never_outside_doc_named', 0):,} | " - f"{s.get('never_outside_deprecated', 0):,} | {s.get('never_outside_pinned', 0):,} | " - f"{s['candidates']:,} " - f"({s.get('candidate_theorems', 0):,} / {s.get('candidate_definitions', 0):,}) |") - return out - - -def markdown(report: dict, top: int) -> str: - t = report["totals"] - s = t["surface"] - dirty = " with uncommitted changes" if report["dirty"] else "" - out = [f"Revision `{report['revision']}`{dirty} ({report['date']}); build outputs " - f"{report['outputs']}. {t['modules']:,} library modules, {s['public']:,} public " - f"declarations written in source, {report['private_declarations']:,} private ones. " - f"References to the {report['generated_public']:,} public constants Lean generates " - "(constructors, recursors, equation lemmas, `simps` lemmas, …) count for the " - "declaration they come from; structure fields and constructors count for their type.", - "", "### Quality signals by area (#587)", ""] + area_table(report) - out += ["", "Areas (#587): " + "; ".join(f"**{n}** = {d}" for n, d, _ in AREAS) - + f"; **{OTHER_AREA}** = `Init` and any unassigned path. (c) excludes " - f"`{TIDY_EXEMPT}`. (d) lists theorems named in a module's \"Main …\" sections or used " - "by an abstract. (f) counts declarations whose statement is alpha-equivalent to one " - "in another module, and definitions whose type and exposed body both are. (g) counts " - "library modules only.", ""] - out += ["### Public surface by top-level directory (#584)", ""] - out += surface_table({**report["directories"], "Total": t}) - out += ["", - f"\"Tests or abstracts only\": {s.get('tests_only_tests', 0):,} by tests, " - f"{s.get('tests_only_abstracts', 0):,} by abstracts, {s.get('tests_only_both', 0):,} " - "by both. Candidates are never referenced outside their module, carry no attribute " - "through which they can be used without being named (`simp`, `fun_prop`, `aesop`, " - "instances, notation, …), are not named in any module docstring or README, are not " - "deprecated, and are not mentioned by the exported statement or exposed body of a " - "declaration that stays public.", - f"Definitions exposed by `@[expose]` (not instances or abbreviations): " - f"{t['exposed_definitions']:,}. Of these, {t['exposed_unreferenced_elsewhere']:,} are " - "not referenced by any other library module, and " - f"{t['exposed_not_unfolded_elsewhere']:,} more are referenced but never unfolded by " - "name there (`unfold`, `delta`, an element of a `simp`/`rw` list, an equation lemma).", - "", f"### Modules with the most declarations never referenced outside (top {top})", "", - "| Module | Never referenced outside | Candidates | Public | Transitive importers | " - "Rebuild fan-out |", "|---|--:|--:|--:|--:|--:|"] - for row in report["top_modules"][:top]: - out.append(f"| `{row['module'].removeprefix('Complexity.')}` | {row['never_outside']} | " - f"{row['candidates']} | {row['public']} | {row['importers']} | " - f"{row['fanout']} |") - out += ["", f"### Most imported modules (top {top})", "", - "| Module | Transitive importers | Rebuild fan-out | Public | " - "Never referenced outside |", - "|---|--:|--:|--:|--:|"] - for row in report["hubs"][:top]: - out.append(f"| `{row['module'].removeprefix('Complexity.')}` | {row['importers']} | " - f"{row['fanout']} | {row['public']} | {row['never_outside']} |") - out += ["", "Rebuild fan-out: the modules Lake rebuilds when the module's exported interface " - "changes, namely its direct importers and the importers of modules that reexport it " - "through `public import` chains.", "", "Limitations: " + " ".join(report["notes"])] - out += ["", tidy_usage_markdown(report["tidy_usage"], top)] - return "\n".join(out) + "\n" - - -NOTES = [ - "Counts are review signals, not rules: zero in-repository references does not mean that a " - "declaration is unwanted API.", - "Uses through simp sets, instances, fun_prop, Aesop rules, notation and macros leave no " - "reference; such declarations are flagged and never candidates.", - "Definitional unfolding without naming a definition (rfl, decide) is not detected.", - "The guide (#585) is scanned only for S4 source-level tidy signals, not API quality.", -] - - -def build_report(result: dict, top: int) -> dict: - decls = [d for d in result["decls"].values() if d["role"] == "decl"] - by_area, by_dir, by_module = defaultdict(list), defaultdict(list), defaultdict(list) - for d in decls: - by_area[d["area"]].append(d) - by_dir[top_dir(d["path"])].append(d) - by_module[d["module"]].append(d) - modules_by_area, modules_by_dir = defaultdict(list), defaultdict(list) - for m in result["lib_modules"]: - rel = m.removeprefix("Complexity.").replace(".", "/") - modules_by_area[area_of(rel + "/")].append(m) - modules_by_dir[top_dir(rel)].append(m) - revision = run(["git", "rev-parse", "HEAD"], capture_output=True).stdout.strip() - dirty = bool(run(["git", "status", "--porcelain", "--", "Complexity", "ComplexityTests", - "abstracts"], capture_output=True).stdout.strip()) - module_rows = [] - for m in result["lib_modules"]: - s = surface_counts(by_module[m]) - module_rows.append({"module": m, "public": s["public"], "candidates": s["candidates"], - "never_outside": s["never_outside"], - "importers": len(result["importers"][m]), - "fanout": len(result["fanout"][m])}) - order = [name for name, _, _ in AREAS] + [OTHER_AREA] - return { - "revision": revision, "dirty": dirty, "date": datetime.date.today().isoformat(), - "build_dir": str(DEFAULT_BUILD_DIR), "outputs": "", - "notes": NOTES + [f"Proof lengths skip {len(result['proofs_unparsed'])} modules the " - "scanner cannot parse; see `proofs_unparsed`."] * bool( - result["proofs_unparsed"]), - "proofs_unparsed": result["proofs_unparsed"], - "tidy_usage": result["tidy_usage"], - "private_declarations": result["private_count"], - "generated_public": result["generated_public"], - "areas": {a: group_metrics(by_area[a], modules_by_area[a], result) for a in order}, - "directories": {k: group_metrics(by_dir[k], modules_by_dir[k], result) - for k in sorted(modules_by_dir) if by_dir[k]}, - "totals": group_metrics(decls, result["lib_modules"], result), - "top_modules": sorted(module_rows, key=lambda r: (-r["never_outside"], -r["candidates"], - r["module"])), - "hubs": sorted(module_rows, key=lambda r: (-r["importers"], r["module"])), - "duplicates": result["duplicates"], - "doc_drift": {m: x for m, x in result["doc_drift"].items() - if x["missing"] or x["private"] or x["elsewhere"] or x["unlisted"]}, - "declarations": [{k: (sorted(v) if isinstance(v, set) else v) for k, v in d.items() - if k not in ("range", "parent", "role")} for d in decls], - } - - -def main() -> None: - parser = argparse.ArgumentParser(description=__doc__, - formatter_class=argparse.RawDescriptionHelpFormatter) - parser.add_argument("--build-dir", type=Path, default=DEFAULT_BUILD_DIR, - help="read build outputs from here; unless --no-build-check is given, " - "they must equal the current default outputs") - parser.add_argument("--json", type=Path, help="write the full report, with every declaration") - parser.add_argument("--markdown", type=Path, help="write the tables to a file") - parser.add_argument("--top", type=int, default=20) - parser.add_argument("--no-build-check", action="store_true", - help="do not check that the build outputs are current") - args = parser.parse_args() - outputs = check_outputs(args.build_dir, args.no_build_check) - report = build_report(analyse(args.build_dir), args.top) - report["build_dir"], report["outputs"] = str(args.build_dir), outputs - report["tidy_usage"]["provenance"]["outputs"] = outputs - text = markdown(report, args.top) - if args.markdown: - args.markdown.write_text(text) - else: - print(text) - if args.json: - args.json.write_text(json.dumps(report, indent=1, ensure_ascii=False) + "\n") - - -if __name__ == "__main__": - main() diff --git a/scripts/test_audit_queries.py b/scripts/test_audit_queries.py new file mode 100644 index 0000000000..526cc49473 --- /dev/null +++ b/scripts/test_audit_queries.py @@ -0,0 +1,150 @@ +"""Unit tests for scripts/audit_queries.py.""" + +from __future__ import annotations + +import contextlib +import io +import pathlib +import sys +import unittest +from unittest import mock + +sys.path.insert(0, str(pathlib.Path(__file__).resolve().parent)) +import audit_queries as aq # noqa: E402 + + +class HelperTests(unittest.TestCase): + def test_generated_constants_belong_to_their_owner(self) -> None: + owners = {"Foo": "Foo", "Foo.bar": "Foo", "baz": "baz", "Ns.f": "Ns.f"} + self.assertEqual(aq.owner_of("Foo.bar", owners), "Foo") + self.assertEqual(aq.owner_of("baz.eq_1", owners), "baz") + self.assertEqual(aq.owner_of("baz.eq_def", owners), "baz") + self.assertEqual(aq.owner_of("Foo.mk.injEq", owners), "Foo") + self.assertEqual(aq.owner_of("Ns.f._proof_3", owners), "Ns.f") + self.assertEqual(aq.owner_of("Ns.f.match_2.splitter", owners), None) + self.assertIsNone(aq.owner_of("Foo.unrelated", owners)) + self.assertIsNone(aq.owner_of("Mathlib.thing", owners)) + + def test_unfolding_by_name(self) -> None: + self.assertTrue(aq.unfolds_by_name("f.eq_1", "f")) + self.assertTrue(aq.unfolds_by_name("f.eq_def", "f")) + self.assertTrue(aq.unfolds_by_name("f.induct", "f")) + self.assertFalse(aq.unfolds_by_name("f", "f")) + self.assertFalse(aq.unfolds_by_name("f.mk", "f")) + self.assertFalse(aq.unfolds_by_name("fg.eq_1", "f")) + + def test_utf16_columns(self) -> None: + self.assertEqual(aq.utf16_index("abc def", 4), 4) + line = "𝔅 x := foo" # 𝔅 takes two UTF-16 units + self.assertEqual(line[aq.utf16_index(line, 8):], "foo") + self.assertEqual(aq.utf16_index("ℕ → foo", 4), 4) + + def test_unfolding_positions(self) -> None: + def at(before: str, previous: tuple[str, ...] = ()) -> bool: + lines = [*previous, before + "target rest"] + return aq.unfolds_at(lines, len(lines) - 1, len(before)) + + self.assertTrue(at(" unfold ")) + self.assertTrue(at(" unfold other ")) + self.assertTrue(at(" delta ")) + self.assertTrue(at(" simp only [foo, ")) + self.assertTrue(at(" rw [← ")) + self.assertTrue(at(" simp (config := {}) only [")) + self.assertTrue(at(" ", (" simp only [foo,",))) + self.assertFalse(at(" exact ")) + self.assertFalse(at(" rw [sum_coe_sort T fun i => p.")) + self.assertFalse(at(" simp [f ")) + self.assertFalse(at(" rw [show a = b from ")) + self.assertFalse(at(" exact ⟨")) + self.assertFalse(at(" refine foo [")) + + def test_attributes_and_keywords(self) -> None: + keyword, attrs = aq.header_info( + "@[simp, aesop safe apply (rule_sets := [PolyTime]), local instance] theorem foo") + self.assertEqual(keyword, "theorem") + self.assertEqual(attrs, {"simp", "aesop"}) + self.assertEqual(aq.header_info("@[expose] public def bar")[0], "def") + self.assertEqual(aq.header_info("@[deprecated (since := \"2026-10-19\")] alias x")[1], + {"deprecated"}) + self.assertEqual(aq.header_info("noncomputable instance")[0], "instance") + self.assertEqual(aq.attribute_names("scoped simp, simps!"), {"simp", "simps"}) + + def test_name_matching(self) -> None: + self.assertTrue(aq.matches("Cslib.Foo.bar", "Foo.bar")) + self.assertTrue(aq.matches("Cslib.Foo.bar", "Cslib.Foo.bar")) + self.assertFalse(aq.matches("Cslib.Foo.foobar", "bar")) + self.assertTrue(aq.matches("_private.Complexity.A.B.0.Cslib.Foo.bar", "Foo.bar")) + + +def declaration(name: str, line: int, sort: str = "theorem", **refs) -> dict: + return {"name": name, "module": "Complexity.A", "path": "A.lean", "role": "decl", + "range": [line, 0, line, 1, line, 8, line, 9], "sort": sort, "local_uses": 0, + "implicit": [], "lib_refs": set(), "test_refs": set(), "abstract_refs": set(), + **refs} + + +class QueryTests(unittest.TestCase): + def setUp(self) -> None: + self.decls = { + "A.used": declaration("A.used", 3, lib_refs={"Complexity.B", "Complexity.C"}, + test_refs={"ComplexityTests.A"}), + "A.local": declaration("A.local", 5, local_uses=2, implicit=["simp"]), + "A.none": declaration("A.none", 7, sort="definition"), + "A.tested": declaration("A.tested", 9, abstract_refs={"ComplexityAbstracts.X"}), + } + self.decls["B.used"] = {**declaration("B.used", 4), "module": "Complexity.B", + "path": "B.lean"} + + def test_references_list_users_by_role(self) -> None: + self.assertEqual(aq.reference_lines(self.decls, ["Complexity/A.lean"], unused=False), [ + "Complexity/A.lean:3: A.used (theorem): library Complexity.B, Complexity.C; " + "tests ComplexityTests.A", + "Complexity/A.lean:5: A.local (theorem): only its own module " + "[used implicitly through simp?]", + "Complexity/A.lean:7: A.none (definition): nowhere", + "Complexity/A.lean:9: A.tested (theorem): abstracts ComplexityAbstracts.X", + ]) + + def test_unused_keeps_declarations_no_other_module_names(self) -> None: + for decl in self.decls.values(): + decl["category"] = ("outside" if decl["lib_refs"] else "tests_only" + if decl["test_refs"] or decl["abstract_refs"] else "unreferenced") + lines = aq.reference_lines(self.decls, ["Complexity/"], unused=True) + self.assertEqual([line.split(": ")[1].split()[0] for line in lines], + ["A.local", "A.none", "B.used"]) + + def test_duplicates_with_a_member_under_a_prefix(self) -> None: + groups = [{"kind": "thm", "members": [("Complexity.A", "A.used"), + ("Complexity.B", "B.used")]}] + expected = ["alpha-equivalent statements:", " Complexity/A.lean:3: A.used", + " Complexity/B.lean:4: B.used"] + self.assertEqual(aq.duplicate_lines(groups, self.decls, []), expected) + self.assertEqual(aq.duplicate_lines(groups, self.decls, ["Complexity/B"]), expected) + self.assertEqual(aq.duplicate_lines(groups, self.decls, ["Complexity/C"]), []) + + def test_command_line(self) -> None: + for decl in self.decls.values(): + decl["category"] = "outside" if decl["lib_refs"] else "unreferenced" + out = io.StringIO() + with mock.patch.object(aq.lo, "check_outputs"), mock.patch.object(aq.lo, "Library"), \ + mock.patch.object(aq.lo, "collect_declarations", return_value=(self.decls, {})), \ + mock.patch.object(aq, "annotate_headers"), \ + mock.patch.object(aq, "collect_references"), mock.patch.object(aq, "classify"), \ + contextlib.redirect_stdout(out): + self.assertEqual(aq.main(["references", "--unused", "Complexity/B.lean"]), 0) + self.assertEqual(out.getvalue(), "Complexity/B.lean:4: B.used (theorem): nowhere\n") + for argv in (["references"], ["duplicates", "--unused"]): + with self.subTest(argv=argv), self.assertRaises(SystemExit), \ + contextlib.redirect_stderr(io.StringIO()): + aq.main(argv) + + def test_classify(self) -> None: + decl = {**declaration("A.inst", 1), "kind": "def", "keyword": "instance", + "attrs": {"simp"}} + aq.classify({"A.inst": decl}) + self.assertEqual((decl["category"], decl["sort"], decl["implicit"]), + ("unreferenced", "instance", ["simp", "instance"])) + + +if __name__ == "__main__": + unittest.main() diff --git a/scripts/test_check_changed_files.py b/scripts/test_check_changed_files.py index e7d6b0b312..c584fd1282 100644 --- a/scripts/test_check_changed_files.py +++ b/scripts/test_check_changed_files.py @@ -67,6 +67,30 @@ def test_other_sections_and_descriptions_are_not_checked(self) -> None: text = "/-!\n## Implementation notes\n\n* `missing`: x\n\nSee `missing` too.\n-/\n" self.assertEqual(self.check(text), []) + def test_listed_names(self) -> None: + doc = """ +# Title + +Mentions `Ignored.name` in prose. + +## Main definitions + +* `Foo.bar`, `Foo.baz`: two things, related to `NotListed`. +* `Long.first`, + `Long.second`: a bullet continued on the next line. +* `.relative`: a name relative to the previous one. +* `u ≼ v` is notation, not a name. + +## Main results + +* `Foo.bar_spec` + +## References +* `Not.a.result`: references are not listed. +""" + self.assertEqual(c.listed_names(doc), [ + "Foo.bar", "Foo.baz", "Long.first", "Long.second", "relative", "Foo.bar_spec"]) + def test_syntax_names(self) -> None: text = ('syntax (name := foSimp) "fo_simp" (simpArgs)? : tactic\n' 'scoped macro "ppt " : tactic => `(tactic| rfl)\n' diff --git a/scripts/test_check_tidy_surface.py b/scripts/test_check_tidy_surface.py index 0ceb2683af..90fda17e41 100644 --- a/scripts/test_check_tidy_surface.py +++ b/scripts/test_check_tidy_surface.py @@ -1,7 +1,7 @@ """Unit tests for scripts/check_tidy_surface.py, on synthetic build outputs and, when Lean is available, on a compiled module (`CompiledFixtureTests`). -The fixtures have the shape of what `scripts/QualityReport.lean` and the `.ilean` files record for +The fixtures have the shape of what `scripts/LeanOutputs.lean` and the `.ilean` files record for a module like this one, where only `stated`, `exposed` and `Cert.cert` have tidy statements: theorem proved (h : ComputableInPolyTime f e e') : ComputableInPolyTime f e e' := by @@ -30,7 +30,7 @@ def opaqueBody … : Prop := ComputableTidilyInPolyTime f e e' sys.path.insert(0, str(pathlib.Path(__file__).resolve().parent)) import check_tidy_surface as c # noqa: E402 -import quality_report as q # noqa: E402 +import lean_outputs as lo # noqa: E402 TIDY = "Turing.MultiTapeTM.ComputableTidilyInPolyTime" PLAIN = "Turing.MultiTapeTM.ComputableInPolyTime" @@ -73,8 +73,8 @@ def module_fixture(module: str, short: str) -> list[tuple[str, dict, dict | None ] -class FakeLibrary(q.Library): - """`quality_report.Library` over in-memory `.ilean` data and constant rows.""" +class FakeLibrary(lo.Library): + """`lean_outputs.Library` over in-memory `.ilean` data and constant rows.""" def __init__(self, modules: dict[str, list[tuple[str, dict, dict | None]]]): self.ileans, self.constants, self.sources = {}, {}, {} @@ -157,7 +157,7 @@ def run_main(self, baseline: dict[str, int] | None, *flags: str) -> tuple[int, s if baseline is not None: self.baseline.write_text(json.dumps(baseline)) out, err = io.StringIO(), io.StringIO() - with mock.patch.object(q, "Library", lambda _: FakeLibrary(self.modules)), \ + with mock.patch.object(lo, "Library", lambda _: FakeLibrary(self.modules)), \ contextlib.redirect_stdout(out), contextlib.redirect_stderr(err): code = c.main(["--no-build-check", "--allowlist", str(self.allowlist), "--baseline", str(self.baseline), *flags]) @@ -272,7 +272,7 @@ def inType (n : Nat) : {m : Nat // ComputableTidilyFake m} := ⟨n, rfl⟩ @unittest.skipUnless(shutil.which("lake") and (c.ROOT / ".lake/packages").is_dir(), "needs Lean and the repository's packages (CI runs this after the build)") class CompiledFixtureTests(unittest.TestCase): - """The whole count on a compiled module: what `scripts/QualityReport.lean` records as a + """The whole count on a compiled module: what `scripts/LeanOutputs.lean` records as a statement, and what it leaves to proofs.""" @classmethod @@ -288,7 +288,7 @@ def setUpClass(cls) -> None: str(root / "TidyFixture.lean")], cwd=c.ROOT, check=True, capture_output=True) ilean = json.loads((build / "TidyFixture.ilean").read_text()) - constants, _ = q.load_constants(build, ["TidyFixture"]) + constants, _ = lo.load_constants(build, ["TidyFixture"]) cls.constants = constants lib = FakeLibrary({}) lib.ileans, lib.modules, lib.constants = {"TidyFixture": ilean}, ["TidyFixture"], constants diff --git a/scripts/test_lean_outputs.py b/scripts/test_lean_outputs.py new file mode 100644 index 0000000000..e0e6d25b04 --- /dev/null +++ b/scripts/test_lean_outputs.py @@ -0,0 +1,112 @@ +"""Unit tests for scripts/lean_outputs.py.""" + +from __future__ import annotations + +import json +import pathlib +import sys +import tempfile +import unittest + +sys.path.insert(0, str(pathlib.Path(__file__).resolve().parent)) +import lean_outputs as lo # noqa: E402 + + +class ModuleTests(unittest.TestCase): + def test_module_roles(self) -> None: + self.assertEqual(lo.module_role("Complexity.Foundations.Data.List.Basic"), "lib") + self.assertEqual(lo.module_role("ComplexityTests.Smoke"), "test") + self.assertEqual(lo.module_role("ComplexityTests.Abstracts.All"), "abstract") + self.assertEqual(lo.module_role("ComplexityAbstracts.CookLevinBridge"), "abstract") + + +class OutputCheckTests(unittest.TestCase): + def setUp(self) -> None: + tmp = tempfile.TemporaryDirectory() + self.addCleanup(tmp.cleanup) + self.reference = pathlib.Path(tmp.name) / "current" + self.copy = pathlib.Path(tmp.name) / "copy" + for directory in (self.reference, self.copy): + self.write(directory, "Complexity/A.ilean", "{}") + self.write(directory, "Complexity/A.olean", "a") + self.write(directory, "Complexity/A.c", "ignored") + + @staticmethod + def write(directory: pathlib.Path, rel: str, text: str) -> None: + path = directory / rel + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(text) + + def check(self, build_dir: pathlib.Path, skip: bool = False, current: bool = True) -> str: + return lo.check_outputs(build_dir, skip, current=lambda: current, reference=self.reference) + + def test_identical_custom_directory_is_checked(self) -> None: + self.write(self.copy, "Complexity/A.c", "other files do not matter") + self.assertIn("identical", self.check(self.copy)) + self.assertIn("lake build --no-build", self.check(self.reference)) + + def test_stale_custom_directory_is_refused(self) -> None: + # The current outputs gained a declaration that the copied directory lacks. + self.write(self.reference, "Complexity/A.olean", "a with a new declaration") + self.write(self.reference, "Complexity/B.ilean", "{}") + with self.assertRaises(SystemExit) as error: + self.check(self.copy) + self.assertIn("2 file(s)", str(error.exception.code)) + self.assertEqual(lo.output_differences(self.copy, self.reference), + ["Complexity/A.olean", "Complexity/B.ilean"]) + + def test_stale_default_outputs_are_refused(self) -> None: + with self.assertRaises(SystemExit): + self.check(self.reference, current=False) + + def test_stale_root_output_is_refused(self) -> None: + for directory in (self.reference, self.copy): + self.write(directory, "Complexity.ilean", "root") + self.write(self.copy, "Complexity.ilean", "stale root") + self.assertEqual(lo.output_differences(self.copy, self.reference), ["Complexity.ilean"]) + with self.assertRaises(SystemExit): + self.check(self.copy) + + def test_unchecked_reports_say_so(self) -> None: + self.write(self.reference, "Complexity/A.olean", "changed") + self.assertIn("not checked", self.check(self.copy, skip=True)) + + def write_ileans(self, modules: dict[str, list[str]]) -> None: + """Write an `.ilean` file for each module, with the given direct imports.""" + for module, imports in modules.items(): + self.write(self.reference, module.replace(".", "/") + ".ilean", json.dumps( + {"module": module, "directImports": [[i, False, False, False] for i in imports]})) + + def test_outputs_of_deleted_modules_are_ignored(self) -> None: + self.write_ileans({"Complexity": ["Complexity.A"], "ComplexityAbstracts": [], + "Complexity.A": ["Mathlib.Init"], "Complexity.Deleted": []}) + self.assertEqual(list(lo.load_ileans(self.reference, glob=lambda root: [])), + ["Complexity.A"]) + + def test_glob_library_modules_are_read_from_sources(self) -> None: + self.write_ileans({"Complexity": [], "ComplexityAbstracts": [], + "ComplexityTests.T": ["Complexity.B"], "Complexity.B": [], + "ComplexityTests.Stale": []}) + glob = lambda root: ["ComplexityTests.T"] if root == "ComplexityTests" else [] + self.assertEqual(sorted(lo.load_ileans(self.reference, glob=glob)), + ["Complexity.B", "ComplexityTests.T"]) + self.assertEqual(lo.root_modules(glob), + ["Complexity", "ComplexityTests.T", "ComplexityAbstracts"]) + + def test_missing_reachable_output_is_refused(self) -> None: + self.write_ileans({"Complexity": ["Complexity.Live"], "ComplexityAbstracts": [], + "Complexity.Live": ["Complexity.Missing"]}) + with self.assertRaises(SystemExit) as error: + lo.load_ileans(self.reference, glob=lambda root: []) + self.assertIn("Missing.ilean is missing (imported by Complexity.Live)", + str(error.exception.code)) + + def test_missing_root_output_is_refused(self) -> None: + self.write_ileans({"Complexity": []}) + with self.assertRaises(SystemExit) as error: + lo.load_ileans(self.reference, glob=lambda root: []) + self.assertIn("ComplexityAbstracts.ilean is missing (a root)", str(error.exception.code)) + + +if __name__ == "__main__": + unittest.main() diff --git a/scripts/test_list_split_fanout.py b/scripts/test_list_split_fanout.py index e6c1cd47ce..8299940d7f 100644 --- a/scripts/test_list_split_fanout.py +++ b/scripts/test_list_split_fanout.py @@ -2,7 +2,7 @@ import unittest -from list_split_fanout import PREFIX, TOPICS, fixed_scope_counts +from list_split_fanout import PREFIX, TOPICS, fixed_scope_counts, transitive_importers class FixedScopeTests(unittest.TestCase): @@ -19,6 +19,13 @@ def test_new_bridge_is_walked_but_not_counted(self): self.assertEqual(after["Lookup"], 1) self.assertEqual(after["Basic"], 0) + def test_transitive_importers(self): + imports = {"A": [], "B": [("A", False)], "C": [("A", True)], "D": [("C", True)], + "E": [("B", True)], "F": [("D", False)]} + importers = transitive_importers(imports) + self.assertEqual(importers["A"], {"B", "C", "D", "E", "F"}) + self.assertEqual(importers["D"], {"F"}) + if __name__ == "__main__": unittest.main() diff --git a/scripts/test_quality_report.py b/scripts/test_quality_report.py deleted file mode 100644 index e94909a4c8..0000000000 --- a/scripts/test_quality_report.py +++ /dev/null @@ -1,246 +0,0 @@ -"""Unit tests for the pure helpers of scripts/quality_report.py.""" - -from __future__ import annotations - -import json -import pathlib -import sys -import tempfile -import unittest - -sys.path.insert(0, str(pathlib.Path(__file__).resolve().parent)) -import quality_report as q # noqa: E402 - - -class QualityReportTests(unittest.TestCase): - def test_areas_follow_the_program_table(self) -> None: - self.assertEqual(q.area_of("Foundations/Data/List/Basic/"), "Foundations") - self.assertEqual(q.area_of("Probability/PMF/"), "Foundations") - self.assertEqual(q.area_of("Computability/BitString/Basic/"), "Foundations") - self.assertEqual(q.area_of("Computability/Probabilistic/PTM/"), "Machines") - self.assertEqual(q.area_of("Computability/PCP/Basic/"), "Classes") - self.assertEqual(q.area_of("Computability/Circuit/Defs/"), "Circuit") - self.assertEqual(q.area_of("Algorithms/Lean/Queue/"), "WordRAM") - self.assertEqual(q.area_of("Init/"), q.OTHER_AREA) - - def test_areas_assigned_after_the_program_table(self) -> None: - # #587's assignment of the paths its table left out. - for path in ("Computability/GenericRAM/Defs/", "Computability/RAM/Basic/", - "Tactic/PolyTime/"): - self.assertEqual(q.area_of(path), "Machines", path) - self.assertEqual(q.area_of("Computability/BranchingProgram/Defs/"), "Circuit") - for path in ("Computability/Kolmogorov/Basic/", "Computability/MCSP/Basic/", - "Computability/USTCON/Reader/", "Computability/Languages/Regular/", - "MachineLearning/UniformLearning/"): - self.assertEqual(q.area_of(path), "Classes", path) - # A module file named like an assigned directory belongs to it as well. - self.assertEqual(q.area_of("Tactic/"), "Machines") - - def test_module_roles(self) -> None: - self.assertEqual(q.module_role("Complexity.Foundations.Data.List.Basic"), "lib") - self.assertEqual(q.module_role("ComplexityTests.Smoke"), "test") - self.assertEqual(q.module_role("ComplexityTests.Abstracts.All"), "abstract") - self.assertEqual(q.module_role("ComplexityAbstracts.CookLevinBridge"), "abstract") - - def test_generated_constants_belong_to_their_owner(self) -> None: - owners = {"Foo": "Foo", "Foo.bar": "Foo", "baz": "baz", "Ns.f": "Ns.f"} - self.assertEqual(q.owner_of("Foo.bar", owners), "Foo") - self.assertEqual(q.owner_of("baz.eq_1", owners), "baz") - self.assertEqual(q.owner_of("baz.eq_def", owners), "baz") - self.assertEqual(q.owner_of("Foo.mk.injEq", owners), "Foo") - self.assertEqual(q.owner_of("Ns.f._proof_3", owners), "Ns.f") - self.assertEqual(q.owner_of("Ns.f.match_2.splitter", owners), None) - self.assertIsNone(q.owner_of("Foo.unrelated", owners)) - self.assertIsNone(q.owner_of("Mathlib.thing", owners)) - - def test_unfolding_by_name(self) -> None: - self.assertTrue(q.unfolds_by_name("f.eq_1", "f")) - self.assertTrue(q.unfolds_by_name("f.eq_def", "f")) - self.assertTrue(q.unfolds_by_name("f.induct", "f")) - self.assertFalse(q.unfolds_by_name("f", "f")) - self.assertFalse(q.unfolds_by_name("f.mk", "f")) - self.assertFalse(q.unfolds_by_name("fg.eq_1", "f")) - - def test_utf16_columns(self) -> None: - self.assertEqual(q.utf16_index("abc def", 4), 4) - line = "𝔅 x := foo" # 𝔅 takes two UTF-16 units - self.assertEqual(line[q.utf16_index(line, 8):], "foo") - self.assertEqual(q.utf16_index("ℕ → foo", 4), 4) - - def test_unfolding_positions(self) -> None: - def at(before: str, previous: tuple[str, ...] = ()) -> bool: - lines = [*previous, before + "target rest"] - return q.unfolds_at(lines, len(lines) - 1, len(before)) - - self.assertTrue(at(" unfold ")) - self.assertTrue(at(" unfold other ")) - self.assertTrue(at(" delta ")) - self.assertTrue(at(" simp only [foo, ")) - self.assertTrue(at(" rw [← ")) - self.assertTrue(at(" simp (config := {}) only [")) - self.assertTrue(at(" ", (" simp only [foo,",))) - self.assertFalse(at(" exact ")) - self.assertFalse(at(" rw [sum_coe_sort T fun i => p.")) - self.assertFalse(at(" simp [f ")) - self.assertFalse(at(" rw [show a = b from ")) - self.assertFalse(at(" exact ⟨")) - self.assertFalse(at(" refine foo [")) - - def test_attributes_and_keywords(self) -> None: - keyword, attrs = q.header_info( - "@[simp, aesop safe apply (rule_sets := [PolyTime]), local instance] theorem foo") - self.assertEqual(keyword, "theorem") - self.assertEqual(attrs, {"simp", "aesop"}) - self.assertEqual(q.header_info("@[expose] public def bar")[0], "def") - self.assertEqual(q.header_info("@[deprecated (since := \"2026-10-19\")] alias x")[1], - {"deprecated"}) - self.assertEqual(q.header_info("noncomputable instance")[0], "instance") - self.assertEqual(q.attribute_names("scoped simp, simps!"), {"simp", "simps"}) - - def test_listed_names(self) -> None: - doc = """ -# Title - -Mentions `Ignored.name` in prose. - -## Main definitions - -* `Foo.bar`, `Foo.baz`: two things, related to `NotListed`. -* `Long.first`, - `Long.second`: a bullet continued on the next line. -* `.relative`: a name relative to the previous one. -* `u ≼ v` is notation, not a name. - -## Main results - -* `Foo.bar_spec` - -## References -* `Not.a.result`: references are not listed. -""" - self.assertEqual(q.listed_names(doc), [ - "Foo.bar", "Foo.baz", "Long.first", "Long.second", "relative", "Foo.bar_spec"]) - - def test_documentation_in_another_module_protects(self) -> None: - # Module A defines the declarations; only module B's docstring names `docApi`. - names = ["Cslib.Fixture.docApi", "Cslib.Fixture.helper", "Cslib.Other.mono", - "Cslib.Fixture.mono", "Cslib.Fixture.monotone"] - doc_b = "/-! Module B builds on `Cslib.Fixture.docApi` and on `mono`. -/" - named = q.doc_named(names, q.doc_tokens(doc_b)) - self.assertIn("Cslib.Fixture.docApi", named) - self.assertNotIn("Cslib.Fixture.helper", named) - # An ambiguous short name protects every declaration it could denote. - self.assertTrue({"Cslib.Other.mono", "Cslib.Fixture.mono"} <= named) - self.assertNotIn("Cslib.Fixture.monotone", named) - self.assertEqual(q.doc_named(names, q.doc_tokens("`Fixture.docApi`")), - {"Cslib.Fixture.docApi"}) - - def test_name_matching(self) -> None: - self.assertTrue(q.matches("Cslib.Foo.bar", "Foo.bar")) - self.assertTrue(q.matches("Cslib.Foo.bar", "Cslib.Foo.bar")) - self.assertFalse(q.matches("Cslib.Foo.foobar", "bar")) - self.assertTrue(q.matches("_private.Complexity.A.B.0.Cslib.Foo.bar", "Foo.bar")) - self.assertTrue(q.mentioned({"Foo.bar", "x"}, "Cslib.Foo.bar")) - self.assertFalse(q.mentioned({"bar"}, "Cslib.Foo.foobar")) - - def test_rebuild_fanout_follows_public_reexports(self) -> None: - # D publicly imports C, which publicly imports A; B imports A privately; E imports B. - imports = {"A": [], "B": [("A", False)], "C": [("A", True)], "D": [("C", True)], - "E": [("B", True)], "F": [("D", False)]} - fanout = q.rebuild_fanout(imports) - self.assertEqual(fanout["A"], {"B", "C", "D", "F"}) - self.assertEqual(fanout["B"], {"E"}) - importers = q.transitive_importers(imports) - self.assertEqual(importers["A"], {"B", "C", "D", "E", "F"}) - - -class OutputCheckTests(unittest.TestCase): - def setUp(self) -> None: - tmp = tempfile.TemporaryDirectory() - self.addCleanup(tmp.cleanup) - self.reference = pathlib.Path(tmp.name) / "current" - self.copy = pathlib.Path(tmp.name) / "copy" - for directory in (self.reference, self.copy): - self.write(directory, "Complexity/A.ilean", "{}") - self.write(directory, "Complexity/A.olean", "a") - self.write(directory, "Complexity/A.c", "ignored") - - @staticmethod - def write(directory: pathlib.Path, rel: str, text: str) -> None: - path = directory / rel - path.parent.mkdir(parents=True, exist_ok=True) - path.write_text(text) - - def check(self, build_dir: pathlib.Path, skip: bool = False, current: bool = True) -> str: - return q.check_outputs(build_dir, skip, current=lambda: current, reference=self.reference) - - def test_identical_custom_directory_is_checked(self) -> None: - self.write(self.copy, "Complexity/A.c", "other files do not matter") - self.assertIn("identical", self.check(self.copy)) - self.assertIn("lake build --no-build", self.check(self.reference)) - - def test_stale_custom_directory_is_refused(self) -> None: - # The current outputs gained a declaration that the copied directory lacks. - self.write(self.reference, "Complexity/A.olean", "a with a new declaration") - self.write(self.reference, "Complexity/B.ilean", "{}") - with self.assertRaises(SystemExit) as error: - self.check(self.copy) - self.assertIn("2 file(s)", str(error.exception.code)) - self.assertEqual(q.output_differences(self.copy, self.reference), - ["Complexity/A.olean", "Complexity/B.ilean"]) - - def test_stale_default_outputs_are_refused(self) -> None: - with self.assertRaises(SystemExit): - self.check(self.reference, current=False) - - def test_stale_root_output_is_refused(self) -> None: - for directory in (self.reference, self.copy): - self.write(directory, "Complexity.ilean", "root") - self.write(self.copy, "Complexity.ilean", "stale root") - self.assertEqual(q.output_differences(self.copy, self.reference), ["Complexity.ilean"]) - with self.assertRaises(SystemExit): - self.check(self.copy) - - def test_unchecked_reports_say_so(self) -> None: - self.write(self.reference, "Complexity/A.olean", "changed") - self.assertIn("not checked", self.check(self.copy, skip=True)) - - def write_ileans(self, modules: dict[str, list[str]]) -> None: - """Write an `.ilean` file for each module, with the given direct imports.""" - for module, imports in modules.items(): - self.write(self.reference, module.replace(".", "/") + ".ilean", json.dumps( - {"module": module, "directImports": [[i, False, False, False] for i in imports]})) - - def test_outputs_of_deleted_modules_are_ignored(self) -> None: - self.write_ileans({"Complexity": ["Complexity.A"], "ComplexityAbstracts": [], - "Complexity.A": ["Mathlib.Init"], "Complexity.Deleted": []}) - self.assertEqual(list(q.load_ileans(self.reference, glob=lambda root: [])), - ["Complexity.A"]) - - def test_glob_library_modules_are_read_from_sources(self) -> None: - self.write_ileans({"Complexity": [], "ComplexityAbstracts": [], - "ComplexityTests.T": ["Complexity.B"], "Complexity.B": [], - "ComplexityTests.Stale": []}) - glob = lambda root: ["ComplexityTests.T"] if root == "ComplexityTests" else [] - self.assertEqual(sorted(q.load_ileans(self.reference, glob=glob)), - ["Complexity.B", "ComplexityTests.T"]) - self.assertEqual(q.root_modules(glob), - ["Complexity", "ComplexityTests.T", "ComplexityAbstracts"]) - - def test_missing_reachable_output_is_refused(self) -> None: - self.write_ileans({"Complexity": ["Complexity.Live"], "ComplexityAbstracts": [], - "Complexity.Live": ["Complexity.Missing"]}) - with self.assertRaises(SystemExit) as error: - q.load_ileans(self.reference, glob=lambda root: []) - self.assertIn("Missing.ilean is missing (imported by Complexity.Live)", - str(error.exception.code)) - - def test_missing_root_output_is_refused(self) -> None: - self.write_ileans({"Complexity": []}) - with self.assertRaises(SystemExit) as error: - q.load_ileans(self.reference, glob=lambda root: []) - self.assertIn("ComplexityAbstracts.ilean is missing (a root)", str(error.exception.code)) - - -if __name__ == "__main__": - unittest.main() diff --git a/scripts/test_tidy_sweep.py b/scripts/test_tidy_sweep.py index 3b7d0dfe93..acb9c37c36 100644 --- a/scripts/test_tidy_sweep.py +++ b/scripts/test_tidy_sweep.py @@ -32,6 +32,31 @@ def const(tidy=(POLY,), ph: str = "1", e: str = "axiom", tb=()) -> dict: "ph": ph} +class AreaTests(unittest.TestCase): + def test_areas_follow_the_program_table(self) -> None: + self.assertEqual(t.area_of("Foundations/Data/List/Basic/"), "Foundations") + self.assertEqual(t.area_of("Probability/PMF/"), "Foundations") + self.assertEqual(t.area_of("Computability/BitString/Basic/"), "Foundations") + self.assertEqual(t.area_of("Computability/Probabilistic/PTM/"), "Machines") + self.assertEqual(t.area_of("Computability/PCP/Basic/"), "Classes") + self.assertEqual(t.area_of("Computability/Circuit/Defs/"), "Circuit") + self.assertEqual(t.area_of("Algorithms/Lean/Queue/"), "WordRAM") + self.assertEqual(t.area_of("Init/"), t.OTHER_AREA) + + def test_areas_assigned_after_the_program_table(self) -> None: + # #587's assignment of the paths its table left out. + for path in ("Computability/GenericRAM/Defs/", "Computability/RAM/Basic/", + "Tactic/PolyTime/"): + self.assertEqual(t.area_of(path), "Machines", path) + self.assertEqual(t.area_of("Computability/BranchingProgram/Defs/"), "Circuit") + for path in ("Computability/Kolmogorov/Basic/", "Computability/MCSP/Basic/", + "Computability/USTCON/Reader/", "Computability/Languages/Regular/", + "MachineLearning/UniformLearning/"): + self.assertEqual(t.area_of(path), "Classes", path) + # A module file named like an assigned directory belongs to it as well. + self.assertEqual(t.area_of("Tactic/"), "Machines") + + class NameTests(unittest.TestCase): def test_plain_name_replaces_supported_notions_only(self) -> None: self.assertEqual(t.plain_name("A.computableTidilyInPolyTime_foo"), @@ -310,14 +335,14 @@ def test_reindent(self) -> None: def fake_source(text: str, namespaces: set[str]) -> t.SourceFile: src = object.__new__(t.SourceFile) - src.path = t.qr.source_path("M") + src.path = t.lean_outputs.source_path("M") src.text = text src.code, src.mask = masks(text) src.lines = text.split("\n") src.starts = [0] for line in src.lines: src.starts.append(src.starts[-1] + len(line) + 1) - src.commands = [m.start() for m in t.qr.COMMAND_START.finditer(src.mask)] + src.commands = [m.start() for m in t.lean_outputs.COMMAND_START.finditer(src.mask)] src._namespaces, src._scopes = namespaces, None return src @@ -738,22 +763,24 @@ def test_module_paths(self) -> None: class PartialBuildTests(unittest.TestCase): def test_partial_outputs_are_listed(self) -> None: - self.assertEqual(t.qr.listed_modules("module\npublic import A.B\nimport C\n-- import D\n"), - ["A.B", "C"]) + self.assertEqual( + t.lean_outputs.listed_modules("module\npublic import A.B\nimport C\n-- import D\n"), + ["A.B", "C"]) with tempfile.TemporaryDirectory() as tmp: build = pathlib.Path(tmp) - listed = t.qr.listed_modules(t.qr.source_path("Complexity").read_text()) + listed = t.lean_outputs.listed_modules( + t.lean_outputs.source_path("Complexity").read_text()) present = listed[0] path = build / (present.replace(".", "/") + ".ilean") path.parent.mkdir(parents=True) path.write_text(json.dumps({"module": present, "directImports": [], "references": {}, "decls": {}})) missing: list[str] = [] - ileans = t.qr.load_ileans(build, missing) + ileans = t.lean_outputs.load_ileans(build, missing) self.assertEqual(list(ileans), [present]) self.assertIn(listed[1], missing) with self.assertRaises(SystemExit): # strict by default - t.qr.load_ileans(build) + t.lean_outputs.load_ileans(build) def test_partial_outputs_must_be_current(self) -> None: calls = [] @@ -780,17 +807,17 @@ def test_full_names_in_comments(self) -> None: p, src = fake_planner(text, {}, known={"A.computableTidilyInPolyTime_x'"}) p.renames = {"A.computableTidilyInPolyTime_x": "A.computableInPolyTime_x"} p.model.lib = SimpleNamespace(ileans={"M": {}}) - original = t.qr.source_path + original = t.lean_outputs.source_path with tempfile.TemporaryDirectory() as tmp: path = pathlib.Path(tmp) / "M.lean" path.write_text(text) src.path = path p.sources = {path: src} - t.qr.source_path = lambda module: path + t.lean_outputs.source_path = lambda module: path try: p.plan_comments() finally: - t.qr.source_path = original + t.lean_outputs.source_path = original fe = p.files[path] self.assertEqual(t.render(text, fe.replaces, fe.wraps, 0, len(text)), text.replace( "info: 'A.computableTidilyInPolyTime_x'", "info: 'A.computableInPolyTime_x'").replace( diff --git a/scripts/test_tidy_usage.py b/scripts/test_tidy_usage.py index bcd02453d9..32f697125d 100644 --- a/scripts/test_tidy_usage.py +++ b/scripts/test_tidy_usage.py @@ -15,7 +15,7 @@ sys.path.insert(0, str(pathlib.Path(__file__).resolve().parent)) import check_tidy_usage as command -import quality_report as q +import lean_outputs as lo class TidyUsageTests(unittest.TestCase): @@ -24,14 +24,14 @@ def test_private_counts_use_types_not_names_and_exclude_generated_children(self) path = pathlib.Path(directory) / "Source.lean" path.write_text("private theorem plainName : Raw f := proof\n" "private theorem tidyNamed : Plain f := proof\n") - source = q.Source(path) + source = lo.Source(path) raw = {"m": "X", "tidy": ["Raw"], "r": [1, 0, 1, 42, 1, 16, 1, 25]} constants = {"_private.X.0.plainName": raw, "_private.X.0.plainName.eq_1": raw, "_private.X.0.generated": {**raw, "r": None}, "_private.X.0.tidyNamed": {**raw, "tidy": [], "r": [2, 0, 2, 44, 2, 16, 2, 25]}} - found = q.private_tidy_declarations(constants, lambda _: source) + found = command.private_tidy_declarations(constants, lambda _: source) self.assertEqual([r["name"] for r in found["X"]], ["_private.X.0.plainName"]) def test_bridges_mask_nested_comments_and_literals_but_keep_primed_identifiers(self): @@ -44,7 +44,7 @@ def char := '.' theorem g := ComputableInPolyTime.of_tidy h theorem ignored := h.tidy' -- a different identifier ''' - rows = q.tidy_source_signals(text, set())["bridges"] + rows = command.tidy_source_signals(text, set())["bridges"] self.assertEqual(rows, [{"line": 6, "bridge": "tidy"}, {"line": 7, "bridge": "of_tidy"}]) @@ -52,15 +52,15 @@ def test_anonymous_private_instance_counts_once_without_generated_children(self) with tempfile.TemporaryDirectory() as directory: path = pathlib.Path(directory) / "Source.lean" path.write_text("private instance : Raw := proof\n") - source = q.Source(path) + source = lo.Source(path) row = {"m": "X", "tidy": ["Raw"], "r": [1, 0, 1, 31, 1, 8, 1, 16]} owner = "_private.X.0.instProbeFact" constants = {owner: row, owner + ".eq_1": row, owner + "._proof_1": row} - found = q.private_tidy_declarations(constants, lambda _: source) + found = command.private_tidy_declarations(constants, lambda _: source) self.assertEqual([r["name"] for r in found["X"]], [owner]) # Excluding a generated child must not depend on the owner's type being tidy. constants[owner] = {**row, "tidy": []} - self.assertEqual(q.private_tidy_declarations(constants, lambda _: source), {}) + self.assertEqual(command.private_tidy_declarations(constants, lambda _: source), {}) def test_inline_and_command_attributes_count_targets_not_commands(self): text = '''@[local fun_prop] @@ -70,7 +70,7 @@ def test_inline_and_command_attributes_count_targets_not_commands(self): @[fun_prop] theorem global : Raw g := old -- attribute [local fun_prop] phantom ''' - rows = q.tidy_source_signals(text, {"_private.X.0.helper", "Namespace.raw"}, + rows = command.tidy_source_signals(text, {"_private.X.0.helper", "Namespace.raw"}, {"plain"}) self.assertEqual([r["target"] for r in rows["local_tidy_fun_prop"]], ["helper", "helper", "Namespace.raw"]) @@ -82,17 +82,17 @@ def test_multiline_attributes_and_unknown_shape_remain_visible(self): @[local fun_prop] macro "unknown" : term => `(True) ''' - rows = q.tidy_source_signals(text, {"Ns.foo'"}) + rows = command.tidy_source_signals(text, {"Ns.foo'"}) self.assertEqual(rows["local_tidy_fun_prop"][0]["target"], "foo'") self.assertEqual(rows["unresolved_local_fun_prop"], [{"line": 3, "target": None}]) def test_ambiguous_suffix_is_conservative(self): - rows = q.tidy_source_signals("attribute [local fun_prop] rule", {"A.rule", "B.rule"}) + rows = command.tidy_source_signals("attribute [local fun_prop] rule", {"A.rule", "B.rule"}) self.assertEqual(rows["local_tidy_fun_prop"][0]["candidates"], ["A.rule", "B.rule"]) def test_multiline_attribute_targets_stop_at_next_command(self): text = "attribute [local fun_prop]\n first\n second in\nexample : True := by trivial" - rows = q.tidy_source_signals(text, {"Ns.first", "Ns.second"}) + rows = command.tidy_source_signals(text, {"Ns.first", "Ns.second"}) self.assertEqual([r["target"] for r in rows["local_tidy_fun_prop"]], ["first", "second"]) def test_command_has_no_update_or_allow_increase_mode(self): @@ -111,8 +111,9 @@ def test_positive_counts_do_not_fail_or_write_a_baseline(self): report = {"provenance": {"revision": "test"}, "internal_prefixes": [], "modules": [], "totals": {"bridges": 100}, "notes": [], "files_mentioning_tidy": 1} - with patch.object(q, "check_outputs", return_value="unchecked"), \ - patch.object(q, "Library"), patch.object(q, "tidy_usage_report", return_value=report), \ + with patch.object(command, "check_outputs", return_value="unchecked"), \ + patch.object(command, "Library"), \ + patch.object(command, "tidy_usage_report", return_value=report), \ contextlib.redirect_stdout(io.StringIO()): self.assertEqual(command.main([]), 0) self.assertEqual(report["provenance"]["outputs"], "unchecked") @@ -133,14 +134,14 @@ def test_three_authored_private_tidy_declarations_include_anonymous_instance(sel "private theorem namedTheorem : ComputableTidilyProbe 2 := by trivial\n") subprocess.run(["lake", "env", "lean", "-DwarningAsError=true", "-R", str(root), str(src), "-o", str(root / "AnonymousInstance.olean"), "-i", - str(root / "AnonymousInstance.ilean")], cwd=q.ROOT, check=True, + str(root / "AnonymousInstance.ilean")], cwd=lo.ROOT, check=True, capture_output=True, text=True) - result = subprocess.run(["lake", "env", "lean", "--run", "scripts/QualityReport.lean", - str(root)], cwd=q.ROOT, input="AnonymousInstance\n", + result = subprocess.run(["lake", "env", "lean", "--run", "scripts/LeanOutputs.lean", + str(root)], cwd=lo.ROOT, input="AnonymousInstance\n", text=True, capture_output=True, check=True) constants = {row["n"]: row for line in result.stdout.splitlines() if "n" in (row := json.loads(line))} - found = q.private_tidy_declarations(constants, lambda _: q.Source(src)) + found = command.private_tidy_declarations(constants, lambda _: lo.Source(src)) self.assertEqual(len(found["AnonymousInstance"]), 3) self.assertTrue(any("instProbeFact" in row["name"] for row in found["AnonymousInstance"])) @@ -153,23 +154,23 @@ def test_classic_and_split_private_metadata_and_incomplete_split_rejection(self) "private theorem hidden : ComputableTidilyProbe 0 := by trivial\n") subprocess.run(["lake", "env", "lean", "-R", str(root), str(src), "-o", str(root / (module + ".olean")), "-i", - str(root / (module + ".ilean"))], cwd=q.ROOT, check=True, + str(root / (module + ".ilean"))], cwd=lo.ROOT, check=True, capture_output=True, text=True) - cmd = ["lake", "env", "lean", "--run", "scripts/QualityReport.lean", str(root)] - result = subprocess.run(cmd, cwd=q.ROOT, input="Classic\nSplit\n", text=True, + cmd = ["lake", "env", "lean", "--run", "scripts/LeanOutputs.lean", str(root)] + result = subprocess.run(cmd, cwd=lo.ROOT, input="Classic\nSplit\n", text=True, capture_output=True, check=True) rows = [json.loads(line) for line in result.stdout.splitlines()] hidden = [r for r in rows if r.get("n", "").endswith(".hidden")] self.assertEqual({r["m"] for r in hidden}, {"Classic", "Split"}) self.assertTrue(all(r["tidy"] and r["r"] for r in hidden)) (root / "Split.olean.server").unlink() - failure = subprocess.run(cmd, cwd=q.ROOT, input="Split\n", text=True, + failure = subprocess.run(cmd, cwd=lo.ROOT, input="Split\n", text=True, capture_output=True) self.assertNotEqual(failure.returncode, 0) self.assertIn("incomplete split module outputs", failure.stderr) # Both missing parts must not be misread as a valid classic module either. (root / "Split.olean.private").unlink() - failure = subprocess.run(cmd, cwd=q.ROOT, input="Split\n", text=True, + failure = subprocess.run(cmd, cwd=lo.ROOT, input="Split\n", text=True, capture_output=True) self.assertNotEqual(failure.returncode, 0) self.assertIn("incomplete split module outputs", failure.stderr) diff --git a/scripts/tidy_sweep.py b/scripts/tidy_sweep.py index 8343ee4339..0089863bd1 100644 --- a/scripts/tidy_sweep.py +++ b/scripts/tidy_sweep.py @@ -59,8 +59,8 @@ `--diff` writes the plan as a patch instead of rewriting files. `report --partial` analyses a tree that does not build completely, listing the modules without outputs. -Declarations, statements and references come from `scripts/quality_report.py` and -`scripts/QualityReport.lean`, which read the build outputs of +Declarations, statements and references come from `scripts/lean_outputs.py`, +`scripts/audit_queries.py` and `scripts/LeanOutputs.lean`, which read the build outputs of `lake build Complexity ComplexityTests ComplexityAbstracts`. """ @@ -79,10 +79,44 @@ ROOT = Path(__file__).resolve().parents[1] sys.path.insert(0, str(ROOT / "scripts")) -import quality_report as qr # noqa: E402 +import audit_queries as aq # noqa: E402 +import lean_outputs # noqa: E402 from proof_lengths import masks # noqa: E402 ALLOWLIST = ROOT / "scripts/tidy_allowlist.txt" +# Documents outside the libraries whose mentions of renamed declarations are rewritten too. +EXTERNAL_DOCS = ("README.md", "abstracts/README.md") +# The areas of #587 that the report groups declarations by: its table, completed by its +# assignment of the remaining paths +# (https://github.com/cslib-community/complexitylib/issues/587#issuecomment-6376302681). +AREAS = [ + ("Foundations", "Foundations, Probability, Languages, Computability/BitString", + ("Foundations/", "Probability/", "Languages/", "Computability/BitString/")), + ("Machines", "Computability/Machines, Probabilistic, RAM, GenericRAM; Tactic", + ("Computability/Machines/", "Computability/Probabilistic/", "Computability/RAM/", + "Computability/GenericRAM/", "Tactic/")), + ("Classes", "Computability/Complexity, PCP, Communication, DecisionTree, QueryComplexity, " + "TreeEval, Kolmogorov, MCSP, USTCON, Languages; MachineLearning", + ("Computability/Complexity/", "Computability/PCP/", "Computability/Communication/", + "Computability/DecisionTree/", "Computability/QueryComplexity/", "Computability/TreeEval/", + "Computability/Kolmogorov/", "Computability/MCSP/", "Computability/USTCON/", + "Computability/Languages/", "MachineLearning/")), + ("Circuit", "Computability/Circuit, BranchingProgram", + ("Computability/Circuit/", "Computability/BranchingProgram/")), + ("Crypto", "Crypto", ("Crypto/",)), + ("Logics", "Logics", ("Logics/",)), + ("WordRAM", "Computability/WordRAM, Algorithms", ("Computability/WordRAM/", "Algorithms/")), +] +OTHER_AREA = "Other" # `Init.lean` and unassigned paths + + +def area_of(path: str) -> str: + """The #587 area of a library source path relative to `Complexity/`.""" + for name, _, prefixes in AREAS: + if path.startswith(prefixes): + return name + return OTHER_AREA + TM = "Turing.MultiTapeTM." @@ -138,7 +172,7 @@ def plain_name(name: str) -> str: def is_tidy_constant(name: str) -> bool: - """Mirror of `isTidy` in `scripts/QualityReport.lean`.""" + """Mirror of `isTidy` in `scripts/LeanOutputs.lean`.""" last = name.rsplit(".", 1)[-1] return last.startswith(("ComputableTidily", "ComputesTidily", "IsTidy")) @@ -355,7 +389,7 @@ def check_partial_outputs(modules: list[str], runner=subprocess.run) -> None: text=True) if check.returncode: sys.exit("the outputs of some built modules are stale; rebuild them (for instance " - "`lake build " + " ".join(qr.ROOTS) + "`) and retry") + "`lake build " + " ".join(lean_outputs.ROOTS) + "`) and retry") class Model: @@ -365,18 +399,20 @@ def __init__(self, build_dir: Path, allowlist: set[str], partial: bool = False, check: bool = True): pairs = ",".join(f"{n.tidy}={n.plain}" for n in NOTIONS) self.missing: list[str] | None = [] if partial else None - self.lib = qr.Library(build_dir, pairs, self.missing) + self.lib = lean_outputs.Library(build_dir, pairs, self.missing) if partial and check: check_partial_outputs(sorted(self.lib.ileans)) self.constants = self.lib.constants - self.decls, self.owners, _ = qr.collect_declarations(self.lib) - qr.annotate_headers(self.lib, self.decls) - qr.collect_references(self.lib, self.decls, self.owners) - qr.classify(self.decls) + self.decls, self.owners = lean_outputs.collect_declarations(self.lib) + for decl in self.decls.values(): + decl["area"] = area_of(decl["path"].removesuffix(".lean") + "/") + aq.annotate_headers(self.lib, self.decls) + aq.collect_references(self.lib, self.decls, self.owners) + aq.classify(self.decls) self.allowlist = allowlist - roots = sorted(self.lib.ileans) if partial else qr.root_modules() - out = qr.run(["lake", "env", "lean", "--run", "scripts/QualityReport.lean", "--names", - *roots], capture_output=True).stdout + roots = sorted(self.lib.ileans) if partial else lean_outputs.root_modules() + out = lean_outputs.run(["lake", "env", "lean", "--run", "scripts/LeanOutputs.lean", + "--names", *roots], capture_output=True).stdout names, _, tokens = out.partition("\n--tokens--\n") self.names, self.tokens = set(names.split()), set(tokens.split("\n")) - {""} self._users: dict[str, list[tuple[str, list]]] | None = None @@ -411,7 +447,7 @@ def known(self) -> set[str]: # --- Report ------------------------------------------------------------------------------------- -AREA_ORDER = [name for name, _, _ in qr.AREAS] + [qr.OTHER_AREA] +AREA_ORDER = [name for name, _, _ in AREAS] + [OTHER_AREA] def summary(entries: list[Entry]) -> dict: @@ -439,8 +475,8 @@ def markdown_report(report: dict, limit: int = 40) -> str: f"Allowlist: {report['allowlist_size']} modules. Plain twins of tidy theorems: " f"{twins}{registry}.", ""] if report.get("missing") is not None: - by_area = Counter(qr.area_of(m.removeprefix("Complexity.").replace(".", "/") + "/") - if m.startswith("Complexity.") else qr.module_role(m) + by_area = Counter(area_of(m.removeprefix("Complexity.").replace(".", "/") + "/") + if m.startswith("Complexity.") else lean_outputs.module_role(m) for m in report["missing"]) out += [f"**Partial build:** {len(report['missing'])} modules have no build outputs and " "are not analysed (" + ", ".join(f"{a} {n}" for a, n in by_area.most_common()) @@ -481,7 +517,7 @@ def markdown_report(report: dict, limit: int = 40) -> str: # --- Lean source helpers (unit-tested in scripts/test_tidy_sweep.py) ---------------------------- OPENERS, CLOSERS = "([{⦃⟨‹", ")]}⦄⟩›" -IDENT = re.compile(qr.IDENT.pattern) +IDENT = re.compile(lean_outputs.IDENT.pattern) KEYWORDS = {"by", "fun", "λ", "with", "at", "using", "from", "then", "else", "do", "in", "if", "match", "show", "have", "let", "calc", "only", "generalizing", "says", "where", "deriving", "termination_by", "decreasing_by", "obtain", "rcases", "refine", "exact"} @@ -706,7 +742,7 @@ def collapse(text: str) -> str: def notation_tokens(text: str, mask: str) -> set[str]: """The tokens the notation, syntax and macro commands of a source declare: the string literals of each whole command, across continuation lines.""" - starts = [m.start() for m in qr.COMMAND_START.finditer(mask)] + [len(mask)] + starts = [m.start() for m in lean_outputs.COMMAND_START.finditer(mask)] + [len(mask)] tokens = set() for start, end in zip(starts, starts[1:]): if NOTATION_COMMAND.match(mask, start): @@ -790,7 +826,7 @@ def __init__(self, mask: str, namespaces: set[str], text: str | None = None): self.once: list[tuple[int, int, tuple[Open, ...], frozenset[str]]] = [] # frames: [kind, name, opens, aliases, variables] stack: list[list] = [["file", "", [], set(), set()]] - starts = [m.start() for m in qr.COMMAND_START.finditer(mask)] + [len(mask)] + starts = [m.start() for m in lean_outputs.COMMAND_START.finditer(mask)] + [len(mask)] self.tokens = by_first(notation_tokens(text if text is not None else mask, mask)) def namespace() -> str: @@ -1158,7 +1194,7 @@ def __init__(self, path: Path, namespaces: set[str]): self.starts = [0] for line in self.lines: self.starts.append(self.starts[-1] + len(line) + 1) - self.commands = [m.start() for m in qr.COMMAND_START.finditer(self.mask)] + self.commands = [m.start() for m in lean_outputs.COMMAND_START.finditer(self.mask)] self._namespaces = namespaces self._scopes: Scopes | None = None @@ -1170,7 +1206,7 @@ def scopes(self) -> Scopes: def at(self, line: int, column16: int) -> int: """The offset of a 0-based line and UTF-16 column (`.ilean` positions).""" - return self.starts[line] + qr.utf16_index(self.lines[line], column16) + return self.starts[line] + aq.utf16_index(self.lines[line], column16) def at_range(self, line: int, column: int) -> int: """The offset of a 1-based line and code-point column (declaration ranges).""" @@ -1264,7 +1300,7 @@ def source(self, path: Path) -> SourceFile: def refs(self, module: str) -> list[Ref]: if module not in self._refs: - src = self.source(qr.source_path(module)) + src = self.source(lean_outputs.source_path(module)) out = [] for name, _, info in self.model.lib.references(module): for u in info["usages"]: @@ -1274,7 +1310,7 @@ def refs(self, module: str) -> list[Ref]: return self._refs[module] def ref_kind(self, name: str) -> str: - owner = qr.owner_of(name, self.model.owners) or name + owner = aq.owner_of(name, self.model.owners) or name if name in BY_TIDY: return "pred" if owner in self.renames: @@ -1291,7 +1327,7 @@ def ref_kind(self, name: str) -> str: def new_name(self, name: str) -> str: if name in BY_TIDY: return BY_TIDY[name].plain - owner = qr.owner_of(name, self.model.owners) or name + owner = aq.owner_of(name, self.model.owners) or name if owner in self.renames and (name == owner or name.startswith(owner + ".")): return self.renames[owner] + name[len(owner):] return self.twins.get(name, name) @@ -1478,7 +1514,7 @@ def defer_statements(self, analyses: dict) -> None: if name in self.deferred or a is None: continue reasons = [f"statement names deferred `{x.name}`" for x in a["sig_refs"] - if (qr.owner_of(x.name, self.model.owners) or x.name) + if (aq.owner_of(x.name, self.model.owners) or x.name) in self.deferred] if reasons: self.deferred[name] = reasons @@ -1487,7 +1523,7 @@ def defer_statements(self, analyses: dict) -> None: def analyse_decl(self, entry: Entry) -> dict | None: """Parse a declaration and find what prevents restating it.""" decl = self.model.decls[entry.name] - module, path = decl["module"], qr.source_path(decl["module"]) + module, path = decl["module"], lean_outputs.source_path(decl["module"]) if not decl["range"]: return None src = self.source(path) @@ -1525,7 +1561,7 @@ def captures(self, old: str, new: str) -> list[str]: if other in (old, new): continue for module, u in self.model.users(other): - path = qr.source_path(module) + path = lean_outputs.source_path(module) src = self.source(path) start, end = src.at(u[0], u[1]), src.at(u[2], u[3]) token = src.text[start:end].removeprefix("@") @@ -1549,7 +1585,7 @@ def plan_bridges(self) -> None: for module, name in sorted(self.bridge): if name in self.deferred: continue - path = qr.source_path(module) + path = lean_outputs.source_path(module) src = self.source(path) ranges = self.model.lib.ileans.get(module, {}).get("decls", {}) if name.startswith("line:"): @@ -1576,7 +1612,7 @@ def plan_bridges(self) -> None: def defer(self, name: str, a: dict | None) -> None: """A declaration left tidy in this batch; references to it stay unchanged.""" decl = self.model.decls[name] - path = qr.source_path(decl["module"]) + path = lean_outputs.source_path(decl["module"]) self.decls[name] = {"name": name, "target": self.batch[name].target, "path": str(path.relative_to(ROOT)), "line": decl["range"][0] if decl["range"] else 0, @@ -1732,7 +1768,7 @@ def in_batch_decl(self, module: str, offset: int) -> str | None: def plan_clients(self, name: str) -> None: for module, u in self.model.users(name): - path = qr.source_path(module) + path = lean_outputs.source_path(module) src = self.source(path) start, end = src.at(u[0], u[1]), src.at(u[2], u[3]) if self.in_batch_decl(module, start): @@ -1841,8 +1877,8 @@ def plan_comments(self) -> None: for name in self.known: if name.rsplit(".", 1)[-1] in by_last: known_by_last[name.rsplit(".", 1)[-1]].append(name) - paths = [qr.source_path(m) for m in self.model.lib.ileans] + \ - [ROOT / doc for doc in qr.EXTERNAL_DOCS] + paths = [lean_outputs.source_path(m) for m in self.model.lib.ileans] + \ + [ROOT / doc for doc in EXTERNAL_DOCS] for path in paths: if not path.exists() or not lasts.search(path.read_text(encoding="utf-8")): continue @@ -1874,7 +1910,7 @@ def resolve_doc_token(self, src: SourceFile, offset: int, token: str, """The constant a documentation token names: the only one it is a suffix of, or the one it resolves to from the comment's namespace and opened namespaces.""" candidates = [n for n in known_by_last.get(token.rsplit(".", 1)[-1], ()) - if qr.matches(n, token)] + if aq.matches(n, token)] if len(candidates) <= 1: return candidates[0] if candidates else None if src.path.suffix != ".lean": @@ -1912,7 +1948,7 @@ def imports_of(module: str) -> set[str]: direct = ileans.get(module, {}).get("directImports", []) public = {module}.union(*(closure(d) for d, private, *_ in direct if not private)) available = public.union(*(closure(d) for d, *_ in direct)) - path = qr.source_path(module) + path = lean_outputs.source_path(module) src = self.source(path) is_module = re.search(r"(?m)^module\s*$", src.mask) is not None for dep, want_public in sorted(needed.items()): @@ -2100,10 +2136,10 @@ def declaration_at(text: str, line: int) -> str: or attributes before a declaration belongs to it.""" mask = masks(text)[1] offset = sum(len(x) + 1 for x in text.split("\n")[:line - 1]) - after = next((m.start() for m in qr.COMMAND_START.finditer(mask, offset)), len(mask)) + after = next((m.start() for m in lean_outputs.COMMAND_START.finditer(mask, offset)), len(mask)) if not mask[offset:after].strip() or mask[offset:after].lstrip().startswith("@["): offset = after - starts = [m.start() for m in qr.COMMAND_START.finditer(mask) if m.start() <= offset] + starts = [m.start() for m in lean_outputs.COMMAND_START.finditer(mask) if m.start() <= offset] for start in reversed(starts): header = DECL_HEADER.search(mask, start, max(offset + 1, start + 400)) if header: @@ -2143,7 +2179,7 @@ def rewrite(model: Model, entries: list[Entry], twins: dict[str, str], area: str path.write_text(text, encoding="utf-8") if not verify: return planner, None - code, output = build(list(qr.ROOTS)) + code, output = build(list(lean_outputs.ROOTS)) result = check_build(planner, texts, output, code, round_) history.append({k: result[k] for k in ("round", "status", "failing", "forced_wrap", "failing_clients")}) @@ -2203,7 +2239,7 @@ def client_decl(planner: Planner, path: Path, text: str, texts: dict[Path, str], return None module = module_of(path) names = [n for n in planner.model.lib.ileans.get(module, {}).get("decls", {}) - if header and qr.matches(n, header)] + if header and aq.matches(n, header)] if len(names) == 1: return module, names[0] at = command_line(text, line) - 1 @@ -2217,7 +2253,7 @@ def command_line(text: str, line: int) -> int: """The 1-based line where the command containing a 1-based line starts.""" mask = masks(text)[1] offset = sum(len(x) + 1 for x in text.split("\n")[:line - 1]) - starts = [m.start() for m in qr.COMMAND_START.finditer(mask) if m.start() <= offset] + starts = [m.start() for m in lean_outputs.COMMAND_START.finditer(mask) if m.start() <= offset] return text.count("\n", 0, starts[-1]) + 1 if starts else line @@ -2250,7 +2286,7 @@ def main(argv: list[str] | None = None) -> int: parser.add_argument("--registry", type=Path, help="extra original → twin pairs from a migration script (JSON)") parser.add_argument("--allowlist", type=Path, default=ALLOWLIST) - parser.add_argument("--build-dir", type=Path, default=qr.DEFAULT_BUILD_DIR) + parser.add_argument("--build-dir", type=Path, default=lean_outputs.DEFAULT_BUILD_DIR) parser.add_argument("--no-build-check", action="store_true", help="report only: do not check that the build outputs are current") parser.add_argument("--partial", action="store_true", @@ -2288,8 +2324,8 @@ def main(argv: list[str] | None = None) -> int: parser.error(str(error)) outputs = ("partial; every loaded module checked current by `lake build --no-build`" if args.partial and not args.no_build_check - else qr.check_outputs(args.build_dir, args.no_build_check or args.partial)) - if args.partial and args.build_dir.resolve() != qr.DEFAULT_BUILD_DIR.resolve() \ + else lean_outputs.check_outputs(args.build_dir, args.no_build_check or args.partial)) + if args.partial and args.build_dir.resolve() != lean_outputs.DEFAULT_BUILD_DIR.resolve() \ and not args.no_build_check: parser.error("--partial checks the default build directory; pass --no-build-check " "to report on another one unchecked") @@ -2298,9 +2334,10 @@ def main(argv: list[str] | None = None) -> int: twins = twin_map(model.constants, registry) entries = classify_all(model, twins) shown = [e for e in entries if not args.area or e.area in args.area] - revision = qr.run(["git", "rev-parse", "HEAD"], capture_output=True).stdout.strip() - dirty = bool(qr.run(["git", "status", "--porcelain", "--", "Complexity", "ComplexityTests", - "abstracts"], capture_output=True).stdout.strip()) + revision = lean_outputs.run(["git", "rev-parse", "HEAD"], capture_output=True).stdout.strip() + dirty = bool(lean_outputs.run(["git", "status", "--porcelain", "--", "Complexity", + "ComplexityTests", "abstracts"], + capture_output=True).stdout.strip()) report = {"revision": revision, "dirty": dirty, "outputs": outputs, "allowlist_size": len(model.allowlist), "registry": str(args.registry) if args.registry else None, From 784a9ba1fbcda448e953a39e3e08518bee87743d Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 22:57:45 -0400 Subject: [PATCH 2/2] doc(contributing): say that the audit helper is not a privatization driver Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- CONTRIBUTING.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index bb518ddd1a..4676b5b127 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -94,7 +94,8 @@ also loads private information, so such edits do reach its clients. - For an audit, `python3 scripts/audit_queries.py references PREFIX` lists where each declaration under a source path is referenced, and `duplicates` lists declarations with alpha-equivalent statements in different modules. Uses through `rfl`, `decide`, simp sets or instances leave no - reference. It is an on-demand helper, never run in CI. + reference, and a declaration nobody references may still be wanted API: privatize by intent + (#926), not because the helper lists it. It is an on-demand helper, never run in CI. Tidy computability (`ComputableTidily…`, `ComputesTidily…`, `IsTidy…`) may appear anywhere inside proofs, through `.tidy`, `.of_tidy`, a proof-local `attribute [local fun_prop] … in` or a tidy