From 7b23d77737a4d4b82da3bbf362b9a2c58ba4ebad Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sun, 25 Oct 2026 18:37:57 +0000 Subject: [PATCH 1/2] ci(scripts): check_pr_names follow-ups from #1092 review (#1086) - Keep hypothesis-shaped tokens (hasCollision, hamPath) as candidates; drop them only when undeclared and mentioned in the sources. - Resolve module, script and generated field-notation names before reading sources, and read a qualified token's head only for generated names and field notation, so Nat.foo no longer reads every file mentioning Nat. - Read base files with one git cat-file --batch instead of a git show each. - Run lean --print-prefix in the checked root; skip _-led fragments; skip attribute names such as to_additive; disable commit signing in the test. Authored by worker-jetski-d75789e1 (AI agent). --- scripts/check_pr_names.py | 122 ++++++++++++++++++++++----------- scripts/test_check_pr_names.py | 30 ++++++-- 2 files changed, 105 insertions(+), 47 deletions(-) diff --git a/scripts/check_pr_names.py b/scripts/check_pr_names.py index 8fddd39fd..63fb05245 100644 --- a/scripts/check_pr_names.py +++ b/scripts/check_pr_names.py @@ -18,8 +18,9 @@ * it skips fenced code blocks, HTML comments and tokens that are not names: expressions with spaces or operators, numbers and hashes, file names, all-caps words, Lean keywords and tactic - names, single letters and lowercase words without an underscore (`simp`, `trace`, `ε`), which - are usually variables or prose; hypothesis names such as `hx` or `h_le` are skipped as well; + names, single letters, `_`-led fragments and lowercase words without an underscore (`simp`, + `trace`, `ε`), which are usually variables or prose; a name shaped like a hypothesis (`hfA`, + `h_le`) is dropped from the report when it is not declared but occurs in the sources; * a declaration's full name combines its `namespace` blocks with its declared name, and a token is declared when it equals a full name or is a dot-separated suffix of one (`Nodup` and `List.Nodup` both match `List.Nodup`); a namespace name matches its `namespace` block or any @@ -89,7 +90,8 @@ "split_ifs", "nlinarith", "decide_eq_true", "ring_nf", "set_option", "maxHeartbeats", "maxRecDepth", "autoImplicit", "relaxedAutoImplicit", "check_abstract", "print_axioms", "lake", "mk_all", "lint_style", "checkInitImports", "runLinter", "pull_request", - "merge_group", "workflow_dispatch", + "merge_group", "workflow_dispatch", "to_additive", "to_dual", "simps", "irreducible_def", + "fun_prop", "reducible_and_instances", } @@ -113,6 +115,8 @@ def is_candidate(token: str) -> bool: if not NAME.match(token): return False bare = token.lstrip(".").removeprefix("_root_.") + if bare.startswith("_"): + return False # a fragment such as `_leaf_le` parts = bare.split(".") if len(parts) > 1 and parts[-1].lower() in FILE_SUFFIXES: return False @@ -124,7 +128,7 @@ def is_candidate(token: str) -> bool: if letters and all(c.isupper() for c in letters) and len(letters) > 1: return False # environment variables and acronyms: `GITHUB_EVENT_PATH`, `PRF` if len(parts) == 1: - if len(bare) < 2 or HYPOTHESIS.match(bare): + if len(bare) < 2: return False if "_" not in bare and not any(c.isupper() for c in bare): return False # lowercase prose, variables and tactics: `simp`, `trace`, `ε` @@ -133,7 +137,8 @@ def is_candidate(token: str) -> bool: # --- Reading declarations from Lean sources ------------------------------------------------------- -MODIFIERS = r"(?:(?:private|protected|public|noncomputable|partial|unsafe|nonrec|scoped|local|meta)\s+)*" +MODIFIERS = (r"(?:(?:private|protected|public|noncomputable|partial|unsafe|nonrec|scoped|local|" + r"meta)\s+)*") ATTRS = r"(?:@\[[^\]]*\]\s*)*" IDENT = r"[^\s:({\[⦃⟨,|@]+" DECL = re.compile( @@ -203,7 +208,8 @@ def add(self, full: str) -> None: def declared(self, token: str) -> bool: """Whether `token` names a declaration, as a full name or a dotted suffix of one.""" last = token.rsplit(".", 1)[-1] - return any(full == token or full.endswith("." + token) for full in self.by_last.get(last, ())) + return any(full == token or full.endswith("." + token) + for full in self.by_last.get(last, ())) def namespace(self, token: str) -> bool: return any(ns == token or ns.endswith("." + token) for ns in self.namespaces @@ -314,7 +320,7 @@ def full(name: str) -> str: awaiting_where = not re.search(r"(^|\s)where\s*$", rest) -# --- Finding the sources ---------------------------------------------------------------------------- +# --- Finding the sources -------------------------------------------------------------------------- def source_roots(root: Path, core: bool = True) -> list[Path]: """Directories whose `.lean` files are searched for declarations.""" @@ -324,8 +330,8 @@ def source_roots(root: Path, core: bool = True) -> list[Path]: roots += sorted(p for p in packages.iterdir() if p.is_dir()) if core and shutil.which("lean"): try: - prefix = subprocess.run(["lean", "--print-prefix"], capture_output=True, text=True, - timeout=60).stdout.strip() + prefix = subprocess.run(["lean", "--print-prefix"], cwd=root, capture_output=True, + text=True, timeout=60).stdout.strip() except (OSError, subprocess.SubprocessError): prefix = "" src = Path(prefix) / "src" / "lean" if prefix else None @@ -367,7 +373,7 @@ def files_mentioning(roots: list[Path], words: set[str]) -> list[Path]: return found -# --- Resolving tokens ------------------------------------------------------------------------------- +# --- Resolving tokens ----------------------------------------------------------------------------- def additive_variants(token: str) -> set[str]: """Multiplicative names from which Mathlib's `to_additive` could have generated `token`.""" @@ -383,21 +389,31 @@ def additive_variants(token: str) -> set[str]: def search_words(token: str) -> set[str]: - """Words whose files must be read to resolve `token`.""" + """Words whose files must be read to resolve `token` as a declaration in its own right.""" bare = token.lstrip(".").removeprefix("_root_.") - parts = bare.split(".") - words = {parts[-1].rstrip("'!?")} - if len(parts) > 1: - words.add(parts[-2].rstrip("'!?")) - if m := SIMPS_SUFFIX.match(parts[-1]): - words.add(m.group(1)) - elif m := SIMPS_SUFFIX.match(bare): + last = bare.rsplit(".", 1)[-1] + words = {last.rstrip("'!?")} + if m := SIMPS_SUFFIX.match(last): words.add(m.group(1)) for variant in additive_variants(bare): words.add(variant.rsplit(".", 1)[-1].rstrip("'!?")) return {w for w in words if w} +def head_words(token: str) -> set[str]: + """Words whose files are also needed when `token` is a generated name (`Pair.mk`) or field + notation on a theorem (`foo_iff.mp`): the last component of its head. + + Only these tokens look at the head, so that a qualified name in a large namespace (`Nat.foo`) + does not read every file mentioning `Nat`.""" + parts = token.lstrip(".").removeprefix("_root_.").split(".") + if len(parts) < 2: + return set() + head, last = parts[-2], parts[-1] + generated = last in GENERATED or re.fullmatch(r"eq_\d+|proof_\d+|match_\d+", last) + return {head.rstrip("'!?")} if generated or head[:1].islower() else set() + + def module_suffixes(roots: list[Path]) -> set[str]: """Every dotted suffix of the module names of the `.lean` files under `roots`. @@ -503,10 +519,21 @@ def base_declarations(root: Path, base: str, words: set[str]) -> Declarations: return decls listed = git(root, "grep", "-l", "-w", "-F", *[a for w in sorted(words) for a in ("-e", w)], base, "--", *[f"{d}/*.lean" for d in LOCAL_DIRS]) - for line in listed.stdout.splitlines(): - shown = git(root, "show", line) # `line` is `base:path` - if shown.returncode == 0: - parse_source(shown.stdout, decls) + objects = listed.stdout.splitlines() # `base:path`, which `git cat-file` reads as an object + if not objects: + return decls + batch = subprocess.run(["git", "cat-file", "--batch"], cwd=root, capture_output=True, + input="".join(f"{o}\n" for o in objects).encode()) + data, pos = batch.stdout, 0 + while pos < len(data): + end = data.index(b"\n", pos) + header = data[pos:end].split() + pos = end + 1 + if len(header) != 3: # ` missing` + continue + size = int(header[2]) + parse_source(data[pos:pos + size].decode("utf-8", errors="replace"), decls) + pos += size + 1 return decls @@ -529,39 +556,51 @@ def check(text: str, root: Path = ROOT, core: bool = True, base: str | None = No if not tokens: return Report([], [], base) roots = source_roots(root, core) - words = set().union(*(search_words(t) for t in tokens)) decls, local = Declarations(), Declarations() local_roots = tuple(str(root / d) + os.sep for d in LOCAL_DIRS) texts: dict[Path, str] = {} - for path in files_mentioning(roots, words): - try: - texts[path] = path.read_text(encoding="utf-8", errors="replace") - except OSError: - continue - parse_source(texts[path], decls) - if str(path).startswith(local_roots): - parse_source(texts[path], local) - unresolved = [t for t in tokens if not resolves(t, decls, set())] - if unresolved: - modules = module_suffixes(roots) - python = python_names(root) - unresolved = [t for t in unresolved if t.removeprefix("_root_.") not in modules - and not all(part in python for part in t.split("."))] + + def read(words: set[str]) -> None: + for path in files_mentioning(roots, words): + if path in texts: + continue + try: + texts[path] = path.read_text(encoding="utf-8", errors="replace") + except OSError: + continue + parse_source(texts[path], decls) + if str(path).startswith(local_roots): + parse_source(texts[path], local) + + # Module names (`Init`, `Crypto.PRF`), script names and generated names in field notation + # (`.ext_iff`) need no source files; checking them first avoids reading every file that + # mentions a word as common as `Lean`. + modules, python = module_suffixes(roots), python_names(root) + unresolved = [t for t in tokens if t.removeprefix("_root_.") not in modules + and not all(part in python for part in t.split(".")) + and not (t.startswith(".") and t[1:] in GENERATED)] + read(set().union(set(), *(search_words(t) for t in unresolved))) + unresolved = [t for t in unresolved if not resolves(t, decls, set())] + if more := set().union(set(), *(head_words(t) for t in unresolved)): + read(more) + unresolved = [t for t in unresolved if not resolves(t, decls, set())] findings = [] for token in unresolved: last = token.lstrip(".").rsplit(".", 1)[-1] pattern = re.compile(WORD_BOUNDARY + re.escape(last) + r"(?![\w'!?])") mentions = sum(1 for t in texts.values() if last in t and pattern.search(t)) + if mentions and "." not in token and HYPOTHESIS.match(token): + continue # a hypothesis or other binder such as `hfA` or `h_le` findings.append(Finding(token, mentions, sorted(local.by_last.get(last, ()))[:3])) if findings and base: - before = base_declarations(root, base, {search for f in findings - for search in search_words(f.token)}) + before = base_declarations(root, base, {w for f in findings for w in + search_words(f.token) | head_words(f.token)}) for finding in findings: finding.removed = resolves(finding.token, before, set()) return Report(tokens, findings, base) -# --- Output ------------------------------------------------------------------------------------------- +# --- Output --------------------------------------------------------------------------------------- def revision(root: Path) -> str: result = git(root, "rev-parse", "--short=12", "HEAD") @@ -610,7 +649,8 @@ def main(argv: list[str] | None = None, root: Path = ROOT) -> int: source = parser.add_mutually_exclusive_group(required=True) source.add_argument("--pr", type=int, help="check the body of this pull request (uses `gh`)") source.add_argument("--file", help="check this Markdown file (`-` for standard input)") - source.add_argument("--event", help="check the body in this GitHub `pull_request` event payload") + source.add_argument("--event", + help="check the body in this GitHub `pull_request` event payload") parser.add_argument("--strict", action="store_true", help="exit 1 when a name is reported that the change did not remove") parser.add_argument("--github", action="store_true", diff --git a/scripts/test_check_pr_names.py b/scripts/test_check_pr_names.py index 02bf6ae71..607ead4de 100644 --- a/scripts/test_check_pr_names.py +++ b/scripts/test_check_pr_names.py @@ -45,6 +45,8 @@ theorem foo_iff : True ↔ True := Iff.rfl +theorem hasCollision_of_le (hfA : True) (h_le : True) : True := hfA + noncomputable def nonceGame (n : ℕ) : ℕ := go n where go (k : ℕ) : ℕ := k @@ -95,7 +97,8 @@ def test_extracts_backticked_spans_outside_code_blocks_and_comments(self) -> Non def test_candidates_skip_non_names(self) -> None: skipped = ["h k m + padFn 𝒩", "Complexity/Demo/Basic.lean", "CarterWegman.lean", - "0", "c69067ba", "simp", "ε", "trace", "hx", "h_le", "hFoo", "hfA", "pull_request", "GITHUB_EVENT_PATH", + "0", "c69067ba", "simp", "ε", "trace", "hx", "_leaf_le", "pull_request", + "GITHUB_EVENT_PATH", "PRF", "lake build", "mk_all --check", "lint-style", "native_decide", "theorem", "-1", "@[simp]", "x.1", "Y", ".symm", "maxHeartbeats", "linter.style.longLine"] for token in skipped: @@ -117,7 +120,8 @@ def test_declarations_resolve_by_full_name_and_suffix(self) -> None: self.assertEqual(self.check(" ".join(f"`{n}`" for n in names)), {}) def test_members_and_generated_names_resolve(self) -> None: - names = ["Pair.first", "Pair.width", "Pair.second", "Pair.second'", "Pair.toInhabited", "Pair.mk'", + names = ["Pair.first", "Pair.width", "Pair.second", "Pair.second'", "Pair.toInhabited", + "Pair.mk'", "Color.red", "Color.green", "Color.rec", "Pair.ext_iff", "pair_first_eq.eq_1", "nonceGame.go", "foo_iff.mp", "pair_first_eq_apply"] self.assertEqual(self.check(" ".join(f"`{n}`" for n in names)), {}) @@ -139,6 +143,16 @@ def test_missing_names_are_reported_with_context(self) -> None: self.assertIn("did you mean `Cslib.Demo.secureGame`", found["Cslib.Wrong.secureGame"].note(None)) + def test_hypothesis_shaped_names(self) -> None: + found = self.check("`hasCollision_of_le`, `hfA`, `h_le`, `hasNothing`, `hFoo`") + self.assertEqual(list(found), ["hasNothing", "hFoo"]) + + def test_generated_names_read_the_head_only_when_needed(self) -> None: + self.assertEqual(cpn.search_words("Nat.succ_le_of_lt"), {"succ_le_of_lt"}) + self.assertEqual(cpn.head_words("Nat.succ_le_of_lt"), set()) + self.assertEqual(cpn.head_words("Pair.mk"), {"Pair"}) + self.assertEqual(cpn.head_words("foo_iff.mp"), {"foo_iff"}) + def test_python_script_names_resolve(self) -> None: self.write("scripts/check_demo.py", "def changed_files():\n pass\n") found = self.check("`check_demo.changed_files`, `changed_files`, `check_demo.missing_fn`") @@ -154,7 +168,8 @@ def test_python_search_matches_ripgrep(self) -> None: def test_comments_are_not_declarations(self) -> None: self.write("Complexity/Demo/Commented.lean", "/- theorem inBlock : True := trivial -/\n-- theorem inLine : True := trivial\n" - "/-- doc\ntheorem inDoc : True := trivial -/\ntheorem real_decl : True := trivial\n") + "/-- doc\ntheorem inDoc : True := trivial -/\n" + "theorem real_decl : True := trivial\n") self.assertEqual(list(self.check("`inBlock` `inLine` `inDoc` `real_decl`")), ["inBlock", "inLine", "inDoc"]) @@ -164,14 +179,17 @@ def git(self, *args: str) -> str: return subprocess.run(["git", *args], cwd=self.root, check=True, capture_output=True, text=True).stdout.strip() + def commit(self, *args: str) -> None: + self.git("-c", "user.name=t", "-c", "user.email=t@t", "-c", "commit.gpgsign=false", + "commit", "-q", *args) + def test_names_removed_by_the_change_are_recognized(self) -> None: self.git("init", "-q") - self.git("-c", "user.name=t", "-c", "user.email=t@t", "commit", "-q", "--allow-empty", - "-m", "root") + self.commit("--allow-empty", "-m", "root") self.write("Complexity/Demo/Old.lean", "namespace Cslib.Old\ntheorem old_lemma : True := trivial\nend Cslib.Old\n") self.git("add", ".") - self.git("-c", "user.name=t", "-c", "user.email=t@t", "commit", "-q", "-m", "base") + self.commit("-m", "base") base = self.git("rev-parse", "HEAD") (self.root / "Complexity/Demo/Old.lean").unlink() found = self.check("Removes `Cslib.Old.old_lemma`; adds `brandNew`.", base=base) From 0c54249dac368bc4cb615b67707aaadbe2fe938e Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sun, 25 Oct 2026 18:52:25 +0000 Subject: [PATCH 2/2] fix(scripts): resolve structure-parent projections in check_pr_names (#1086) A toX projection generated by `extends X` never appears in its declaring file; search for X as well. Also check the git cat-file header type. Authored by worker-jetski-d75789e1 (AI agent). --- scripts/check_pr_names.py | 4 +++- scripts/test_check_pr_names.py | 10 ++++++++++ 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/scripts/check_pr_names.py b/scripts/check_pr_names.py index 63fb05245..0afa2aa51 100644 --- a/scripts/check_pr_names.py +++ b/scripts/check_pr_names.py @@ -395,6 +395,8 @@ def search_words(token: str) -> set[str]: words = {last.rstrip("'!?")} if m := SIMPS_SUFFIX.match(last): words.add(m.group(1)) + if re.fullmatch(r"to[A-Z]\w*", last): # `extends Inhabited` declares `toInhabited` + words.add(last[2:].rstrip("'!?")) for variant in additive_variants(bare): words.add(variant.rsplit(".", 1)[-1].rstrip("'!?")) return {w for w in words if w} @@ -529,7 +531,7 @@ def base_declarations(root: Path, base: str, words: set[str]) -> Declarations: end = data.index(b"\n", pos) header = data[pos:end].split() pos = end + 1 - if len(header) != 3: # ` missing` + if len(header) != 3 or header[1] != b"blob": # ` missing`; a path may hold spaces continue size = int(header[2]) parse_source(data[pos:pos + size].decode("utf-8", errors="replace"), decls) diff --git a/scripts/test_check_pr_names.py b/scripts/test_check_pr_names.py index 607ead4de..445f38490 100644 --- a/scripts/test_check_pr_names.py +++ b/scripts/test_check_pr_names.py @@ -143,6 +143,16 @@ def test_missing_names_are_reported_with_context(self) -> None: self.assertIn("did you mean `Cslib.Demo.secureGame`", found["Cslib.Wrong.secureGame"].note(None)) + def test_parent_projections_resolve_from_the_structure_file(self) -> None: + tmp = tempfile.TemporaryDirectory() + self.addCleanup(tmp.cleanup) + self.root = pathlib.Path(tmp.name) + self.write("Complexity/Parent.lean", "class Base (α : Type) where\n base : α\n") + self.write("Complexity/Child.lean", + "structure Pair (α : Type) extends Base α where\n first : α\n") + self.assertEqual(self.check("`Pair.toBase`"), {}) + self.assertEqual(list(self.check("`Pair.toNotAThing`")), ["Pair.toNotAThing"]) + def test_hypothesis_shaped_names(self) -> None: found = self.check("`hasCollision_of_le`, `hfA`, `h_le`, `hasNothing`, `hFoo`") self.assertEqual(list(found), ["hasNothing", "hFoo"])