From b3f9fdb1b0261eb207bb85018d9a0536a96b38dc Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 20:34:17 -0400 Subject: [PATCH 01/10] feat(scripts): plan and rewrite the S2 tidy sweep `scripts/tidy_sweep.py` classifies every public declaration outside the #608 raw-machine allowlist whose statement mentions a tidy predicate into the cases of the S2 design (#456): a registered plain twin, a theorem to rename and restate, or a definition or structure field; the rest are unclassifiable (unsupported notion, bridge, deprecated alias, collision). `report` prints per-area counts and each area's rewrite plan as Markdown and JSON; `rewrite --area` applies one area's batch at the `.ilean` reference ranges, translating or wrapping each restated proof and keeping the old type at call sites in proofs that stay tidy. `--verify` builds the libraries and falls back from translation to wrapping, then to a local plain-to-tidy `fun_prop` transition. `scripts/QualityReport.lean` reports tidy constants in exposed bodies and, on request, a statement hash that identifies tidy and plain predicates and per-binder tidy flags. The registry stub holds the existing exact twins in the format of #608's `#mirror_pairs`; the allowlist is #608's. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- scripts/QualityReport.lean | 72 +- scripts/quality_report.py | 12 +- scripts/test_tidy_sweep.py | 337 ++++++ scripts/tidy_allowlist.txt | 27 + scripts/tidy_mirror_registry.json | 82 ++ scripts/tidy_sweep.py | 1882 +++++++++++++++++++++++++++++ 6 files changed, 2401 insertions(+), 11 deletions(-) create mode 100644 scripts/test_tidy_sweep.py create mode 100644 scripts/tidy_allowlist.txt create mode 100644 scripts/tidy_mirror_registry.json create mode 100644 scripts/tidy_sweep.py diff --git a/scripts/QualityReport.lean b/scripts/QualityReport.lean index 85693e8542..6df0804cb2 100644 --- a/scripts/QualityReport.lean +++ b/scripts/QualityReport.lean @@ -9,9 +9,10 @@ import Lean /-! # Declaration data for `scripts/quality_report.py` -Run as `lake env lean --run scripts/QualityReport.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: +Run as `lake env lean --run scripts/QualityReport.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: * `n`, `m`: the constant and its module; * `k`: its kind in the private part (`def`, `thm`, `induct`, `ctor`, `rec`, `opaque`, `quot`, @@ -20,11 +21,21 @@ name per line on standard input. For every module it reads the three parts of th 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`: those in its exposed body, for an exported definition; * `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. +An optional second argument, comma-separated `tidy=plain` pairs of predicate names (used by +`scripts/tidy_sweep.py`), adds two fields. `ph`, for an exported constant: a hash of its type with +universe parameters renamed positionally and each listed tidy or plain predicate replaced by its +plain one, so that a statement and its plain transport hash alike. `sg`, for a constant whose type +mentions a listed tidy predicate: `[[[binderInfo, flag], ...], flag]` for the leading binders and +the conclusion, with binder info `0` explicit, `1` implicit, `2` strict implicit, `3` instance, and +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. + It then prints `{"dup": [...], "k": ...}` lines grouping exported constants of different modules whose types are alpha-equivalent (`k = "thm"`), or whose types and exposed bodies are (`k = "def"`). Universe parameters are renamed positionally before comparing. @@ -83,7 +94,44 @@ def normalize (c : ConstantInfo) (e : Expr) : Expr := let us := c.levelParams.length.fold (fun i _ acc => acc.push (Level.param (.num `u i))) #[] e.instantiateLevelParams c.levelParams us.toList -unsafe def run (libDir : System.FilePath) : IO Unit := do +/-- Replace each predicate of `canon` by its plain counterpart, without universe levels. -/ +def canonicalize (canon : NameMap Name) (e : Expr) : Expr := + e.replace fun + | .const n _ => (canon.find? n).map (Expr.const · []) + | _ => none + +/-- `1` for an application of a listed tidy predicate, `2` for another mention of a tidy constant, +`0` otherwise. -/ +def tidyFlag (preds : NameSet) (t : Expr) : Nat := + match t.consumeMData.getAppFn with + | .const n _ => if preds.contains n then 1 else if t.getUsedConstants.any isTidy then 2 else 0 + | _ => if t.getUsedConstants.any isTidy then 2 else 0 + +def binderCode : BinderInfo → Nat + | .default => 0 + | .implicit => 1 + | .strictImplicit => 2 + | .instImplicit => 3 + +/-- The flags of the leading binders and of the conclusion of a type. -/ +partial def signature (preds : NameSet) (e : Expr) (acc : Array Json := #[]) : Json := + match e with + | .forallE _ t b bi => signature preds b (acc.push (toJson #[binderCode bi, tidyFlag preds t])) + | .mdata _ b => signature preds b acc + | _ => Json.arr #[Json.arr acc, toJson (tidyFlag preds e)] + +/-- Parse `tidy=plain,…` into the map sending both names to the plain one. -/ +def parseCanon (arg : String) : NameMap Name × NameSet := Id.run do + let mut canon : NameMap Name := {} + let mut preds : NameSet := {} + for pair in arg.splitOn "," do + if let [tidy, plain] := pair.splitOn "=" then + canon := (canon.insert tidy.toName plain.toName).insert plain.toName plain.toName + preds := preds.insert tidy.toName + return (canon, preds) + +unsafe def run (libDir : System.FilePath) (pairs : Option String := none) : IO Unit := do + let (canon, preds) := parseCanon (pairs.getD "") let stdin ← IO.getStdin let stdout ← IO.getStdout let mut theorems : Std.HashMap Expr (Array (String × Name)) := {} @@ -115,11 +163,21 @@ unsafe def run (libDir : System.FilePath) : IO Unit := do | some ec => ec.type.getUsedConstants | none => #[] let uses := uses.filter (fun n => n != c.name && sameModule.contains n) |>.toList.eraseDups - stdout.putStrLn <| Json.compress <| Json.mkObj [ + let tidyBody := match e with + | some (.defnInfo v) => v.value.getUsedConstants.filter isTidy |>.map Name.toString + | _ => #[] + 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), + ("doc", docs.contains c.name), ("tidy", toJson tidy), ("tb", toJson tidyBody), ("u", toJson (uses.map (·.toString))), ("r", (ranges.find? c.name).map rangeJson |>.getD .null)] + if pairs.isSome then + if let some ec := e then + let hash := (canonicalize canon (normalize ec ec.type)).hash + row := row ++ [("ph", toJson (toString hash))] + if c.type.getUsedConstants.any preds.contains then + row := row ++ [("sg", signature preds c.type)] + stdout.putStrLn <| Json.compress <| Json.mkObj row if let some ec := e then unless c.name.isInternalDetail do match c, ec with @@ -142,4 +200,4 @@ unsafe def run (libDir : System.FilePath) : IO Unit := do end ComplexityScripts.QualityReport unsafe def main (args : List String) : IO Unit := - ComplexityScripts.QualityReport.run (args.headD ".lake/build/lib/lean") + ComplexityScripts.QualityReport.run (args.headD ".lake/build/lib/lean") args[1]? diff --git a/scripts/quality_report.py b/scripts/quality_report.py index 43bee8da40..c5e70f31db 100644 --- a/scripts/quality_report.py +++ b/scripts/quality_report.py @@ -422,8 +422,12 @@ def load_ileans(build_dir: Path) -> dict[str, dict]: return ileans -def load_constants(build_dir: Path, modules: list[str]) -> tuple[dict[str, dict], list[dict]]: - out = run(["lake", "env", "lean", "--run", "scripts/QualityReport.lean", str(build_dir)], +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(): @@ -463,10 +467,10 @@ def offset(self, line0: int, index: int) -> int: class Library: """Build outputs and sources of the three libraries, loaded lazily where possible.""" - def __init__(self, build_dir: Path): + def __init__(self, build_dir: Path, pairs: str | None = None): self.ileans = load_ileans(build_dir) self.modules = sorted(m for m in self.ileans if m.startswith("Complexity.")) - self.constants, self.duplicate_rows = load_constants(build_dir, self.modules) + self.constants, self.duplicate_rows = load_constants(build_dir, self.modules, pairs) self.sources: dict[str, Source] = {} def source(self, module: str) -> Source: diff --git a/scripts/test_tidy_sweep.py b/scripts/test_tidy_sweep.py new file mode 100644 index 0000000000..b645b47df9 --- /dev/null +++ b/scripts/test_tidy_sweep.py @@ -0,0 +1,337 @@ +"""Unit tests for the pure helpers of scripts/tidy_sweep.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 tidy_sweep as t # noqa: E402 +from proof_lengths import masks # noqa: E402 + +POLY = "Turing.MultiTapeTM.ComputableTidilyInPolyTime" +PLAIN = "Turing.MultiTapeTM.ComputableInPolyTime" + + +def decl(name: str, kind: str = "thm", role: str = "decl", attrs=(), keyword="theorem", + area: str = "Logics") -> dict: + return {"name": name, "module": "Complexity.M", "path": "M.lean", "area": area, + "role": role, "kind": kind, "keyword": keyword, "attrs": set(attrs), + "implicit": [], "lib_refs": set(), "test_refs": set(), "abstract_refs": set()} + + +def const(tidy=(POLY,), ph: str = "1", e: str = "axiom", tb=()) -> dict: + return {"m": "Complexity.M", "k": "thm", "e": e, "tidy": list(tidy), "tb": list(tb), + "ph": ph} + + +class NameTests(unittest.TestCase): + def test_plain_name_replaces_supported_notions_only(self) -> None: + self.assertEqual(t.plain_name("A.computableTidilyInPolyTime_foo"), + "A.computableInPolyTime_foo") + self.assertEqual(t.plain_name(POLY + ".comp"), PLAIN + ".comp") + self.assertEqual(t.plain_name("x_computableTidilyInO_y"), "x_computableInO_y") + self.assertEqual(t.plain_name("Cslib.Complexity.ComputableTidilyInFPTTime.of_x"), + "Cslib.Complexity.ComputableInFPTTime.of_x") + for unsupported in ("computableTidilyInDegree_foo", "ComputableTidilyInTimeAndSpace.x", + "computableTidilyInOracle", "ComputesTidily"): + self.assertEqual(t.plain_name(unsupported), unsupported) + + def test_notion_bridges(self) -> None: + notion = t.BY_TIDY[POLY] + self.assertEqual(notion.dot_of_tidy, POLY + ".computableInPolyTime") + self.assertIn(PLAIN + ".of_tidy", t.BRIDGES) + self.assertIn(notion.iff, t.BRIDGES) + + def test_renamed_token_keeps_the_written_prefix(self) -> None: + old = "Cslib.A.CNF.computableTidilyInPolyTime_vars" + new = "Cslib.A.CNF.computableInPolyTime_vars" + self.assertEqual(t.renamed_token("CNF.computableTidilyInPolyTime_vars", old, new), + "CNF.computableInPolyTime_vars") + self.assertEqual(t.renamed_token("@CNF.computableTidilyInPolyTime_vars", old, new), + "@CNF.computableInPolyTime_vars") + self.assertEqual(t.renamed_token(old, old, new), new) + # Written relative to the tidy namespace: the prefix itself changes. + self.assertIsNone(t.renamed_token("map", POLY + ".map", PLAIN + ".map")) + + def test_written_name_is_the_shortest_unambiguous_suffix(self) -> None: + known = {PLAIN + ".map", "Other.ComputableInPolyTime.map", "List.map"} + self.assertEqual(t.written_name(PLAIN + ".map", ["Turing.MultiTapeTM", ""], known), + "ComputableInPolyTime.map") + self.assertEqual(t.written_name(PLAIN + ".map", [PLAIN, ""], known), "map") + # `ComputableInPolyTime.map` is ambiguous when `Other` is open too. + self.assertEqual(t.written_name(PLAIN + ".map", ["Turing.MultiTapeTM", "Other", ""], + known), PLAIN + ".map") + self.assertEqual(t.written_name(PLAIN + ".map", ["Turing", "Other", ""], known), + "MultiTapeTM.ComputableInPolyTime.map") + + def test_scopes_track_namespaces_and_opens(self) -> None: + text = ("namespace Cslib.Logic\n\nopen Turing.MultiTapeTM ComputableTidilyInPolyTime\n\n" + "theorem a : True := trivial\n\nend Cslib.Logic\n\nopen Foo in\n" + "theorem b : True := trivial\n\ntheorem c : True := trivial\n") + scopes = t.Scopes(masks(text)[1], t.namespaces_of([POLY + ".map", "Foo.x"])) + namespace, opens = scopes.at(text.index("theorem a")) + self.assertEqual(namespace, "Cslib.Logic") + self.assertEqual(opens, ("Turing.MultiTapeTM", POLY)) + self.assertEqual(scopes.at(text.index("theorem b")), ("", ("Foo",))) + self.assertEqual(scopes.at(text.index("theorem c")), ("", ())) + self.assertEqual(scopes.prefixes(text.index("theorem a"))[:3], + ["Cslib.Logic", "Cslib", ""]) + + +class ClassificationTests(unittest.TestCase): + def classify(self, d: dict, c: dict, registry=None, constants=None, private=None): + return t.classify_decl(d, c, registry or {}, constants or {d["name"]: c}, private or {}) + + def test_case_two_renames_and_checks_the_target(self) -> None: + e = self.classify(decl("A.computableTidilyInPolyTime_x"), const()) + self.assertEqual((e.case, e.target), ("2", "A.computableInPolyTime_x")) + e = self.classify(decl("A.mem_X_iff"), const()) + self.assertEqual((e.case, e.target), ("2", "A.mem_X_iff")) + + def test_collisions(self) -> None: + c = const(ph="1") + constants = {"A.computableTidilyInPolyTime_x": c, + "A.computableInPolyTime_x": const(tidy=(), ph="2")} + e = self.classify(decl("A.computableTidilyInPolyTime_x"), c, constants=constants) + self.assertEqual((e.case, e.reason), ("unclassifiable", "collision")) + self.assertFalse(e.collision["equivalent"]) + constants["A.computableInPolyTime_x"]["ph"] = "1" + e = self.classify(decl("A.computableTidilyInPolyTime_x"), c, constants=constants) + self.assertTrue(e.collision["equivalent"]) + # A private declaration of the same module blocks the name as well. + e = self.classify(decl("A.computableTidilyInPolyTime_y"), c, + private={"Complexity.M": {"A.computableInPolyTime_y"}}) + self.assertEqual(e.reason, "collision") + + def test_registered_twin_is_case_one(self) -> None: + c = const(ph="5") + constants = {POLY + ".map": c, PLAIN + ".map": const(tidy=(), ph="5")} + e = self.classify(decl(POLY + ".map"), c, {POLY + ".map": PLAIN + ".map"}, constants) + self.assertEqual((e.case, e.target, e.warnings), ("1", PLAIN + ".map", [])) + e = self.classify(decl(POLY + ".map"), c, {POLY + ".map": "Missing.twin"}, constants) + self.assertEqual(e.reason, "registered twin missing") + + def test_unclassifiable_reasons(self) -> None: + degree = "Turing.MultiTapeTM.ComputableTidilyInDegree" + e = self.classify(decl("A.foo"), const(tidy=(POLY, degree))) + self.assertEqual(e.reason, "unsupported notion") + e = self.classify(decl("A.foo", attrs=("deprecated",)), const()) + self.assertEqual(e.reason, "deprecated alias") + e = self.classify(decl("A.pSimulates_iff_tidy"), const()) + self.assertEqual(e.reason, "bridge") + e = self.classify(decl(PLAIN + ".of_tidy"), const()) + self.assertEqual(e.reason, "bridge") + e = self.classify(decl("A.ComputableTidilyInX", kind="def", keyword="def"), const()) + self.assertEqual(e.reason, "tidy notion definition") + + def test_definitions_and_fields_are_case_three(self) -> None: + e = self.classify(decl("A.P", kind="def", keyword="def"), const(tidy=(), tb=(POLY,))) + self.assertEqual((e.case, e.kind, e.body_only), ("3", "definition", True)) + e = self.classify(decl("A.S.polyTime", role="member"), const()) + self.assertEqual((e.case, e.kind), ("3", "structure field")) + + def test_registry_formats(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + path = pathlib.Path(tmp) / "r.json" + path.write_text(json.dumps([{"original": "a", "plain": "b", "module": "M"}])) + self.assertEqual(t.load_registry(path), {"a": "b"}) + path.write_text(json.dumps({"pairs": [{"original": "c", "plain": "d"}]})) + self.assertEqual(t.load_registry(path), {"c": "d"}) + path.write_text(json.dumps([{"original": "c"}])) + with self.assertRaises(ValueError): + t.load_registry(path) + self.assertEqual(t.load_registry(pathlib.Path(tmp) / "missing.json"), {}) + + def test_allowlist_ignores_comments(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + path = pathlib.Path(tmp) / "a.txt" + path.write_text("# header\nA/B.lean\n\nC.lean # note\n") + self.assertEqual(t.load_allowlist(path), {"A/B.lean", "C.lean"}) + + +class ParsingTests(unittest.TestCase): + def test_brackets_and_top_level_tokens(self) -> None: + text = "(a : b := c) : T := x" + self.assertEqual(t.match_bracket(text, 0), 11) + self.assertEqual(t.find_top_level(text, 0, len(text), ":"), 13) + self.assertEqual(t.find_top_level(text, 0, len(text), ":="), 17) + + def test_parse_decl(self) -> None: + text = ("theorem foo {f : V → W} [DecidableEq V]\n (hf hg : P f e e) (x : ℕ := 0) :\n" + " P (g ∘ f) e e := by\n simp\n") + mask = masks(text)[1] + start = text.index("foo") + dt = t.parse_decl(mask, 0, start, start + 3, len(text.rstrip())) + self.assertEqual([b.bracket for b in dt.binders], ["{", "[", "(", "("]) + self.assertEqual(dt.binders[2].names, ["hf", "hg"]) + self.assertEqual(text[dt.binders[2].type_start:dt.binders[2].type_end].strip(), "P f e e") + self.assertTrue(dt.binders[3].default) + self.assertEqual(text[dt.colon + 1:dt.assign].strip(), "P (g ∘ f) e e") + self.assertEqual(dt.problems, []) + body, tactic = t.proof_parts(text, dt.assign, dt.end) + self.assertTrue(tactic) + dt = t.parse_decl(masks("theorem f : T\n | 0 => a")[1], 0, 8, 9, 23) + self.assertIn("no `:=` (pattern-matching definition)", dt.problems) + + def test_arguments(self) -> None: + text = "X (f := id) a (b c) ⟨d, e⟩ h.1 |>.comp\n more" + mask = masks(text)[1] + named = [] + args = t.parse_args(mask, 1, len(mask), 5, 0, named) + self.assertEqual([text[a:b] for a, b in args], ["a", "(b c)", "⟨d, e⟩", "h.1"]) + self.assertEqual([text[a:b] for a, b in named], ["(f := id)"]) + # Arguments continue on a more indented line, and stop at keywords. + text = " X a\n b\n c" + self.assertEqual(len(t.parse_args(text, 3, len(text), 3, 2)), 2) + self.assertEqual(t.parse_args("X by simp", 1, 9, 1, 0), []) + + def test_atomic_application(self) -> None: + text = "P f (encList e) enc" + self.assertEqual(t.is_atomic_application(text, 0, len(text)), (0, 1)) + self.assertIsNone(t.is_atomic_application("P f → Q g", 0, 9)) + self.assertIsNone(t.is_atomic_application("∀ n, P n", 0, 8)) + + def test_receiver_and_opener(self) -> None: + text = "foo (bar baz).qux" + self.assertEqual(t.receiver_start(text, text.index(".qux")), 4) + text = "foo hf.comp" + self.assertEqual(t.receiver_start(text, text.index(".comp")), 4) + text = "simp [a, b]" + self.assertEqual(t.enclosing_opener(text, 9), 5) + + +class EditTests(unittest.TestCase): + def test_nested_wraps_render_inside_out(self) -> None: + text = "f (X a) b" + # The argument `(X a)` gets `(.of_tidy …)`; its own site appends `.tidy`. + wraps = [t.Wrap(2, 7, "(.of_tidy ", ")", 0), t.Wrap(2, 7, "", ".tidy", 3)] + reps = [t.Replace(3, 4, "Y")] + self.assertEqual(t.render(text, reps, wraps, 0, len(text)), "f (.of_tidy (Y a).tidy) b") + + def test_regions_transform_their_edited_text(self) -> None: + text = "a := X\nb" + out = t.apply_edits(text, [t.Replace(5, 6, "Y")], [], + [t.Region(4, 6, lambda s: "[" + s + "]", "d")]) + self.assertEqual(out, "a :=[ Y]\nb") + + def test_round_trips(self) -> None: + cases = { + "f (.of_tidy (X a).tidy) b": "f (X a) b", + "f (.of_tidy hV.tidy) b": "f hV b", + "exact .of_tidy <| h.tidy\n": "exact h\n", + "exact ComputableInPolyTime.of_tidy (h.tidy)": "exact h", + "(X a).tidy.computableInPolyTime": "(X a)", + } + for before, after in cases.items(): + self.assertEqual(t.cancel_round_trips(before)[0], after, before) + for kept in (".of_tidy <| (X a).tidy.comp h", ".of_tidy (f a.tidy)", + ".of_tidy <| h.tidy.comp g", "-- .of_tidy (h.tidy)"): + self.assertEqual(t.cancel_round_trips(kept), (kept, 0), kept) + + +class WrapTests(unittest.TestCase): + def test_term_without_hypotheses(self) -> None: + self.assertEqual(t.wrap_proof("\n map f", 2, 0, [], "P", True, "iff"), + "\n .of_tidy (map f)") + + def test_term_with_hypotheses(self) -> None: + hyps = [t.Hyp(["hf"], "P f", True), t.Hyp(["hg"], "∀ n, P (g n)", False)] + self.assertEqual( + t.wrap_proof("\n (hf.comp\n hg)", 2, 0, hyps, "P h", True, "iff"), + " by\n have hf := hf.tidy\n have hg : ∀ n, P (g n) := by simpa only [iff] using hg" + "\n exact .of_tidy ((hf.comp\n hg))") + + def test_tactic_block(self) -> None: + body = " by\n unfold f\n fun_prop" + self.assertEqual(t.wrap_proof(body, 2, 0, [t.Hyp(["h"], "P g", True)], "P f", True, "i"), + " by\n have h := h.tidy\n refine .of_tidy ?_\n unfold f\n fun_prop") + self.assertEqual(t.wrap_proof(body, 2, 0, [], "P f ↔ Q", False, "i"), + " by\n have this : P f ↔ Q := by\n unfold f\n fun_prop\n" + " simpa only [i] using this") + self.assertEqual(t.wrap_proof(" by simp", 2, 0, [t.Hyp(["h"], "P g", True)], None, + False, "i"), " by\n have h := h.tidy\n simp") + + def test_reindent(self) -> None: + self.assertEqual(t.reindent([" a", "", " b"], -2), ["a", "", " b"]) + self.assertIsNone(t.reindent([" a"], -2)) + + +class ConvertTests(unittest.TestCase): + def planner(self, sg) -> t.Planner: + p = object.__new__(t.Planner) + p.model = type("M", (), {"constants": {"X": {"sg": sg}}})() + return p + + def convert(self, text: str, sg, at: str = "X") -> tuple[str, str | None]: + src = object.__new__(t.SourceFile) + src.text, src.mask = text, masks(text)[1] + fe = t.FileEdits() + start = text.index(at) + problem = self.planner(sg).convert_site(src, fe, start, start + len(at), "X") + return t.render(text, fe.replaces, fe.wraps, 0, len(text)), problem + + def test_application_keeps_its_old_type(self) -> None: + sg = [[[1, 0], [0, 0], [0, 1]], 1] # {V} (enc) (hc : tidy) : tidy + self.assertEqual(self.convert(" exact X enc hc", sg), + (" exact (X enc (.of_tidy hc)).tidy", None)) + self.assertEqual(self.convert(" exact (X enc hc).comp g", sg)[0], + " exact (X enc (.of_tidy hc)).tidy.comp g") + self.assertEqual(self.convert(" X (V := ℕ) enc hc", sg)[0], + " (X (V := ℕ) enc (.of_tidy hc)).tidy") + + def test_constants_and_dot_chains(self) -> None: + self.assertEqual(self.convert(" exact X.comp h", [[[1, 0]], 1])[0], + " exact X.tidy.comp h") + + def test_unconvertible_sites(self) -> None: + sg = [[[0, 0]], 1] + self.assertIn("partial", self.convert(" map X", sg)[1]) + self.assertIn("lemma list", self.convert(" simp [X]", sg)[1]) + self.assertIn("leading-dot", self.convert(" exact .X a", sg, "X")[1]) + self.assertIn("binders", self.convert(" X a", [[[0, 2]], 1])[1]) + self.assertIn("implicit", self.convert(" X a", [[[1, 1], [0, 0]], 1])[1]) + self.assertIn("bare", self.convert(" X a", [[[0, 0]], 2])[1]) + + +class BuildOutputTests(unittest.TestCase): + def test_diagnostics_and_declarations(self) -> None: + out = ("✖ [3/4] Building M\nerror: ././././Complexity/M.lean:5:2: unknown identifier 'x'\n" + "warning: Complexity/M.lean:9:0: unused variable `h`\n") + self.assertEqual(t.diagnostics(out), [ + {"level": "error", "path": "Complexity/M.lean", "line": 5, + "message": "unknown identifier 'x'"}, + {"level": "warning", "path": "Complexity/M.lean", "line": 9, + "message": "unused variable `h`"}]) + text = "/-- doc -/\n@[simp]\ntheorem A.foo (x : ℕ) :\n x = x := by\n rfl\n" + self.assertEqual(t.declaration_at(text, 5), "A.foo") + # Lean reports some errors at the docstring, which belongs to the next declaration. + text = ("theorem a : True := by\n trivial\n\n/-- doc\nmore -/\n" + "theorem b : True := trivial\n") + self.assertEqual([t.declaration_at(text, n) for n in (2, 4, 6)], ["a", "b", "b"]) + self.assertEqual(t.command_line(text, 7), 6) + self.assertTrue(t.CONSEQUENCE.search("❌️ Docstring on `#guard_msgs` does not match")) + + def test_module_paths(self) -> None: + self.assertEqual(t.module_of(t.ROOT / "Complexity/A/B.lean"), "Complexity.A.B") + self.assertEqual(t.module_of(t.ROOT / "abstracts/ComplexityAbstracts/X.lean"), + "ComplexityAbstracts.X") + + +class SummaryTests(unittest.TestCase): + def test_counts_by_area_and_case(self) -> None: + entries = [t.Entry("a", "M", "p", "Logics", "theorem", "2"), + t.Entry("b", "M", "p", "Logics", "theorem", "unclassifiable", "bridge"), + t.Entry("c", "M", "p", "Crypto", "definition", "3")] + s = t.summary(entries) + self.assertEqual(s["areas"]["Logics"], {"total": 2, "2": 1, "unclassifiable": 1}) + self.assertEqual(s["total"]["total"], 3) + self.assertEqual(s["unclassifiable_reasons"], {"bridge": 1}) + self.assertEqual(list(s["areas"]), ["Crypto", "Logics"]) + + +if __name__ == "__main__": + unittest.main() diff --git a/scripts/tidy_allowlist.txt b/scripts/tidy_allowlist.txt new file mode 100644 index 0000000000..59af7485b4 --- /dev/null +++ b/scripts/tidy_allowlist.txt @@ -0,0 +1,27 @@ +# The raw machine constructions that may state tidy computability publicly: finite controls, +# tape routing, blank-work-tape restoration, exact-time TM/PTM composition. One path per line. +# Source: #608 (https://github.com/cslib-community/complexitylib/issues/608#issuecomment-6376743596), +# checked at main cded1fc9. Exact paths only; mixed modules need declaration-level handling. +Complexity/Computability/Machines/Turing/MultiTape/Combinators/Append.lean +Complexity/Computability/Machines/Turing/MultiTape/Combinators/Comp.lean +Complexity/Computability/Machines/Turing/MultiTape/Combinators/CopyWord.lean +Complexity/Computability/Machines/Turing/MultiTape/Combinators/Foldl.lean +Complexity/Computability/Machines/Turing/MultiTape/Combinators/Ite.lean +Complexity/Computability/Machines/Turing/MultiTape/Combinators/IterateWhile.lean +Complexity/Computability/Machines/Turing/MultiTape/Combinators/MultiPass.lean +Complexity/Computability/Machines/Turing/MultiTape/Combinators/Reverse.lean +Complexity/Computability/Machines/Turing/MultiTape/Combinators/StepMachine.lean +Complexity/Computability/Machines/Turing/MultiTape/Combinators/StreamFold.lean +Complexity/Computability/Machines/Turing/MultiTape/Combinators/TidyNormalForm.lean +Complexity/Computability/Machines/Turing/MultiTape/Combinators/TidyZeroSpace.lean +Complexity/Computability/Machines/Turing/MultiTape/Combinators/Transducer.lean +Complexity/Computability/Machines/Turing/MultiTape/Plumbing/InputFromTape.lean +Complexity/Computability/Machines/Turing/MultiTape/Plumbing/OnWords.lean +Complexity/Computability/Machines/Turing/MultiTape/Plumbing/OutputToTape.lean +Complexity/Computability/Machines/Turing/MultiTape/Plumbing/Tidy/Basic.lean +Complexity/Computability/Machines/Turing/MultiTape/Plumbing/Tidy/Defs.lean +Complexity/Computability/Machines/Turing/MultiTape/Plumbing/Tidy/Run.lean +Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/RunsWords.lean +Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Tidy.lean +Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Tidy/Redirect.lean +Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/IterateWhile.lean diff --git a/scripts/tidy_mirror_registry.json b/scripts/tidy_mirror_registry.json new file mode 100644 index 0000000000..248c9e34c1 --- /dev/null +++ b/scripts/tidy_mirror_registry.json @@ -0,0 +1,82 @@ +[ + { + "original": "Cslib.Complexity.computableTidilyInPolyTime_andVerifier", + "plain": "Cslib.Complexity.computableInPolyTime_andVerifier", + "module": "Complexity.Computability.Complexity.Classes.SharpP.Combinators" + }, + { + "original": "Cslib.Complexity.computableTidilyInPolyTime_orVerifier", + "plain": "Cslib.Complexity.computableInPolyTime_orVerifier", + "module": "Complexity.Computability.Complexity.Classes.SharpP.Combinators" + }, + { + "original": "Cslib.Complexity.computableTidilyInPolyTime_selectVerifier", + "plain": "Cslib.Complexity.computableInPolyTime_selectVerifier", + "module": "Complexity.Computability.Complexity.Classes.SharpP.Combinators" + }, + { + "original": "Turing.MultiTapeTM.ComputableInTimeAndSpace.computableTidilyInPolyTime", + "plain": "Turing.MultiTapeTM.ComputableInTimeAndSpace.computableInPolyTime", + "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain" + }, + { + "original": "Turing.MultiTapeTM.ComputableTidilyInPolySpace.id'", + "plain": "Turing.MultiTapeTM.ComputableInPolySpace.id'", + "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolySpace" + }, + { + "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.comp", + "plain": "Turing.MultiTapeTM.ComputableInPolyTime.comp", + "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" + }, + { + "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.comp'", + "plain": "Turing.MultiTapeTM.ComputableInPolyTime.comp'", + "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" + }, + { + "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.const", + "plain": "Turing.MultiTapeTM.ComputableInPolyTime.const", + "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" + }, + { + "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.fst", + "plain": "Turing.MultiTapeTM.ComputableInPolyTime.fst", + "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" + }, + { + "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.id'", + "plain": "Turing.MultiTapeTM.ComputableInPolyTime.id'", + "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" + }, + { + "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.ite'", + "plain": "Turing.MultiTapeTM.ComputableInPolyTime.ite'", + "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" + }, + { + "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.of_eq", + "plain": "Turing.MultiTapeTM.ComputableInPolyTime.of_eq", + "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" + }, + { + "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.pair", + "plain": "Turing.MultiTapeTM.ComputableInPolyTime.pair", + "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" + }, + { + "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.polyBounded_length", + "plain": "Turing.MultiTapeTM.ComputableInPolyTime.polyBounded_length", + "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" + }, + { + "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.prod", + "plain": "Turing.MultiTapeTM.ComputableInPolyTime.prod", + "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" + }, + { + "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.snd", + "plain": "Turing.MultiTapeTM.ComputableInPolyTime.snd", + "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" + } +] diff --git a/scripts/tidy_sweep.py b/scripts/tidy_sweep.py new file mode 100644 index 0000000000..2a5621bcb5 --- /dev/null +++ b/scripts/tidy_sweep.py @@ -0,0 +1,1882 @@ +#!/usr/bin/env python3 +"""Plan and apply S2 of #456: remove tidy computability from public statements. + +Usage: python3 scripts/tidy_sweep.py report [--area AREA]... [--json OUT] [--markdown OUT] + python3 scripts/tidy_sweep.py rewrite --area AREA [--diff OUT | --verify [--rounds N]] + python3 scripts/tidy_sweep.py stub-registry [--output FILE] +Common options: [--registry FILE] [--allowlist FILE] [--build-dir DIR] [--no-build-check] + +Tidy computability is a proof device: outside the raw machine constructions of the allowlist +(`scripts/tidy_allowlist.txt`, from #608), no public statement should mention it. Every public +declaration outside the allowlist whose statement (its type, or the exposed body of a definition) +mentions a tidy predicate falls in one case of the S2 design +(https://github.com/cslib-community/complexitylib/issues/456#issuecomment-6376748411): + +1. a theorem with a registered plain twin (`--registry`): proofs that become plain use the twin; +2. any other theorem: it is renamed `computableTidily…` → `computable…` (the target name must be + free) and restated with the plain predicates; +3. a definition, instance or structure field: it is listed for a hand-written plain redefinition. + +A declaration that fits none of these is *unclassifiable*: it mentions a tidy notion without a +same-bound plain equivalence, is a plain/tidy bridge or a deprecated alias, or its target name is +taken (a collision). `report` prints the classification with per-area counts (#587's areas) and +each area's rewrite plan, without writing anything. + +`rewrite --area AREA` restates the area's case 2 declarations and rewrites every reference to them +in the three libraries, at the exact ranges recorded in the `.ilean` files (full names, names +relative to namespaces and `open`s, dot notation), and in comments and READMEs. A declaration is +*deferred* (left tidy) when its statement names another tidy declaration, gets a tidy hypothesis +from a `variable` command, or is written inside a tidy namespace. A restated proof is *translated* +when every tidy declaration it names has a plain counterpart (a twin or a restated lemma): those +names are replaced in place. Otherwise it is *wrapped*: the old proof runs on tidy hypotheses +(`have h := h.tidy`) and its conclusion is converted (`refine .of_tidy ?_`); statements that are +not a bare predicate are transported with `simpa only []`. A reference from a proof +that stays tidy keeps its old type: the application becomes `(lemma args).tidy`, with `.of_tidy` +around tidy arguments, and references to case 1 originals stay. `.of_tidy (x.tidy)` round trips +are then removed. Whatever cannot be done mechanically is listed as manual work. + +With `--verify`, the three libraries are built after the rewrite, repeatedly: a translated proof +that fails is wrapped instead, and a wrapped proof or a client declaration that fails (typically +a tidy `fun_prop` that used a restated `@[fun_prop]` lemma) is preceded by +`attribute [local fun_prop] ComputableInPolyTime.tidy in`. Remaining failures are reported. With +`--stub-failures` (measurement only, never commit the result), proofs that still fail become +`sorry`, so that later rounds reach the modules downstream of them. `--diff` writes the plan as a +patch instead of rewriting files. + +The registry is a JSON array of `{"original": name, "plain": name, "module": module}` objects, the +format of #608's `#mirror_pairs`. Until S1 lands, `scripts/tidy_mirror_registry.json` is a stub, +written by `stub-registry`: the existing declarations whose name is the plain rename of a tidy +theorem and whose statement is its plain transport. + +Declarations, statements and references come from `scripts/quality_report.py` and +`scripts/QualityReport.lean`, which read the build outputs of +`lake build Complexity ComplexityTests ComplexityAbstracts`. +""" + +from __future__ import annotations + +import argparse +import difflib +import json +import re +import subprocess +import sys +from collections import Counter, defaultdict +from dataclasses import dataclass, field +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +sys.path.insert(0, str(ROOT / "scripts")) +import quality_report as qr # noqa: E402 +from proof_lengths import masks # noqa: E402 + +ALLOWLIST = ROOT / "scripts/tidy_allowlist.txt" +REGISTRY = ROOT / "scripts/tidy_mirror_registry.json" +TM = "Turing.MultiTapeTM." + + +@dataclass(frozen=True) +class Notion: + """A tidy predicate with a same-bound plain counterpart and their equivalence.""" + tidy: str + plain: str + iff: str # `plain ↔ tidy` + + @property + def to_tidy(self) -> str: + return self.plain + ".tidy" + + @property + def of_tidy(self) -> str: + return self.plain + ".of_tidy" + + @property + def dot_of_tidy(self) -> str: + """`Tidy.computable…`: `of_tidy` for dot notation on a tidy hypothesis.""" + last = self.plain.rsplit(".", 1)[1] + return self.tidy + "." + last[0].lower() + last[1:] + + @property + def bridges(self) -> set[str]: + return {self.to_tidy, self.of_tidy, self.iff, self.dot_of_tidy} + + +NOTIONS = ( + Notion(TM + "ComputableTidilyInPolyTime", TM + "ComputableInPolyTime", + TM + "computableInPolyTime_iff_computableTidilyInPolyTime"), + Notion(TM + "ComputableTidilyInPolySpace", TM + "ComputableInPolySpace", + TM + "computableInPolySpace_iff_computableTidilyInPolySpace"), + Notion(TM + "ComputableTidilyInSpace", TM + "ComputableInSpace", + TM + "computableInSpace_iff_computableTidilyInSpace"), + Notion(TM + "ComputableTidilyInO", TM + "ComputableInO", + TM + "computableInO_iff_computableTidilyInO"), + Notion("Cslib.Complexity.ComputableTidilyInFPTTime", "Cslib.Complexity.ComputableInFPTTime", + "Cslib.Complexity.computableInFPTTime_iff_computableTidilyInFPTTime"), +) +BY_TIDY = {n.tidy: n for n in NOTIONS} +BRIDGES = set().union(*(n.bridges for n in NOTIONS)) +# `computableTidilyInPolyTime_foo` → `computableInPolyTime_foo`, for the supported notions only. +RENAME = re.compile(r"([cC])omputableTidily(In(?:PolyTime|PolySpace|Space|O|FPTTime))" + r"(?![A-Za-z0-9])") +# Name components that still say "tidy" after renaming mark a plain/tidy helper. +TIDY_WORD = re.compile(r"(?i)tid(?:y|ily)") + + +def plain_name(name: str) -> str: + return RENAME.sub(r"\1omputable\2", name) + + +def is_tidy_constant(name: str) -> bool: + """Mirror of `isTidy` in `scripts/QualityReport.lean`.""" + last = name.rsplit(".", 1)[-1] + return last.startswith(("ComputableTidily", "ComputesTidily", "IsTidy")) + + +def load_allowlist(path: Path) -> set[str]: + """Library source paths (relative to the repository root), one per line; `#` comments.""" + return {line.split("#", 1)[0].strip() for line in path.read_text().splitlines()} - {""} + + +def load_registry(path: Path | None) -> dict[str, str]: + """original → plain twin, from a JSON array of `{"original", "plain", "module"}` objects (the + output of #608's `#mirror_pairs`), or an object holding it under `"pairs"`.""" + if path is None or not path.exists(): + return {} + data = json.loads(path.read_text()) + if isinstance(data, dict): + data = data.get("pairs", []) + registry = {} + for row in data: + if not (isinstance(row, dict) and isinstance(row.get("original"), str) + and isinstance(row.get("plain"), str)): + raise ValueError(f"{path}: malformed registry entry {row!r}") + registry[row["original"]] = row["plain"] + return registry + + +# --- Classification ----------------------------------------------------------------------------- + +@dataclass +class Entry: + name: str + module: str + path: str # relative to `Complexity/` + area: str + kind: str # theorem, definition, structure field, constructor, instance + case: str # "1", "2", "3" or "unclassifiable" + reason: str = "" + target: str = "" # the twin (case 1) or the new name (case 2) + notions: list[str] = field(default_factory=list) + unsupported: list[str] = field(default_factory=list) + body_only: bool = False # mentions tidy only in its exposed body + implicit: list[str] = field(default_factory=list) + users: int = 0 # other modules that name it + detail: str = "" + collision: dict | None = None + warnings: list[str] = field(default_factory=list) + + +def decl_kind(decl: dict) -> str: + if decl["role"] == "member": + return "constructor" if decl["kind"] == "ctor" else "structure field" + if decl["keyword"] == "instance" or "instance" in decl["attrs"]: + return "instance" + if decl["kind"] == "thm": + return "theorem" + return "definition" + + +def classify_decl(decl: dict, const: dict, registry: dict[str, str], constants: dict[str, dict], + private_names: dict[str, set[str]]) -> Entry: + """The S2 case of one public declaration whose statement mentions a tidy constant.""" + name = decl["name"] + tidy = sorted(set(const.get("tidy", [])) | set(const.get("tb", []))) + entry = Entry(name=name, module=decl["module"], path=decl["path"], area=decl["area"], + kind=decl_kind(decl), case="unclassifiable", + notions=[t for t in tidy if t in BY_TIDY], + unsupported=[t for t in tidy if t not in BY_TIDY], + body_only=not const.get("tidy"), implicit=list(decl.get("implicit", [])), + users=len(decl.get("lib_refs", ())) + len(decl.get("test_refs", ())) + + len(decl.get("abstract_refs", ()))) + last = name.rsplit(".", 1)[-1] + if "deprecated" in decl["attrs"]: + entry.reason, entry.detail = "deprecated alias", "#588: delete, no aliases" + elif is_tidy_constant(name) and entry.kind != "theorem": + entry.reason = "tidy notion definition" + elif name in BRIDGES or (entry.kind == "theorem" and TIDY_WORD.search(plain_name(last))): + entry.reason, entry.detail = "bridge", "kept for proofs; S3 stores it internally" + elif entry.unsupported: + entry.reason = "unsupported notion" + entry.detail = "no same-bound plain equivalence: " + ", ".join( + f"`{t}`" for t in entry.unsupported) + elif entry.kind != "theorem": + entry.case = "3" + elif name in registry: + twin = registry[name] + entry.target = twin + if twin not in constants: + entry.reason, entry.detail = "registered twin missing", f"`{twin}` is not built" + else: + entry.case = "1" + if constants[twin].get("ph") != const.get("ph"): + entry.warnings.append("the twin's statement is not the syntactic plain " + "transport (checked only up to definitional equality " + "by S1)") + else: + target = plain_name(name) + entry.target = target + taken = target in constants or target in private_names.get(decl["module"], set()) + if target != name and taken: + existing = constants.get(target) + same = existing is not None and existing.get("ph") == const.get("ph") + entry.collision = { + "target": target, "module": existing["m"] if existing else decl["module"], + "equivalent": same, "private": existing is None or not existing["e"]} + entry.reason = "collision" + entry.detail = ("the target has the plain statement but is not a registered twin" + if same else "the target exists with another statement") + else: + entry.case = "2" + return entry + + +def private_by_module(constants: dict[str, dict]) -> dict[str, set[str]]: + """The user-facing names of private constants, by module.""" + out: dict[str, set[str]] = defaultdict(set) + for name, const in constants.items(): + if name.startswith("_private."): + rest = name.removeprefix("_private.").split(".0.", 1) + if len(rest) == 2: + out[const["m"]].add(rest[1]) + return out + + +def classify_all(model: "Model", registry: dict[str, str]) -> list[Entry]: + entries = [] + privates = private_by_module(model.constants) + for name, decl in sorted(model.decls.items()): + const = model.constants.get(name, {}) + if decl["role"] == "generated" or not (const.get("tidy") or const.get("tb")): + continue + if "Complexity/" + decl["path"] in model.allowlist: + continue + entries.append(classify_decl(decl, const, registry, model.constants, privates)) + targets = Counter(e.target for e in entries if e.case == "2" and e.target != e.name) + for e in entries: + if e.case == "2" and e.target != e.name and targets[e.target] > 1: + e.case, e.reason = "unclassifiable", "collision" + e.detail = "another declaration renames to the same target" + e.collision = {"target": e.target, "module": e.module, "equivalent": False, + "private": False} + return entries + + +def registry_problems(registry: dict[str, str], constants: dict[str, dict]) -> list[str]: + out = [] + for original, twin in sorted(registry.items()): + if original not in constants: + out.append(f"`{original}` is registered but not in the build") + elif twin not in constants: + out.append(f"twin `{twin}` of `{original}` is not in the build") + return out + + +# --- Loading ------------------------------------------------------------------------------------ + +class Model: + """Declarations, constants and references of the built libraries.""" + + def __init__(self, build_dir: Path, allowlist: set[str]): + pairs = ",".join(f"{n.tidy}={n.plain}" for n in NOTIONS) + self.lib = qr.Library(build_dir, pairs) + 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.allowlist = allowlist + self._users: dict[str, list[tuple[str, list]]] | None = None + self._known: set[str] | None = None + + def users(self, name: str) -> list[tuple[str, list]]: + """`(module, usage)` for every reference to `name` in the three libraries.""" + if self._users is None: + self._users = defaultdict(list) + for module in self.lib.ileans: + for ref, _, info in self.lib.references(module): + for usage in info["usages"]: + self._users[ref].append((module, usage)) + return self._users.get(name, []) + + @property + def known(self) -> set[str]: + """Every constant name the build defines or references, for name resolution.""" + if self._known is None: + self._known = set(self.constants) + for module in self.lib.ileans: + self._known.update(ref for ref, _, _ in self.lib.references(module)) + return self._known + + +# --- Report ------------------------------------------------------------------------------------- + +AREA_ORDER = [name for name, _, _ in qr.AREAS] + [qr.OTHER_AREA] + + +def summary(entries: list[Entry]) -> dict: + by_area: dict[str, Counter] = defaultdict(Counter) + reasons: Counter = Counter() + for e in entries: + by_area[e.area]["total"] += 1 + by_area[e.area][e.case] += 1 + if e.case == "unclassifiable": + reasons[e.reason] += 1 + total = Counter() + for counts in by_area.values(): + total.update(counts) + return {"areas": {a: dict(by_area[a]) for a in AREA_ORDER if a in by_area}, + "total": dict(total), "unclassifiable_reasons": dict(reasons.most_common())} + + +def markdown_report(report: dict, limit: int = 40) -> str: + s = report["summary"] + dirty = " with uncommitted changes" if report["dirty"] else "" + out = [f"Revision `{report['revision']}`{dirty}; build outputs {report['outputs']}. " + f"Allowlist: {report['allowlist_size']} modules. " + f"Registry: {report['registry_size']} pairs (`{report['registry']}`).", "", + "### Public declarations whose statement mentions a tidy predicate", "", + "| Area | Total | (1) Registered twin | (2) Rename and restate | " + "(3) Definition or field | Unclassifiable |", "|---|--:|--:|--:|--:|--:|"] + for area, c in list(s["areas"].items()) + [("Total", s["total"])]: + out.append(f"| {area} | {c.get('total', 0):,} | {c.get('1', 0):,} | {c.get('2', 0):,} | " + f"{c.get('3', 0):,} | {c.get('unclassifiable', 0):,} |") + out += ["", "Unclassifiable, by reason: " + "; ".join( + f"{r} ({n})" for r, n in s["unclassifiable_reasons"].items()) + "."] + collisions = [e for e in report["entries"] if e["collision"]] + if collisions: + out += ["", "### Collisions", "", + "| Declaration | Target | Target module | Same plain statement |", + "|---|---|---|---|"] + for e in collisions[:limit]: + c = e["collision"] + out.append(f"| `{e['name']}` | `{c['target']}` | `{c['module']}` | " + f"{'yes' if c['equivalent'] else 'no'} |") + if len(collisions) > limit: + out.append(f"| … {len(collisions) - limit} more in the JSON report | | | |") + unsupported = Counter(t for e in report["entries"] for t in e["unsupported"]) + if unsupported: + out += ["", "Tidy notions without a same-bound plain equivalence, by declarations " + "mentioning them: " + ", ".join(f"`{t}` ({n})" for t, n in + unsupported.most_common()) + "."] + third = [e for e in report["entries"] if e["case"] == "3"] + if third: + out += ["", "### Case 3: definitions and structure fields", ""] + out += [f"* `{e['name']}` ({e['kind']}, {e['area']})" for e in third[:limit]] + if len(third) > limit: + out.append(f"* … {len(third) - limit} more in the JSON report") + if report["registry_problems"]: + out += ["", "Registry problems: " + "; ".join(report["registry_problems"][:limit])] + return "\n".join(out) + "\n" + + +# --- Lean source helpers (unit-tested in scripts/test_tidy_sweep.py) ---------------------------- + +OPENERS, CLOSERS = "([{⦃⟨‹", ")]}⦄⟩›" +IDENT = re.compile(qr.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"} +COMMAND_KEYWORD = re.compile(r"#?[A-Za-z_]+") +NAME_ONLY_COMMANDS = {"#print", "#check", "#guard_msgs", "attribute", "open", "export", "#eval", + "#reduce", "#synth", "add_decl_doc", "#lint", "#help"} +LEMMA_LIST_TACTIC = re.compile( + r"\b(?:simp|simp_all|dsimp|simp_rw|rw|rwa|rewrite|erw|nth_rewrite|nth_rw|simpa|fun_prop|" + r"aesop|norm_num|field_simp|grind|polytime|positivity|unfold|delta|gcongr|subst_vars|" + r"continuity|measurability|bound|decide|omega|linarith|nlinarith|exact\?|apply\?|" + r"rw_mod_cast|push_cast|norm_cast|simp_arith|conv)\b[^\[\]\n]*$") + + +def match_bracket(mask: str, i: int, limit: int | None = None) -> int: + """The index of the bracket closing the one at `mask[i]`, or -1.""" + depth, end = 0, len(mask) if limit is None else limit + for j in range(i, end): + char = mask[j] + if char in OPENERS: + depth += 1 + elif char in CLOSERS: + depth -= 1 + if depth == 0: + return j + return -1 + + +def find_top_level(mask: str, start: int, end: int, token: str) -> int: + """The first `token` at bracket depth 0 in `mask[start:end]`, or -1. `:` excludes `:=`.""" + depth = 0 + for j in range(start, end): + char = mask[j] + if char in OPENERS: + depth += 1 + elif char in CLOSERS: + depth -= 1 + elif depth == 0 and mask.startswith(token, j): + if token == ":" and (mask.startswith(":=", j) or mask.startswith("::", j) + or (j and mask[j - 1] == ":")): + continue + return j + return -1 + + +def line_indent(text: str, offset: int) -> int: + start = text.rfind("\n", 0, offset) + 1 + return len(text[start:]) - len(text[start:].lstrip(" ")) + + +def column(text: str, offset: int) -> int: + return offset - (text.rfind("\n", 0, offset) + 1) + + +def atom_end(mask: str, i: int, limit: int) -> int: + """The end of the atom (identifier, number, `?_`, bracket group, `.ident`) at `i` together + with directly attached projections (`.field`, `.1`), or `i` when no atom starts there.""" + if i >= limit: + return i + char = mask[i] + if char in OPENERS: + end = match_bracket(mask, i, limit) + if end < 0: + return i + j = end + 1 + elif char == "." and i + 1 < limit and IDENT.match(mask, i + 1): + j = IDENT.match(mask, i + 1).end() + elif char == "?" and mask.startswith("?_", i): + j = i + 2 + elif char == "@" and i + 1 < limit and IDENT.match(mask, i + 1): + j = IDENT.match(mask, i + 1).end() + elif char.isdigit(): + j = i + while j < limit and (mask[j].isalnum() or mask[j] == "."): + j += 1 + else: + match = IDENT.match(mask, i) + if not match or match[0].rstrip(".") in KEYWORDS: + return i + j = match.end() + while j < limit and mask[j] == "." and j + 1 < limit and ( + mask[j + 1].isdigit() or IDENT.match(mask, j + 1)): + j = IDENT.match(mask, j + 1).end() if IDENT.match(mask, j + 1) else j + 2 + return min(j, limit) + + +NAMED_ARG = re.compile(r"\(\s*[^\W\d][\w'₀-₉]*\s*:=") + + +def parse_args(mask: str, pos: int, limit: int, count: int, base_indent: int, + named: list[tuple[int, int]] | None = None) -> list[tuple[int, int]]: + """Up to `count` positional application arguments after `pos`: atoms separated by blanks, + continuing onto lines indented more than `base_indent`. Named arguments `(x := e)` are + skipped and, when `named` is given, appended to it.""" + args = [] + i = pos + while len(args) < count and i < limit: + j = i + while j < limit and mask[j] in " \t": + j += 1 + if j < limit and mask[j] == "\n": + k = j + while k < limit and mask[k] in " \t\n": + k += 1 + if k >= limit or line_indent(mask, k) <= base_indent: + break + j = k + if j == i and args: + break # no blank after the previous argument + end = atom_end(mask, j, limit) + if end == j: + break + if NAMED_ARG.match(mask, j): + if named is not None: + named.append((j, end)) + else: + args.append((j, end)) + i = end + return args + + +def strip_space(mask: str, start: int, end: int) -> tuple[int, int]: + while start < end and mask[start].isspace(): + start += 1 + while end > start and mask[end - 1].isspace(): + end -= 1 + return start, end + + +def is_atomic_application(mask: str, start: int, end: int) -> tuple[int, int] | None: + """For text `P args` in `mask[start:end]` made of atoms only, the span of `P`; else None.""" + start, end = strip_space(mask, start, end) + head = atom_end(mask, start, end) + if head == start: + return None + args = parse_args(mask, head, end, 10 ** 6, -1) + last = args[-1][1] if args else head + return (start, head) if strip_space(mask, last, end)[0] == end else None + + +@dataclass +class Binder: + start: int + end: int + bracket: str + names: list[str] + type_start: int + type_end: int + default: bool + + +@dataclass +class DeclText: + start: int + sel_start: int + sel_end: int + end: int + binders: list[Binder] + colon: int # the `:` before the type, or -1 + assign: int # the `:=` before the body, or -1 + problems: list[str] + + +def parse_decl(mask: str, start: int, sel_start: int, sel_end: int, end: int) -> DeclText: + """Binders, type and body of the declaration whose name ends at `sel_end`.""" + assign = find_top_level(mask, sel_end, end, ":=") + stop = assign if assign >= 0 else end + binders, problems, colon = [], [], -1 + i = sel_end + if mask.startswith(".{", i): + i = match_bracket(mask, i + 1, stop) + 1 + while i < stop: + char = mask[i] + if char.isspace(): + i += 1 + elif char in "([{⦃": + close = match_bracket(mask, i, stop) + if close < 0: + problems.append("unbalanced binder") + break + inner = find_top_level(mask, i + 1, close, ":") + default = find_top_level(mask, i + 1, close, ":=") + if inner < 0: + names, type_start = mask[i + 1:close].split(), close + else: + names, type_start = mask[i + 1:inner].split(), inner + 1 + type_end = default if default >= 0 else close + binders.append(Binder(i, close + 1, char, names, type_start, type_end, + default >= 0)) + i = close + 1 + elif char == ":": + colon = i + break + else: + problems.append("binder without brackets") + break + if assign < 0: + problems.append("no `:=` (pattern-matching definition)") + return DeclText(start, sel_start, sel_end, end, binders, colon, assign, problems) + + +def proof_parts(text: str, assign: int, end: int) -> tuple[str, bool]: + """The text after `:=` and whether it is a tactic block.""" + body = text[assign + 2:end] + return body, re.match(r"\s*by(?:\s|$)", body) is not None + + +def collapse(text: str) -> str: + return " ".join(text.split()) + + +# --- Scopes and names --------------------------------------------------------------------------- + +SCOPE_COMMAND = re.compile( + r"^(?P(?:@\[[^\]\n]*\]\s*)?(?:(?:public|private|noncomputable|protected|meta)\s+)*)" + r"(?Pnamespace|section|end|open|mutual)\b(?P[^\n]*)", re.M) + + +def namespaces_of(names) -> set[str]: + """Every name and every proper prefix of a name, as namespaces.""" + out = set() + for name in names: + parts = name.split(".") + for i in range(1, len(parts) + 1): + out.add(".".join(parts[:i])) + return out + + +class Scopes: + """The current namespace and opened namespaces at each offset of a masked source.""" + + def __init__(self, mask: str, namespaces: set[str]): + self.points: list[tuple[int, str, tuple[str, ...]]] = [(0, "", ())] + self.once: list[tuple[int, int, tuple[str, ...]]] = [] + stack: list[tuple[str, str, list[str]]] = [] + starts = [m.start() for m in qr.COMMAND_START.finditer(mask)] + [len(mask)] + for match in SCOPE_COMMAND.finditer(mask): + kw, rest = match["kw"], match["rest"].split() + namespace = ".".join(n for k, n, _ in stack if k == "namespace" and n) + opens = [o for _, _, os in stack for o in os] + if kw == "namespace" and rest: + stack.append(("namespace", rest[0], [])) + elif kw in ("section", "mutual"): + stack.append((kw, rest[0] if rest and kw == "section" else "", [])) + elif kw == "end": + if stack: + stack.pop() + elif kw == "open": + one_shot = bool(rest) and rest[-1] == "in" + words = [w for w in (rest[:-1] if one_shot else rest) + if w not in ("scoped", "hiding", "renaming", "→", "private") + and not w.startswith("(") and IDENT.fullmatch(w)] + resolved = [] + for word in words: + prefixes = [".".join(namespace.split(".")[:i]) + for i in range(len(namespace.split(".")), -1, -1)] if namespace \ + else [""] + found = [p + "." + word if p else word for p in prefixes + opens + resolved + if (p + "." + word if p else word) in namespaces] + resolved += found or [word] + if one_shot: + after = next((s for s in starts if s > match.end()), len(mask)) + following = next((s for s in starts if s > after), len(mask)) + self.once.append((match.start(), following, tuple(resolved))) + continue + if not stack: + stack.append(("file", "", [])) + stack[-1][2].extend(resolved) + namespace = ".".join(n for k, n, _ in stack if k == "namespace" and n) + opens = [o for _, _, os in stack for o in os] + self.points.append((match.end(), namespace, tuple(opens))) + + def at(self, offset: int) -> tuple[str, tuple[str, ...]]: + namespace, opens = "", () + for point, ns, os in self.points: + if point > offset: + break + namespace, opens = ns, os + extra = tuple(o for start, end, os in self.once if start <= offset < end for o in os) + return namespace, opens + extra + + def prefixes(self, offset: int) -> list[str]: + """Namespaces a written name may be relative to, innermost first (`""` is the root).""" + namespace, opens = self.at(offset) + parts = namespace.split(".") if namespace else [] + return [".".join(parts[:i]) for i in range(len(parts), -1, -1)] + list(opens) + + +def written_name(target: str, prefixes: list[str], known: set[str]) -> str: + """The shortest suffix of `target` that resolves to it, and to nothing else, from a position + whose namespace prefixes and opened namespaces are `prefixes`.""" + parts = target.split(".") + for k in range(1, len(parts) + 1): + suffix = ".".join(parts[-k:]) + hits = {p + "." + suffix if p else suffix for p in prefixes} + resolved = {h for h in hits if h in known or h == target} + if resolved == {target}: + return suffix + return target + + +def renamed_token(token: str, old: str, new: str) -> str | None: + """`token` (a written form of `old`) with the renamed part, when the written prefix still + resolves the same way (`old = P.token` and `new = P.result`); otherwise None.""" + at = "@" if token.startswith("@") else "" + bare = token[len(at):] + root = "_root_." if bare.startswith("_root_.") else "" + bare = bare[len(root):] + if not (old == bare or old.endswith("." + bare)): + return None + prefix = old[:len(old) - len(bare)] + if not new.startswith(prefix): + return None + result = new[len(prefix):] + if not result or (prefix and result.startswith(".")): + return None + return at + root + result + + +# --- Edits -------------------------------------------------------------------------------------- + +@dataclass +class Replace: + start: int + end: int + text: str + + +@dataclass +class Wrap: + """Text inserted before `open` and after `close`; `site` orders wraps with equal spans (the + wrap of the site that starts first is outermost).""" + open: int + close: int + before: str + after: str + site: int + + +@dataclass +class Region: + """A span whose edited text is then transformed by `build`.""" + start: int + end: int + build: object + decl: str + + +def render(text: str, replaces: list[Replace], wraps: list[Wrap], lo: int, hi: int) -> str: + """`text[lo:hi]` with the replacements and wraps inside it applied. At one position, wraps + close (innermost first) before others open (outermost first), then a replacement starts.""" + reps = sorted((r for r in replaces if lo <= r.start and r.end <= hi), + key=lambda r: (r.start, r.end)) + ws = [w for w in wraps if lo <= w.open and w.close <= hi] + points = sorted({r.start for r in reps} | {w.open for w in ws} | {w.close for w in ws}) + starting = defaultdict(list) + for r in reps: + starting[r.start].append(r) + out, cur = [], lo + for p in points: + if p < cur: + continue # inside a replaced span + out.append(text[cur:p]) + out += [w.after for w in sorted((w for w in ws if w.close == p), + key=lambda w: (-w.open, -w.site))] + out += [w.before for w in sorted((w for w in ws if w.open == p), + key=lambda w: (-w.close, w.site))] + cur = p + for r in starting.get(p, []): + out.append(r.text) + cur = max(cur, r.end) + out.append(text[cur:hi]) + return "".join(out) + + +def apply_edits(text: str, replaces: list[Replace], wraps: list[Wrap], + regions: list[Region]) -> str: + out, cur = [], 0 + for region in sorted(regions, key=lambda r: r.start): + out.append(render(text, replaces, wraps, cur, region.start)) + out.append(region.build(render(text, replaces, wraps, region.start, region.end))) + cur = region.end + out.append(render(text, replaces, wraps, cur, len(text))) + return "".join(out) + + +# --- Round trips -------------------------------------------------------------------------------- + +OF_TIDY = re.compile(r"(? tuple[str, int]: + """Remove `of_tidy (x.tidy)`, `of_tidy <| x.tidy` and `x.tidy.computableIn…` round trips, + where `x` is an atom. Returns the new text and the number of removals.""" + count = 0 + while True: + mask = masks(text)[1] + change = None + for match in DOT_ROUND_TRIP.finditer(mask): + change = (match.start(), match.end(), "") + break + if change is None: + for match in OF_TIDY.finditer(mask): + i = match.end() + while i < len(mask) and mask[i] in " \t": + i += 1 + pipe = mask.startswith("<|", i) + if pipe: + i += 2 + while i < len(mask) and mask[i] in " \t": + i += 1 + end = atom_end(mask, i, len(mask)) + if end == i: + continue + inner = (i, end) + if mask[i] == "(" and match_bracket(mask, i) == end - 1: + inner = strip_space(mask, i + 1, end - 1) + start, stop = inner + if not mask[start:stop].endswith(".tidy") or atom_end(mask, start, stop) != stop: + continue + core_end = stop - len(".tidy") + if atom_end(mask, start, core_end) != core_end: + continue + if pipe: + after = end + while after < len(mask) and mask[after] in " \t": + after += 1 + if after < len(mask) and mask[after] not in CLOSERS + "\n,": + continue + change = (match.start(), end, text[start:core_end]) + break + if change is None: + return text, count + start, end, new = change + new_mask = masks(new)[1] + if (start > 0 and text[start - 1] == "(" and end < len(text) and text[end] == ")" + and atom_end(new_mask, 0, len(new)) == len(new) and not new.startswith("@")): + start, end = start - 1, end + 1 + text = text[:start] + new + text[end:] + count += 1 + + +# --- Wrapping ----------------------------------------------------------------------------------- + +@dataclass +class Hyp: + names: list[str] + old_type: str # one line + simple: bool + + +def reindent(lines: list[str], delta: int) -> list[str] | None: + """Shift lines by `delta` columns; None when that would remove non-blank text.""" + out = [] + for line in lines: + if not line.strip(): + out.append("") + elif delta >= 0: + out.append(" " * delta + line) + elif len(line) - len(line.lstrip(" ")) >= -delta: + out.append(line[-delta:]) + else: + return None + return out + + +def wrap_proof(body: str, body_column: int, decl_indent: int, hyps: list[Hyp], + conclusion: str | None, simple_conclusion: bool, iffs: str) -> str | None: + """The new text after `:=` for a proof `body` of the old (tidy) statement, now stated plainly: + tidy hypotheses are recovered, and the old conclusion converted. `body_column` is the column + of the first character of `body`. None when the layout cannot be preserved.""" + stripped = body.lstrip() + lead = body[:len(body) - len(stripped)] + first_col = body_column + len(lead) if "\n" not in lead else len(lead.rsplit("\n", 1)[1]) + stripped = stripped.rstrip() + tactic = re.match(r"by(?=\s|$)", stripped) is not None + if not hyps and simple_conclusion and not tactic: + return f"{lead}.of_tidy ({stripped})" + k = decl_indent + 2 + rebind = [] + for hyp in hyps: + for name in hyp.names: + rebind.append(f"have {name} := {name}.tidy" if hyp.simple else + f"have {name} : {hyp.old_type} := by simpa only [{iffs}] using {name}") + if tactic: + rest = stripped[2:] + if rest.lstrip(" \t").startswith("\n") or not rest.strip(): + lines = rest.lstrip(" \t")[1:].split("\n") + nonblank = [ln for ln in lines if ln.strip()] + if not nonblank: + return None + k = min(len(ln) - len(ln.lstrip(" ")) for ln in nonblank) + else: + first_line, _, tail = rest.lstrip(" \t").partition("\n") + tactic_col = first_col + 2 + (len(rest) - len(rest.lstrip(" \t"))) + shifted = reindent(tail.split("\n"), k - tactic_col) if tail else [] + if shifted is None: + return None + lines = [" " * k + first_line] + shifted + pad = " " * k + out = [pad + line for line in rebind] + if conclusion is None: + out += lines + elif simple_conclusion: + out += [pad + "refine .of_tidy ?_"] + lines + else: + inner = reindent(lines, 2) + out += [pad + f"have this : {conclusion} := by"] + inner + \ + [pad + f"simpa only [{iffs}] using this"] + return " by\n" + "\n".join(out) + first, _, tail = stripped.partition("\n") + tail_lines = tail.split("\n") if tail else [] + nonblank = [ln for ln in tail_lines if ln.strip()] + shift = 0 + if nonblank: + least = min(len(ln) - len(ln.lstrip(" ")) for ln in nonblank) + shift = max(0, k + 2 - least) + tail_lines = reindent(tail_lines, shift) or tail_lines + pad = " " * k + out = [pad + line for line in rebind] + term = "\n".join([first] + tail_lines) + if conclusion is None: + out.append(pad + "exact " + term) + elif simple_conclusion: + out.append(pad + "exact .of_tidy (" + term + ")") + else: + out += [pad + f"have this : {conclusion} :=", pad + " " + term, + pad + f"simpa only [{iffs}] using this"] + return " by\n" + "\n".join(out) + + +# --- Planning ----------------------------------------------------------------------------------- + +@dataclass +class Manual: + path: str + line: int + decl: str + kind: str + detail: str = "" + + +@dataclass +class Ref: + name: str + start: int + end: int + decl: str | None + + +class SourceFile: + def __init__(self, path: Path, namespaces: set[str]): + self.path = path + self.text = path.read_text(encoding="utf-8") + self.code, self.mask = masks(self.text) if path.suffix == ".lean" else (self.text,) * 2 + self.lines = self.text.split("\n") + 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._namespaces = namespaces + self._scopes: Scopes | None = None + + @property + def scopes(self) -> Scopes: + if self._scopes is None: + self._scopes = Scopes(self.mask, self._namespaces) + return 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) + + def at_range(self, line: int, column: int) -> int: + """The offset of a 1-based line and code-point column (declaration ranges).""" + return self.starts[line - 1] + column + + def line_of(self, offset: int) -> int: + """The 1-based line of an offset.""" + return self.text.count("\n", 0, offset) + 1 + + def command_keyword(self, offset: int) -> str: + starts = [s for s in self.commands if s <= offset] + if not starts: + return "" + match = COMMAND_KEYWORD.match(self.mask, starts[-1]) + return match[0] if match else "" + + def comment_spans(self) -> list[tuple[int, int]]: + if self.path.suffix != ".lean": + return [(0, len(self.text))] + spans, i = [], 0 + while i < len(self.text): + if self.code[i] != self.text[i]: + j = i + while j < len(self.text) and self.code[j] != self.text[j] or ( + j < len(self.text) and self.text[j] == "\n" and j + 1 < len(self.text) + and self.code[j + 1] != self.text[j + 1]): + j += 1 + spans.append((i, j)) + i = j + else: + i += 1 + return spans + + +@dataclass +class FileEdits: + replaces: list[Replace] = field(default_factory=list) + wraps: list[Wrap] = field(default_factory=list) + regions: list[Region] = field(default_factory=list) + + +class Planner: + """The edits of one area's batch: case 2 declarations restated and renamed, their clients + converted, and case 1 twins used in translated proofs.""" + + def __init__(self, model: Model, entries: list[Entry], registry: dict[str, str], area: str, + force_wrap: frozenset[str] = frozenset(), + force_bridge: frozenset[tuple[str, str]] = frozenset(), + stub: frozenset[tuple[str, str]] = frozenset()): + self.model, self.area, self.force_wrap = model, area, force_wrap + self.force_bridge, self.stub = force_bridge, stub + self.entries = {e.name: e for e in entries} + self.batch = {e.name: e for e in entries if e.area == area and e.case == "2"} + self.renames = {name: e.target for name, e in self.batch.items()} + self.twins = {o: p for o, p in registry.items() if p in model.constants} + self.files: dict[Path, FileEdits] = defaultdict(FileEdits) + self.sources: dict[Path, SourceFile] = {} + self.manual: list[Manual] = [] + self.decls: dict[str, dict] = {} + self.spans: dict[str, list[tuple[int, int, str]]] = defaultdict(list) + self.needs: dict[str, dict[str, bool]] = defaultdict(dict) + self.sites = Counter() + self.imports: list[tuple[str, str, bool]] = [] + self.known = model.known | set(self.renames.values()) + self.namespaces = namespaces_of(self.known) + self.round_trips = 0 + self.deferred: dict[str, list[str]] = {} + self.bridged: list[str] = [] + self.stubbed: list[str] = [] + + # Sources and references. + + def source(self, path: Path) -> SourceFile: + if path not in self.sources: + self.sources[path] = SourceFile(path, self.namespaces) + return self.sources[path] + + def refs(self, module: str) -> list[Ref]: + src = self.source(qr.source_path(module)) + out = [] + for name, _, info in self.model.lib.references(module): + for u in info["usages"]: + out.append(Ref(name, src.at(u[0], u[1]), src.at(u[2], u[3]), + u[4] if len(u) == 5 else None)) + return out + + def ref_kind(self, name: str) -> str: + owner = qr.owner_of(name, self.model.owners) or name + if name in BY_TIDY: + return "pred" + if owner in self.renames: + return "renamed" + if name in self.twins: + return "twin" + if name in BRIDGES: + return "bridge" + const = self.model.constants.get(name, {}) + if const.get("tidy") or const.get("tb") or is_tidy_constant(name): + return "tidy" + return "plain" + + 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 + 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) + + def note(self, path: Path, offset: int, decl: str | None, kind: str, detail: str = ""): + src = self.source(path) + self.manual.append(Manual(str(path.relative_to(ROOT)), src.line_of(offset), decl or "", + kind, detail)) + + def need(self, module: str, constant: str, public: bool) -> None: + defining = self.model.constants.get(constant, {}).get("m") + if defining and defining != module: + self.needs[module][defining] = self.needs[module].get(defining, False) or public + + def notions_of(self, name: str) -> list[Notion]: + const = self.model.constants.get(name, {}) + return [BY_TIDY[t] for t in const.get("tidy", []) if t in BY_TIDY] + + # Names. + + def rename_at(self, src: SourceFile, start: int, end: int, old: str, new: str) -> str | None: + """The written form of `new` replacing the reference to `old` at `start`.""" + token = src.text[start:end] + if old == new: + return token + if start and src.text[start - 1] == ".": # field or leading-dot notation + if old.rsplit(".", 1)[-1] == new.rsplit(".", 1)[-1]: + return token + if old.rsplit(".", 1)[0] == new.rsplit(".", 1)[0] and "." not in token: + return new.rsplit(".", 1)[-1] + return None + candidate = renamed_token(token, old, new) + if candidate is not None and not candidate.lstrip("@").startswith("_root_."): + return candidate + at = "@" if token.startswith("@") else "" + return at + written_name(new, src.scopes.prefixes(start), self.known) + + # Declarations. + + def plan(self) -> "Planner": + analyses = {name: self.analyse_decl(self.batch[name]) for name in sorted(self.batch)} + changed = True + while changed: # a statement naming a deferred declaration is deferred too + changed = False + for name, a in analyses.items(): + if name in self.deferred or a is None: + continue + reasons = list(a["defer"]) + [ + f"statement names deferred `{x.name}`" for x in a["sig_refs"] + if (qr.owner_of(x.name, self.model.owners) or x.name) in self.deferred] + if reasons: + self.deferred[name] = reasons + changed = True + for name, a in analyses.items(): + if a is None: + self.deferred.setdefault(name, ["declaration range missing"]) + for name in self.deferred: + self.renames.pop(name, None) + for name in sorted(self.batch): + if name in self.deferred: + self.defer(name, analyses[name]) + else: + self.plan_decl(self.batch[name], analyses[name]) + for name in sorted(self.renames): + self.plan_clients(name) + self.plan_bridges() + self.plan_stubs() + self.plan_comments() + self.plan_imports() + return self + + 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"]) + if not decl["range"]: + return None + src = self.source(path) + r = decl["range"] + start, end = src.at_range(r[0], r[1]), src.at_range(r[2], r[3]) + sel_start, sel_end = src.at_range(r[4], r[5]), src.at_range(r[6], r[7]) + dt = parse_decl(src.mask, start, sel_start, sel_end, end) + refs = [x for x in self.refs(module) if start <= x.start < end] + split = dt.assign if dt.assign >= 0 else end + a = {"module": module, "path": path, "src": src, "dt": dt, "start": start, "end": end, + "sig_refs": [x for x in refs if x.start < split], + "proof_refs": [x for x in refs if x.start >= split], "defer": []} + if entry.target != entry.name and renamed_token( + src.text[sel_start:sel_end], entry.name, entry.target) is None: + a["defer"].append("name written inside a tidy namespace") + for x in a["sig_refs"]: + if self.ref_kind(x.name) in ("bridge", "tidy"): + a["defer"].append(f"statement names tidy `{x.name}`") + written = sum(1 for x in a["sig_refs"] if x.name in BY_TIDY) + if not written or self.hidden_tidy(entry.name, src, dt, a["sig_refs"]): + a["defer"].append("tidy predicate from a `variable` command or notation") + return a + + def plan_bridges(self) -> None: + """Let the tidy `fun_prop` calls of the declarations in `force_bridge` use the restated + (plain) certificates: `attribute [local fun_prop] ComputableInPolyTime.tidy in`.""" + notions = {n for name in self.renames for n in self.notions_of(name)} + for module, name in sorted(self.force_bridge): + ranges = self.model.lib.ileans.get(module, {}).get("decls", {}) + path = qr.source_path(module) + src = self.source(path) + if name.startswith("line:"): + start = src.starts[command_start_line(src, int(name[5:]))] + elif name in ranges: + start = src.at(ranges[name][0], ranges[name][1]) + else: + continue + if name in self.batch: + own = set(self.notions_of(name)) + else: + own = notions + lines = "".join( + f"attribute [local fun_prop] " + f"{written_name(n.to_tidy, src.scopes.prefixes(start), self.known)} in\n" + for n in sorted(own, key=lambda n: n.tidy)) + self.files[path].replaces.append(Replace(start, start, lines)) + for n in own: + self.need(module, n.to_tidy, False) + self.bridged.append(name) + + def plan_stubs(self) -> None: + """Measurement only (`--stub-failures`): replace the proofs of `stub` by `sorry`, so that + a build reaches the modules downstream of them.""" + for module, name in sorted(self.stub): + ranges = self.model.lib.ileans.get(module, {}).get("decls", {}) + if name not in ranges: + continue + path = qr.source_path(module) + src, r = self.source(path), ranges[name] + start, end = src.at(r[0], r[1]), src.at(r[2], r[3]) + assign = find_top_level(src.mask, src.at(r[6], r[7]), end, ":=") + if assign < 0: + continue + fe = self.files[path] + fe.regions = [g for g in fe.regions if not (g.start >= start and g.end <= end)] + fe.regions.append(Region(assign + 2, end, lambda _: " by\n sorry", name)) + self.stubbed.append(name) + + 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"]) + 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, + "mode": "deferred", "blocking": [], + "issues": self.deferred[name]} + for reason in self.deferred[name]: + self.note(path, a["start"] if a else 0, name, "deferred", reason) + + def plan_decl(self, entry: Entry, a: dict) -> None: + module, path, src, dt = a["module"], a["path"], a["src"], a["dt"] + start, end, sig_refs, proof_refs = a["start"], a["end"], a["sig_refs"], a["proof_refs"] + fe = self.files[path] + info = {"name": entry.name, "target": entry.target, "path": str(path.relative_to(ROOT)), + "line": src.line_of(start), "mode": "manual", "blocking": [], "issues": []} + self.decls[entry.name] = info + self.spans[module].append((start, end, entry.name)) + + def issue(kind: str, detail: str = "", offset: int = start) -> None: + info["issues"].append(kind) + self.note(path, offset, entry.name, kind, detail) + + if entry.target != entry.name: + token = src.text[dt.sel_start:dt.sel_end] + fe.replaces.append(Replace(dt.sel_start, dt.sel_end, + renamed_token(token, entry.name, entry.target))) + for x in sig_refs: + if self.ref_kind(x.name) in ("pred", "renamed", "twin"): + new = self.rename_at(src, x.start, x.end, x.name, self.new_name(x.name)) + if new is None: + issue("statement reference in dot notation", x.name, x.start) + continue + fe.replaces.append(Replace(x.start, x.end, new)) + self.need(module, self.new_name(x.name), True) + doc = src.text[start:dt.sel_start] + if TIDY_WORD.search(doc.split("-/")[0] if "/--" in doc else ""): + issue("docstring mentions tidiness (review wording)") + info["blocking"] = sorted({x.name for x in proof_refs + if self.ref_kind(x.name) in ("bridge", "tidy") + and x.name != entry.name}) + wrap, problems = self.wrap_plan(entry, src, dt, sig_refs) + if not info["blocking"] and entry.name not in self.force_wrap and dt.assign >= 0: + info["mode"] = "translate" + elif wrap is not None: + info["mode"] = "wrap" + else: + for problem in problems: + issue("cannot wrap the proof", problem) + if not info["blocking"] and dt.assign >= 0: + info["mode"] = "translate" + return + for x in proof_refs: + kind = self.ref_kind(x.name) + if info["mode"] == "translate" and kind in ("pred", "renamed", "twin"): + new = self.rename_at(src, x.start, x.end, x.name, self.new_name(x.name)) + if new is None: + issue("proof reference in dot notation to a renamed twin", x.name, x.start) + elif new != src.text[x.start:x.end]: + fe.replaces.append(Replace(x.start, x.end, new)) + if kind == "twin": + self.need(module, self.new_name(x.name), False) + elif info["mode"] == "wrap" and kind == "renamed" and x.name != entry.name: + if x.name in self.renames: + self.convert(path, module, x.start, x.end, x.name, entry.name, "tidy") + else: + issue("generated constant of a restated declaration", x.name, x.start) + if info["mode"] == "wrap": + fe.regions.append(Region(dt.assign + 2, end, wrap, entry.name)) + for notion in self.notions_of(entry.name): + self.need(module, notion.of_tidy, False) + self.need(module, notion.iff, False) + + def hidden_tidy(self, name: str, src: SourceFile, dt: DeclText, sig_refs: list[Ref]) -> bool: + """Whether the statement has more tidy binders or conclusions than are written.""" + sg = self.model.constants.get(name, {}).get("sg") + if not sg: + return False + lean = sum(1 for _, flag in sg[0] if flag) + (sg[1] != 0) + written = 0 + for b in dt.binders: + if any(b.type_start <= x.start < b.type_end and x.name in BY_TIDY for x in sig_refs): + written += max(1, len(b.names)) + if dt.colon >= 0: + written += sum(1 for x in sig_refs if x.start > dt.colon and x.name in BY_TIDY) + return lean > written + + def wrap_plan(self, entry: Entry, src: SourceFile, dt: DeclText, sig_refs: list[Ref]): + """The proof transformation of a wrapped declaration, or None and the problems.""" + problems = [p for p in dt.problems] + preds = [x for x in sig_refs if x.name in BY_TIDY] + hyps = [] + for b in dt.binders: + inside = [x for x in preds if b.type_start <= x.start < b.type_end] + if not inside: + continue + if b.bracket == "[" or not b.names or "_" in b.names: + problems.append("unnamed or instance tidy hypothesis") + if b.default: + problems.append("tidy hypothesis with a default value") + if src.mask[b.type_start:b.type_end] != src.text[b.type_start:b.type_end]: + problems.append("comment inside a tidy hypothesis") + head = is_atomic_application(src.mask, b.type_start, b.type_end) + simple = head is not None and any(x.start == head[0] for x in inside) + hyps.append(Hyp(b.names, collapse(src.text[b.type_start:b.type_end]), simple)) + conclusion, simple = None, False + if dt.colon >= 0 and dt.assign >= 0: + inside = [x for x in preds if x.start > dt.colon] + if inside: + conclusion = collapse(src.text[dt.colon + 1:dt.assign]) + head = is_atomic_application(src.mask, dt.colon + 1, dt.assign) + simple = head is not None and any(x.start == head[0] for x in inside) + if src.mask[dt.colon + 1:dt.assign] != src.text[dt.colon + 1:dt.assign]: + problems.append("comment inside the statement") + if dt.assign >= 0 and re.search(r"(?m)^\s*(?:termination_by|decreasing_by|where)\b", + src.mask[dt.assign:dt.end]): + problems.append("termination or `where` clauses") + if self.hidden_tidy(entry.name, src, dt, sig_refs): + problems.append("tidy hypothesis from a `variable` command or notation") + if problems: + return None, problems + prefixes = src.scopes.prefixes(dt.start) + iffs = ", ".join(written_name(n.iff, prefixes, self.known) + for n in self.notions_of(entry.name)) + body_column = column(src.text, dt.assign + 2) + indent = line_indent(src.text, dt.sel_start) + args = (body_column, indent, hyps, conclusion, simple, iffs) + if wrap_proof(src.text[dt.assign + 2:dt.end], *args) is None: + return None, ["proof layout"] + return (lambda body: wrap_proof(body, *args)), [] + + # Clients. + + def in_batch_decl(self, module: str, offset: int) -> str | None: + for start, end, name in self.spans.get(module, ()): + if start <= offset < end: + return name + return None + + def plan_clients(self, name: str) -> None: + for module, u in self.model.users(name): + path = qr.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): + continue + context = "name" if src.command_keyword(start) in NAME_ONLY_COMMANDS else "tidy" + self.convert(path, module, start, end, name, u[4] if len(u) == 5 else None, context) + + def convert(self, path: Path, module: str, start: int, end: int, old: str, + decl: str | None, context: str) -> None: + """Rename a reference to a restated declaration; in a proof that stays tidy, keep the + site's old type with `.tidy` around the application and `.of_tidy` around tidy + arguments.""" + src, fe = self.source(path), self.files[path] + new = self.renames[old] + token = src.text[start:end] + written = self.rename_at(src, start, end, old, new) + self.sites[context] += 1 + if written is None: + self.note(path, start, decl, "reference in dot notation", f"`{token}`") + return + if written != token: + fe.replaces.append(Replace(start, end, written)) + if context != "tidy": + return + problem = self.convert_site(src, fe, start, end, old) + if problem: + self.note(path, start, decl, "reference kept tidy", f"`{token}`: {problem}") + else: + for notion in self.notions_of(old): + self.need(module, notion.of_tidy, False) + + def convert_site(self, src: SourceFile, fe: FileEdits, start: int, end: int, + old: str) -> str | None: + sg = self.model.constants.get(old, {}).get("sg") + if not sg: + return None + binders, conclusion = sg + mask = src.mask + opener = enclosing_opener(mask, start) + if opener >= 0 and mask[opener] == "[" and LEMMA_LIST_TACTIC.search( + mask[mask.rfind("\n", 0, opener) + 1:opener]): + return "used in a tactic lemma list" + explicit_all = src.text[start:end].startswith("@") or (start and mask[start - 1] == "@") + site_start = start - 1 if start and mask[start - 1] == "@" else start + positions = [i for i, (bi, _) in enumerate(binders) if explicit_all or bi == 0] + if not explicit_all and any(flag and bi != 0 for bi, flag in binders): + return "implicit tidy hypothesis" + if start and mask[start - 1] == ".": + before = mask[start - 2] if start >= 2 else " " + if before.isspace() or before in OPENERS or before in "<|$,": + return "leading-dot notation" + site_start = receiver_start(mask, start - 1) + if not positions or binders[positions[0]][1]: + return "dot notation on a tidy receiver" + positions = positions[1:] + named: list[tuple[int, int]] = [] + args = parse_args(mask, end, len(mask), len(positions), line_indent(mask, start), named) + if len(args) < len(positions): + return f"partial application ({len(args)} of {len(positions)} explicit arguments)" + for (a, b), i in zip(args, positions): + if binders[i][1] == 2: + return "tidy hypothesis under binders" + if binders[i][1] == 1: + fe.wraps.append(Wrap(a, b, "(.of_tidy ", ")", start)) + site_end = max([end] + [b for _, b in args + named]) + if conclusion == 2: + return "conclusion is not a bare tidy predicate" + if conclusion == 1: + left = site_start - 1 + while left >= 0 and mask[left] in " \t\n": + left -= 1 + right = site_end + while right < len(mask) and mask[right] in " \t\n": + right += 1 + if left >= 0 and mask[left] == "(" and match_bracket(mask, left) == right: + fe.wraps.append(Wrap(left, right + 1, "", ".tidy", site_start)) + elif not args and site_start == start and IDENT.fullmatch(src.text[start:end]): + fe.wraps.append(Wrap(start, end, "", ".tidy", site_start)) + else: + fe.wraps.append(Wrap(site_start, site_end, "(", ").tidy", site_start)) + return None + + # Documentation. + + def plan_comments(self) -> None: + renamed = {old: new for old, new in self.renames.items() if old != new} + if not renamed: + return + by_last: dict[str, list[str]] = defaultdict(list) + for old in renamed: + by_last[old.rsplit(".", 1)[-1]].append(old) + full = re.compile(r"(? str | None: + """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 len(candidates) <= 1: + return candidates[0] if candidates else None + if src.path.suffix != ".lean": + return None + for prefix in src.scopes.prefixes(offset): + full = prefix + "." + token if prefix else token + if full in candidates: + return full + return None + + # Imports. + + def plan_imports(self) -> None: + ileans = self.model.lib.ileans + reexports: dict[str, set[str]] = {} + + def closure(module: str) -> set[str]: + if module not in reexports: + reexports[module] = {module} + for dep, private, *_ in ileans.get(module, {}).get("directImports", []): + if not private: + reexports[module] |= closure(dep) + return reexports[module] + + def imports_of(module: str) -> set[str]: + seen, stack = set(), [module] + while stack: + for dep, *_ in ileans.get(stack.pop(), {}).get("directImports", []): + if dep not in seen: + seen.add(dep) + stack.append(dep) + return seen + + for module, needed in sorted(self.needs.items()): + 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) + 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()): + if dep in (public if want_public and is_module else available): + continue + if module in imports_of(dep): + self.note(path, 0, None, "import cycle", f"needs `{dep}`") + continue + self.imports.append((module, dep, want_public and is_module)) + header = list(re.finditer(r"(?m)^(public\s+)?(?:meta\s+)?import\s+\S+[^\n]*\n", + src.mask)) + kind = [h for h in header if bool(h[1]) == (want_public and is_module)] + at = (kind or header)[-1].end() if header else 0 + if want_public and is_module and not kind and header: + at = header[0].start() + prefix = "public import " if want_public and is_module else "import " + self.files[path].replaces.append(Replace(at, at, prefix + dep + "\n")) + + # Output. + + def render(self) -> dict[Path, str]: + out = {} + for path, fe in self.files.items(): + if not (fe.replaces or fe.wraps or fe.regions): + continue + src = self.source(path) + text = apply_edits(src.text, fe.replaces, fe.wraps, fe.regions) + text, removed = cancel_round_trips(text) if path.suffix == ".lean" else (text, 0) + self.round_trips += removed + if text != src.text: + out[path] = text + return out + + def summary(self) -> dict: + modes = Counter(d["mode"] for d in self.decls.values()) + kinds = Counter(m.kind for m in self.manual) + return {"area": self.area, "declarations": len(self.batch), "modes": dict(modes), + "manual": dict(kinds.most_common()), "sites": dict(self.sites), + "imports": [list(i) for i in self.imports], "bridged": sorted(self.bridged), + "stubbed": sorted(self.stubbed)} + + +def command_start_line(src: SourceFile, line: int) -> int: + """The first line of the docstring and attributes above the 0-based `line`.""" + while line > 0: + above, above_mask = src.lines[line - 1], src.mask.split("\n")[line - 1] + if above.strip() and (not above_mask.strip() or above_mask.lstrip().startswith("@[")): + line -= 1 + else: + break + return line + + +def enclosing_opener(mask: str, pos: int) -> int: + """The unmatched opening bracket before `pos`, or -1.""" + depth = 0 + for j in range(pos - 1, -1, -1): + char = mask[j] + if char in CLOSERS: + depth += 1 + elif char in OPENERS: + if depth == 0: + return j + depth -= 1 + return -1 + + +def receiver_start(mask: str, dot: int) -> int: + """The start of the atom ending just before the `.` at `dot`.""" + j = dot - 1 + if j >= 0 and mask[j] in CLOSERS: + depth = 0 + while j >= 0: + if mask[j] in CLOSERS: + depth += 1 + elif mask[j] in OPENERS: + depth -= 1 + if depth == 0: + return j + j -= 1 + return 0 + while j >= 0 and (mask[j].isalnum() or mask[j] in "_'.!?₀₁₂₃₄₅₆₇₈₉" or ord(mask[j]) > 127 + and mask[j] not in OPENERS + CLOSERS and not mask[j].isspace()): + j -= 1 + return j + 1 + + +def plan_markdown(plan: dict, limit: int = 40) -> str: + s = plan["summary"] + out = [f"### Rewrite plan for {s['area']}", "", + f"{s['declarations']} case 2 declarations: " + ", ".join( + f"{n} {m}" for m, n in sorted(s["modes"].items())) + ". References converted: " + + ", ".join(f"{n} in {c} contexts" for c, n in sorted(s["sites"].items())) + "."] + if s["imports"]: + out.append(f"Imports added: {len(s['imports'])}.") + if plan.get("round_trips"): + out.append(f"Round trips removed: {plan['round_trips']}.") + if s["manual"]: + out += ["", "Manual work, by kind: " + "; ".join(f"{k} ({n})" + for k, n in s["manual"].items()) + ".", + "", "| File | Line | Declaration | Kind | Detail |", "|---|--:|---|---|---|"] + for m in plan["manual"][:limit]: + out.append(f"| `{m['path']}` | {m['line']} | `{m['decl']}` | {m['kind']} | " + f"{m['detail']} |") + if len(plan["manual"]) > limit: + out.append(f"| … {len(plan['manual']) - limit} more in the JSON report | | | | |") + if plan.get("build"): + b = plan["build"] + out += ["", f"Build: {b['status']}. Declarations failing: {len(b['failing'])}."] + return "\n".join(out) + + +# --- Rewriting and verification ----------------------------------------------------------------- + +DIAGNOSTIC = re.compile(r"^(?Perror|warning): (?:\./)*(?P[^\s:]+\.lean):" + r"(?P\d+):(?P\d+): (?P.*)$", re.M) +DECL_HEADER = re.compile(r"\b(?:theorem|lemma|def|abbrev|instance|example|structure|class|" + r"inductive|opaque)\b\s*([^\s(:{\[⦃]*)") + + +# Messages that report a consequence (axiom audits, `#guard_msgs` checks) rather than a proof +# the loop can repair. +CONSEQUENCE = re.compile(r"#guard_msgs|abstract audit|axiom audit|depends on disallowed axiom|" + r"declaration uses `sorry`") + + +def module_of(path: Path) -> str: + rel = path.relative_to(ROOT).with_suffix("") + parts = rel.parts[1:] if rel.parts[0] == "abstracts" else rel.parts + return ".".join(parts) + + +def diagnostics(output: str) -> list[dict]: + return [{"level": m["level"], "path": m["path"], "line": int(m["line"]), + "message": m["msg"]} for m in DIAGNOSTIC.finditer(output)] + + +def declaration_at(text: str, line: int) -> str: + """The name in the header of the command containing a 1-based line; a line in the docstring + 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)) + 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] + for start in reversed(starts): + header = DECL_HEADER.search(mask, start, max(offset + 1, start + 400)) + if header: + return header[1] or "(anonymous)" + return "" + + +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] + return text.count("\n", 0, starts[-1]) + 1 if starts else line + + +def lake_build(targets: list[str]) -> tuple[int, str]: + proc = subprocess.run(["lake", "build", *targets], cwd=ROOT, text=True, + capture_output=True) + return proc.returncode, proc.stdout + proc.stderr + + +def rewrite(model: Model, entries: list[Entry], registry: dict[str, str], area: str, + verify: bool, rounds: int, stub_failures: bool = False + ) -> tuple[Planner, dict | None]: + """Write the area's rewrite. With `verify`, build the three libraries and retry, up to + `rounds` times: a translated proof that fails is wrapped, and a wrapped proof or a client + declaration that fails gets a local plain → tidy `fun_prop` transition. With + `stub_failures` (measurement only), proofs that still fail become `sorry`, so that the next + round reaches the modules downstream of them.""" + originals: dict[Path, str] = {} + force: set[str] = set() + bridge: set[tuple[str, str]] = set() + stub: set[tuple[str, str]] = set() + build, history = None, [] + for round_ in range(1, rounds + 1): + for path, text in originals.items(): # plan against the sources of the build + path.write_text(text, encoding="utf-8") + planner = Planner(model, entries, registry, area, frozenset(force), + frozenset(bridge), frozenset(stub)).plan() + texts = planner.render() + for path, text in texts.items(): + originals.setdefault(path, planner.source(path).text) + path.write_text(text, encoding="utf-8") + if not verify: + return planner, None + targets = list(qr.ROOTS) + code, output = lake_build(targets) + build = check_build(planner, texts, output, code, round_, targets) + history.append({k: build[k] for k in ("round", "status", "failing", "forced_wrap", + "failing_clients")}) + retry = {d for d in build["failing"] if planner.decls.get(d, {}).get("mode") + == "translate"} + wrapped = {(planner.model.decls[d]["module"], d) for d in build["failing"] + if planner.decls.get(d, {}).get("mode") == "wrap"} + clients = {tuple(c) for c in build["failing_clients"]} + new_bridges = (wrapped | clients) - bridge + new_stubs = {x for x in (wrapped | clients) & bridge if not x[1].startswith("line:") + } - stub if stub_failures else set() + if not (retry or new_bridges or new_stubs) or round_ == rounds: + break + force |= retry + bridge |= new_bridges + stub |= new_stubs + if build is not None: + build["history"] = history + return planner, build + + +def check_build(planner: Planner, texts: dict[Path, str], output: str, code: int, round_: int, + targets: list[str]) -> dict: + by_written = {} + for name, info in planner.decls.items(): + by_written[(info["path"], name.rsplit(".", 1)[-1])] = name + by_written[(info["path"], info["target"].rsplit(".", 1)[-1])] = name + failing, clients, failing_clients, problems = set(), [], set(), [] + for d in diagnostics(output): + path = ROOT / d["path"] + text = texts.get(path) or (path.read_text() if path.exists() else "") + header = declaration_at(text, d["line"]) if text else "" + decl = by_written.get((d["path"], header.rsplit(".", 1)[-1])) + item = {**d, "decl": decl or header} + if d["level"] == "error" and CONSEQUENCE.search(d["message"]): + item["consequence"] = True + elif d["level"] == "error" and decl: + failing.add(decl) + planner.decls[decl].setdefault("errors", []).append(d["message"]) + elif d["level"] == "error": + 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 len(names) == 1: + failing_clients.add((module, names[0])) + item["decl"] = names[0] + elif text: + at = command_line(text, d["line"]) - 1 + block = text.split("\n")[at:min(at + 3, d["line"])] + original = planner.source(path).lines if path in texts else text.split("\n") + hits = [i for i in range(len(original)) + if original[i:i + len(block)] == block] + if len(hits) == 1: + failing_clients.add((module, f"line:{hits[0]}")) + clients.append(item) + problems.append(item) + return {"round": round_, "targets": targets, "status": "passed" if code == 0 else "failed", + "failing": sorted(failing), "client_errors": clients, + "failing_clients": sorted(failing_clients), "diagnostics": problems, + "forced_wrap": sorted(planner.force_wrap), + "bridged": sorted(planner.bridged), "stubbed": sorted(planner.stubbed)} + + +def unified_diff(planner: Planner) -> str: + out = [] + for path, text in sorted(planner.render().items()): + rel = str(path.relative_to(ROOT)) + out += difflib.unified_diff(planner.source(path).text.splitlines(True), + text.splitlines(True), "a/" + rel, "b/" + rel) + return "".join(out) + + +def stub_registry(model: Model) -> list[dict]: + """Existing plain twins: for each tidy theorem, the declaration named by its plain rename + whose statement is its plain transport.""" + pairs = [] + for name, const in sorted(model.constants.items()): + if const["k"] != "thm" or not const["e"] or not const.get("tidy"): + continue + if any(t not in BY_TIDY for t in const["tidy"]) or name in BRIDGES: + continue + twin = plain_name(name) + other = model.constants.get(twin) + if twin != name and other and other["e"] and other.get("ph") == const.get("ph") \ + and not other.get("tidy"): + pairs.append({"original": name, "plain": twin, "module": const["m"]}) + return pairs + + +# --- Command line ------------------------------------------------------------------------------- + +def entry_json(e: Entry) -> dict: + return {k: v for k, v in e.__dict__.items()} + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__, + formatter_class=argparse.RawDescriptionHelpFormatter) + parser.add_argument("command", choices=("report", "rewrite", "stub-registry")) + parser.add_argument("--area", action="append", default=[], + help="restrict to an area of #587 (repeatable for report)") + parser.add_argument("--registry", type=Path, default=REGISTRY) + parser.add_argument("--allowlist", type=Path, default=ALLOWLIST) + parser.add_argument("--build-dir", type=Path, default=qr.DEFAULT_BUILD_DIR) + parser.add_argument("--no-build-check", action="store_true") + parser.add_argument("--json", type=Path, help="write the full report as JSON") + parser.add_argument("--markdown", type=Path, help="write the report as Markdown") + parser.add_argument("--no-plan", action="store_true", help="report: skip rewrite plans") + parser.add_argument("--verify", action="store_true", + help="rewrite: build the touched modules and wrap failing translations") + parser.add_argument("--diff", type=Path, + help="rewrite: write a unified diff of the plan instead of the files") + parser.add_argument("--rounds", type=int, default=6) + parser.add_argument("--stub-failures", action="store_true", + help="rewrite --verify, measurement only: replace proofs that still " + "fail by `sorry` to reach downstream modules (never commit the result)") + parser.add_argument("--output", type=Path, default=REGISTRY, + help="stub-registry: where to write the registry") + parser.add_argument("--limit", type=int, default=40, help="rows per Markdown table") + args = parser.parse_args(argv) + for area in args.area: + if area not in AREA_ORDER: + parser.error(f"unknown area {area}; choose from {', '.join(AREA_ORDER)}") + if args.command == "rewrite" and len(args.area) != 1: + parser.error("rewrite needs exactly one --area") + outputs = qr.check_outputs(args.build_dir, args.no_build_check) + model = Model(args.build_dir, load_allowlist(args.allowlist)) + if args.command == "stub-registry": + pairs = stub_registry(model) + args.output.write_text(json.dumps(pairs, indent=1) + "\n") + print(f"wrote {len(pairs)} pairs to {args.output}") + return 0 + registry = load_registry(args.registry) + entries = classify_all(model, registry) + 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()) + report = {"revision": revision, "dirty": dirty, "outputs": outputs, + "allowlist_size": len(model.allowlist), "registry": str(args.registry), + "registry_size": len(registry), + "registry_problems": registry_problems(registry, model.constants), + "summary": summary(shown), "entries": [entry_json(e) for e in shown]} + plans = [] + if args.command == "rewrite" and args.diff: + planner = Planner(model, entries, registry, args.area[0]).plan() + args.diff.write_text(unified_diff(planner)) + plans.append((planner, None)) + elif args.command == "rewrite": + planner, build = rewrite(model, entries, registry, args.area[0], args.verify, + args.rounds, args.stub_failures) + plans.append((planner, build)) + elif not args.no_plan: + for area in args.area or AREA_ORDER: + if any(e.area == area and e.case == "2" for e in entries): + planner = Planner(model, entries, registry, area).plan() + planner.render() + plans.append((planner, None)) + report["plans"] = [{"summary": p.summary(), "round_trips": p.round_trips, + "decls": list(p.decls.values()), + "manual": [m.__dict__ for m in p.manual], "build": b} + for p, b in plans] + text = markdown_report(report, args.limit) + "".join( + "\n" + plan_markdown(p, args.limit) + "\n" for p in report["plans"]) + 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") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) From 8b6b1d403d772e72e782ebd252459dc7a8efe7c0 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 22:21:35 -0400 Subject: [PATCH 02/10] fix(scripts): make the tidy sweep's rewrites and verification safe Addresses review 5635891057 on #666 and follows Samuel's plain-first direction on #456 and #671: - A replacement name is written only if it resolves to its target, and nothing else, from its position (namespaces, opens, same-module private names, local binders), falling back to `_root_.`; no edit is made at a span that does not spell the referenced constant, and `rewrite` refuses `--no-build-check`. Leading-dot spans are recognised. - Call-site conversions are staged and applied only when complete; a declaration with a reference that cannot be converted is deferred, so skipped references stay unchanged. - Verification builds strictly (`--wfail --iofail`), reports `passed` only without errors, and exits nonzero otherwise. The measurement mode that wrote `sorry` into sources and the local plain-to-tidy `fun_prop` fallback are removed; remaining failures are reported as gaps. - Twins are the committed plain declarations named by the plain rename (exact or broader); the checked-in registry is gone. `--registry` reads extra pairs from a migration script and rejects missing files, other keys, empty names, self-pairs and conflicting duplicates. - Plans count the references left on case 1 originals, for their internalization. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- scripts/test_tidy_sweep.py | 317 ++++++++++-- scripts/tidy_mirror_registry.json | 82 ---- scripts/tidy_sweep.py | 781 ++++++++++++++++-------------- 3 files changed, 691 insertions(+), 489 deletions(-) delete mode 100644 scripts/tidy_mirror_registry.json diff --git a/scripts/test_tidy_sweep.py b/scripts/test_tidy_sweep.py index b645b47df9..07b9b6224a 100644 --- a/scripts/test_tidy_sweep.py +++ b/scripts/test_tidy_sweep.py @@ -2,11 +2,14 @@ from __future__ import annotations +import contextlib +import io import json import pathlib import sys import tempfile import unittest +from types import SimpleNamespace sys.path.insert(0, str(pathlib.Path(__file__).resolve().parent)) import tidy_sweep as t # noqa: E402 @@ -83,8 +86,8 @@ def test_scopes_track_namespaces_and_opens(self) -> None: class ClassificationTests(unittest.TestCase): - def classify(self, d: dict, c: dict, registry=None, constants=None, private=None): - return t.classify_decl(d, c, registry or {}, constants or {d["name"]: c}, private or {}) + def classify(self, d: dict, c: dict, twins=None, constants=None, private=None): + return t.classify_decl(d, c, twins or {}, constants or {d["name"]: c}, private or {}) def test_case_two_renames_and_checks_the_target(self) -> None: e = self.classify(decl("A.computableTidilyInPolyTime_x"), const()) @@ -94,25 +97,31 @@ def test_case_two_renames_and_checks_the_target(self) -> None: def test_collisions(self) -> None: c = const(ph="1") + # A target that still states tidy computability is not a twin. constants = {"A.computableTidilyInPolyTime_x": c, - "A.computableInPolyTime_x": const(tidy=(), ph="2")} + "A.computableInPolyTime_x": const(ph="2")} e = self.classify(decl("A.computableTidilyInPolyTime_x"), c, constants=constants) self.assertEqual((e.case, e.reason), ("unclassifiable", "collision")) - self.assertFalse(e.collision["equivalent"]) - constants["A.computableInPolyTime_x"]["ph"] = "1" - e = self.classify(decl("A.computableTidilyInPolyTime_x"), c, constants=constants) - self.assertTrue(e.collision["equivalent"]) # A private declaration of the same module blocks the name as well. e = self.classify(decl("A.computableTidilyInPolyTime_y"), c, private={"Complexity.M": {"A.computableInPolyTime_y"}}) - self.assertEqual(e.reason, "collision") - - def test_registered_twin_is_case_one(self) -> None: - c = const(ph="5") - constants = {POLY + ".map": c, PLAIN + ".map": const(tidy=(), ph="5")} - e = self.classify(decl(POLY + ".map"), c, {POLY + ".map": PLAIN + ".map"}, constants) - self.assertEqual((e.case, e.target, e.warnings), ("1", PLAIN + ".map", [])) - e = self.classify(decl(POLY + ".map"), c, {POLY + ".map": "Missing.twin"}, constants) + self.assertEqual((e.reason, e.detail), ("collision", "the target is private")) + + def test_committed_plain_twins(self) -> None: + original = const(ph="5") + constants = {POLY + ".map": original, PLAIN + ".map": const(tidy=(), ph="5"), + POLY + ".comp": original, PLAIN + ".comp": const(tidy=(), ph="6"), + POLY + ".fst": original, PLAIN + ".fst": const(ph="5"), + POLY + ".snd": original, PLAIN + ".snd": const(tidy=(), e="")} + twins = t.discover_twins(constants) + self.assertEqual(twins, {POLY + ".map": (PLAIN + ".map", "exact"), + POLY + ".comp": (PLAIN + ".comp", "by name")}) + e = self.classify(decl(POLY + ".comp"), original, twins, constants) + self.assertEqual((e.case, e.target, e.twin), ("1", PLAIN + ".comp", "by name")) + self.assertEqual(len(e.warnings), 1) + twins = t.twin_map(constants, {POLY + ".fst": "Missing.twin"}) + self.assertEqual(twins[POLY + ".fst"], ("Missing.twin", "registry")) + e = self.classify(decl(POLY + ".fst"), original, twins, constants) self.assertEqual(e.reason, "registered twin missing") def test_unclassifiable_reasons(self) -> None: @@ -134,18 +143,6 @@ def test_definitions_and_fields_are_case_three(self) -> None: e = self.classify(decl("A.S.polyTime", role="member"), const()) self.assertEqual((e.case, e.kind), ("3", "structure field")) - def test_registry_formats(self) -> None: - with tempfile.TemporaryDirectory() as tmp: - path = pathlib.Path(tmp) / "r.json" - path.write_text(json.dumps([{"original": "a", "plain": "b", "module": "M"}])) - self.assertEqual(t.load_registry(path), {"a": "b"}) - path.write_text(json.dumps({"pairs": [{"original": "c", "plain": "d"}]})) - self.assertEqual(t.load_registry(path), {"c": "d"}) - path.write_text(json.dumps([{"original": "c"}])) - with self.assertRaises(ValueError): - t.load_registry(path) - self.assertEqual(t.load_registry(pathlib.Path(tmp) / "missing.json"), {}) - def test_allowlist_ignores_comments(self) -> None: with tempfile.TemporaryDirectory() as tmp: path = pathlib.Path(tmp) / "a.txt" @@ -153,6 +150,49 @@ def test_allowlist_ignores_comments(self) -> None: self.assertEqual(t.load_allowlist(path), {"A/B.lean", "C.lean"}) +class RegistryTests(unittest.TestCase): + """Review 5635891057: malformed or ambiguous registry input is an error.""" + + def load(self, data) -> dict: + with tempfile.TemporaryDirectory() as tmp: + path = pathlib.Path(tmp) / "r.json" + path.write_text(data if isinstance(data, str) else json.dumps(data)) + return t.load_registry(path) + + def test_valid_shapes(self) -> None: + self.assertEqual(self.load([{"original": "a", "plain": "b", "module": "M"}]), {"a": "b"}) + self.assertEqual(self.load({"pairs": [{"original": "c", "plain": "d"}]}), {"c": "d"}) + # Repeating a pair is harmless. + self.assertEqual(self.load([{"original": "a", "plain": "b"}] * 2), {"a": "b"}) + self.assertEqual(t.load_registry(None), {}) + + def test_malformed_input_is_rejected(self) -> None: + cases = { + "misspelled key": {"pair": [{"original": "a", "plain": "b"}]}, + "extra key": {"pairs": [], "version": 1}, + "not an array": {"pairs": {"a": "b"}}, + "scalar": "3", + "not JSON": "[{", + "missing plain": [{"original": "a"}], + "unknown entry key": [{"original": "a", "plain": "b", "kind": "x"}], + "empty name": [{"original": "", "plain": "b"}], + "blank name": [{"original": "a", "plain": " b"}], + "non-string": [{"original": "a", "plain": 3}], + "entry not an object": [["a", "b"]], + "own twin": [{"original": "a", "plain": "a"}], + "conflicting twins": [{"original": "o", "plain": "p"}, + {"original": "o", "plain": "q"}], + } + for label, data in cases.items(): + with self.assertRaises(ValueError, msg=label): + self.load(data) + + def test_a_requested_file_must_exist(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + with self.assertRaisesRegex(ValueError, "not found"): + t.load_registry(pathlib.Path(tmp) / "missing.json") + + class ParsingTests(unittest.TestCase): def test_brackets_and_top_level_tokens(self) -> None: text = "(a : b := c) : T := x" @@ -260,41 +300,215 @@ def test_reindent(self) -> None: self.assertIsNone(t.reindent([" a"], -2)) +def fake_source(text: str, namespaces: set[str]) -> t.SourceFile: + src = object.__new__(t.SourceFile) + src.path = t.ROOT / "Fake.lean" + 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._namespaces, src._scopes = namespaces, None + return src + + +def fake_planner(text: str, constants: dict, known=(), privates=None, refs=()): + """A planner over one source `Fake.lean` (module `M`) without a build.""" + p = object.__new__(t.Planner) + p.model = SimpleNamespace(constants=constants, owners={}, + lib=SimpleNamespace(ileans={})) + p.known = set(known) | set(constants) + p.privates = privates or {} + p.twins, p.force_wrap = {}, frozenset() + p.namespaces = t.namespaces_of(p.known) + src = fake_source(text, p.namespaces) + p.sources = {src.path: src} + p._refs = {"M": [t.Ref(n, a, b, None) for n, a, b in refs]} + p._locals = {} + p.deferred = {} + p.batch = {} + p.reset() + return p, src + + class ConvertTests(unittest.TestCase): - def planner(self, sg) -> t.Planner: - p = object.__new__(t.Planner) - p.model = type("M", (), {"constants": {"X": {"sg": sg}}})() - return p - - def convert(self, text: str, sg, at: str = "X") -> tuple[str, str | None]: - src = object.__new__(t.SourceFile) - src.text, src.mask = text, masks(text)[1] - fe = t.FileEdits() + def convert(self, text: str, sg, at: str = "X") -> tuple[str, str]: + p, src = fake_planner(text, {"X": {"m": "M", "sg": sg, "tidy": [POLY]}}, + known={"Y"}) + p.renames = {"X": "Y"} start = text.index(at) - problem = self.planner(sg).convert_site(src, fe, start, start + len(at), "X") - return t.render(text, fe.replaces, fe.wraps, 0, len(text)), problem + p.convert(src.path, "M", start, start + len(at), "X", None, "tidy") + fe = p.files[src.path] + blocked = "; ".join(p.blockers.get("X", [])) + return t.render(text, fe.replaces, fe.wraps, 0, len(text)), blocked def test_application_keeps_its_old_type(self) -> None: sg = [[[1, 0], [0, 0], [0, 1]], 1] # {V} (enc) (hc : tidy) : tidy self.assertEqual(self.convert(" exact X enc hc", sg), - (" exact (X enc (.of_tidy hc)).tidy", None)) + (" exact (Y enc (.of_tidy hc)).tidy", "")) self.assertEqual(self.convert(" exact (X enc hc).comp g", sg)[0], - " exact (X enc (.of_tidy hc)).tidy.comp g") + " exact (Y enc (.of_tidy hc)).tidy.comp g") self.assertEqual(self.convert(" X (V := ℕ) enc hc", sg)[0], - " (X (V := ℕ) enc (.of_tidy hc)).tidy") + " (Y (V := ℕ) enc (.of_tidy hc)).tidy") def test_constants_and_dot_chains(self) -> None: self.assertEqual(self.convert(" exact X.comp h", [[[1, 0]], 1])[0], - " exact X.tidy.comp h") - - def test_unconvertible_sites(self) -> None: - sg = [[[0, 0]], 1] - self.assertIn("partial", self.convert(" map X", sg)[1]) - self.assertIn("lemma list", self.convert(" simp [X]", sg)[1]) - self.assertIn("leading-dot", self.convert(" exact .X a", sg, "X")[1]) - self.assertIn("binders", self.convert(" X a", [[[0, 2]], 1])[1]) - self.assertIn("implicit", self.convert(" X a", [[[1, 1], [0, 0]], 1])[1]) - self.assertIn("bare", self.convert(" X a", [[[0, 0]], 2])[1]) + " exact Y.tidy.comp h") + + def test_leading_dot_with_a_plain_conclusion(self) -> None: + # `.of_foo h : DecidableInExpTime …`: the expected type does not change, so only the + # tidy argument is converted. The `.ilean` span includes the leading dot. + p, src = fake_planner(" exact .of_foo hc", {"N.of_foo": {"m": "M", + "sg": [[[0, 1]], 0], "tidy": [POLY]}}, known={"N.of_bar"}) + p.renames = {"N.of_foo": "N.of_bar"} + start = src.text.index(".of_foo") + self.assertTrue(p.convert(src.path, "M", start, start + 7, "N.of_foo", None, "tidy")) + fe = p.files[src.path] + self.assertEqual(t.render(src.text, fe.replaces, fe.wraps, 0, len(src.text)), + " exact .of_bar (.of_tidy hc)") + self.assertTrue(t.spells(".of_foo", "N.of_foo")) + + def test_unconvertible_sites_stay_unchanged(self) -> None: + """Review 5635891057: a skipped call keeps its text (no rename, no partial wraps) and + blocks the referenced declaration, which is then deferred.""" + cases = [(" map X", [[[0, 0]], 1], "partial"), + (" simp [X]", [[[0, 0]], 1], "lemma list"), + (" exact .X a", [[[0, 0]], 1], "dot notation"), + (" X a", [[[0, 2]], 1], "binders"), + (" X a", [[[1, 1], [0, 0]], 1], "implicit"), + # The argument is tidy, but the conclusion is not a bare predicate. + (" X hc", [[[0, 1]], 2], "bare"), + # The first argument converts, the second cannot. + (" X hc hd", [[[0, 1], [0, 2]], 1], "binders")] + for text, sg, reason in cases: + out, blocked = self.convert(text, sg) + self.assertEqual(out, text, text) + self.assertIn(reason, blocked, text) + + +class ResolutionTests(unittest.TestCase): + """Review 5635891057: a replacement must denote its target from where it is written, and a + stale span is never edited.""" + + TEXT = ("namespace A\n\nopen Turing.MultiTapeTM\n\n" + "theorem t (f : ℕ → ℕ) : ComputableTidilyInPolyTime f e e := sorry\n\nend A\n") + + def written(self, text: str, token: str, old: str, new: str, known=(), privates=None, + refs=()): + p, src = fake_planner(text, {old: {"m": "M"}, new: {"m": "M"}}, known, privates, refs) + start = text.index(token) + return p.written("M", src, start, start + len(token), old, new) + + def test_a_shadowing_declaration_forces_a_longer_name(self) -> None: + # `A.ComputableInPolyTime` would capture a bare `ComputableInPolyTime` inside `A`. + written, _ = self.written(self.TEXT, "ComputableTidilyInPolyTime", POLY, PLAIN, + known={"A.ComputableInPolyTime"}) + self.assertEqual(written, PLAIN) + written, _ = self.written(self.TEXT, "ComputableTidilyInPolyTime", POLY, PLAIN) + self.assertEqual(written, "ComputableInPolyTime") + + def test_private_names_of_the_module_shadow_too(self) -> None: + written, _ = self.written(self.TEXT, "ComputableTidilyInPolyTime", POLY, PLAIN, + privates={"M": {"A.ComputableInPolyTime"}}) + self.assertEqual(written, PLAIN) + + def test_local_binders_shadow_short_names(self) -> None: + text = ("namespace B\n\ntheorem t (map : ℕ) : True := by\n exact Old.map\n\nend B\n") + start = text.index("Old.map") + refs = [("Old.map", start, start + len("Old.map"))] + written, _ = self.written(text, "Old.map", "Old.map", "B.map", refs=refs) + self.assertEqual(written, "B.map") # `map` alone is the binder + + def test_root_prefix_when_every_suffix_is_ambiguous(self) -> None: + known = {"A.Turing.MultiTapeTM.ComputableInPolyTime", "A.ComputableInPolyTime", + "A.MultiTapeTM.ComputableInPolyTime"} + written, _ = self.written(self.TEXT, "ComputableTidilyInPolyTime", POLY, PLAIN, known) + self.assertEqual(written, "_root_." + PLAIN) + + def test_stale_spans_are_not_edited(self) -> None: + text = "theorem t : True := completelyUnrelated\n" + written, why = self.written(text, "completelyUnrelated", POLY, PLAIN) + self.assertIsNone(written) + self.assertIn("does not spell", why) + self.assertTrue(t.spells("ComputableTidilyInPolyTime", POLY)) + self.assertTrue(t.spells("@MultiTapeTM.ComputableTidilyInPolyTime", POLY)) + self.assertFalse(t.spells("TidilyInPolyTime", POLY)) + self.assertFalse(t.spells("", POLY)) + + +class VerificationTests(unittest.TestCase): + """Review 5635891057: verification is strict, reports failures and exits nonzero.""" + + def test_builds_are_strict(self) -> None: + calls = [] + + def runner(cmd, **_): + calls.append(cmd) + return SimpleNamespace(returncode=1, stdout="", stderr="") + self.assertEqual(t.lake_build(["Complexity"], runner)[0], 1) + self.assertEqual(calls, [["lake", "build", "--wfail", "--iofail", "Complexity"]]) + + def check(self, output: str, code: int) -> dict: + planner = SimpleNamespace(decls={}, force_wrap=frozenset()) + return t.check_build(planner, {}, output, code, 1) + + def test_status_is_passed_only_without_errors(self) -> None: + self.assertEqual(self.check("", 0)["status"], "passed") + self.assertEqual(self.check("", 1)["status"], "failed") + error = "error: Complexity/Nope.lean:3:0: unknown identifier 'x'\n" + self.assertEqual(self.check(error, 0)["status"], "failed") + sorry = "warning: Complexity/Nope.lean:3:8: declaration uses `sorry`\n" + self.assertEqual(self.check(sorry, 1)["status"], "failed") + + def test_rewrite_writes_reports_and_fails_honestly(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + path = pathlib.Path(tmp) / "M.lean" + path.write_text("old\n") + + class FakePlanner: + def __init__(self, *args): + self.decls, self.force_wrap = {}, frozenset() + + def plan(self): + return self + + def render(self): + return {path: "new\n"} + + def source(self, _): + return SimpleNamespace(text="old\n") + + def build(_): + return 1, "warning: Complexity/M.lean:1:8: declaration uses `sorry`\n" + original = t.Planner + t.Planner = FakePlanner + try: + _, result = t.rewrite(None, [], {}, "Logics", True, 3, build) + finally: + t.Planner = original + self.assertEqual(path.read_text(), "new\n") + self.assertEqual(result["status"], "failed") + self.assertEqual(len(result["history"]), 1) + plans = [{"build": result}] + self.assertEqual(t.exit_status(plans), 1) + self.assertIn("FAILED", t.plan_markdown({"summary": { + "area": "Logics", "declarations": 0, "modes": {}, "sites": {}, "imports": [], + "manual": {}}, "manual": [], "build": result})) + self.assertEqual(t.exit_status([{"build": None}]), 0) + + def test_measurement_stubs_and_unchecked_rewrites_are_refused(self) -> None: + with tempfile.TemporaryDirectory() as tmp, \ + contextlib.redirect_stderr(io.StringIO()) as err: + for argv in (["rewrite", "--area", "Logics", "--stub-failures"], + ["rewrite", "--area", "Logics", "--no-build-check"], + ["report", "--registry", str(pathlib.Path(tmp) / "missing.json")]): + with self.assertRaises(SystemExit, msg=argv) as raised: + t.main(argv) + self.assertEqual(raised.exception.code, 2) + self.assertIn("--no-build-check is only for report", err.getvalue()) + self.assertIn("registry file not found", err.getvalue()) class BuildOutputTests(unittest.TestCase): @@ -312,7 +526,6 @@ def test_diagnostics_and_declarations(self) -> None: text = ("theorem a : True := by\n trivial\n\n/-- doc\nmore -/\n" "theorem b : True := trivial\n") self.assertEqual([t.declaration_at(text, n) for n in (2, 4, 6)], ["a", "b", "b"]) - self.assertEqual(t.command_line(text, 7), 6) self.assertTrue(t.CONSEQUENCE.search("❌️ Docstring on `#guard_msgs` does not match")) def test_module_paths(self) -> None: diff --git a/scripts/tidy_mirror_registry.json b/scripts/tidy_mirror_registry.json deleted file mode 100644 index 248c9e34c1..0000000000 --- a/scripts/tidy_mirror_registry.json +++ /dev/null @@ -1,82 +0,0 @@ -[ - { - "original": "Cslib.Complexity.computableTidilyInPolyTime_andVerifier", - "plain": "Cslib.Complexity.computableInPolyTime_andVerifier", - "module": "Complexity.Computability.Complexity.Classes.SharpP.Combinators" - }, - { - "original": "Cslib.Complexity.computableTidilyInPolyTime_orVerifier", - "plain": "Cslib.Complexity.computableInPolyTime_orVerifier", - "module": "Complexity.Computability.Complexity.Classes.SharpP.Combinators" - }, - { - "original": "Cslib.Complexity.computableTidilyInPolyTime_selectVerifier", - "plain": "Cslib.Complexity.computableInPolyTime_selectVerifier", - "module": "Complexity.Computability.Complexity.Classes.SharpP.Combinators" - }, - { - "original": "Turing.MultiTapeTM.ComputableInTimeAndSpace.computableTidilyInPolyTime", - "plain": "Turing.MultiTapeTM.ComputableInTimeAndSpace.computableInPolyTime", - "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain" - }, - { - "original": "Turing.MultiTapeTM.ComputableTidilyInPolySpace.id'", - "plain": "Turing.MultiTapeTM.ComputableInPolySpace.id'", - "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolySpace" - }, - { - "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.comp", - "plain": "Turing.MultiTapeTM.ComputableInPolyTime.comp", - "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" - }, - { - "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.comp'", - "plain": "Turing.MultiTapeTM.ComputableInPolyTime.comp'", - "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" - }, - { - "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.const", - "plain": "Turing.MultiTapeTM.ComputableInPolyTime.const", - "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" - }, - { - "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.fst", - "plain": "Turing.MultiTapeTM.ComputableInPolyTime.fst", - "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" - }, - { - "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.id'", - "plain": "Turing.MultiTapeTM.ComputableInPolyTime.id'", - "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" - }, - { - "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.ite'", - "plain": "Turing.MultiTapeTM.ComputableInPolyTime.ite'", - "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" - }, - { - "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.of_eq", - "plain": "Turing.MultiTapeTM.ComputableInPolyTime.of_eq", - "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" - }, - { - "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.pair", - "plain": "Turing.MultiTapeTM.ComputableInPolyTime.pair", - "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" - }, - { - "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.polyBounded_length", - "plain": "Turing.MultiTapeTM.ComputableInPolyTime.polyBounded_length", - "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" - }, - { - "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.prod", - "plain": "Turing.MultiTapeTM.ComputableInPolyTime.prod", - "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" - }, - { - "original": "Turing.MultiTapeTM.ComputableTidilyInPolyTime.snd", - "plain": "Turing.MultiTapeTM.ComputableInPolyTime.snd", - "module": "Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime" - } -] diff --git a/scripts/tidy_sweep.py b/scripts/tidy_sweep.py index 2a5621bcb5..3579348b6c 100644 --- a/scripts/tidy_sweep.py +++ b/scripts/tidy_sweep.py @@ -3,51 +3,55 @@ Usage: python3 scripts/tidy_sweep.py report [--area AREA]... [--json OUT] [--markdown OUT] python3 scripts/tidy_sweep.py rewrite --area AREA [--diff OUT | --verify [--rounds N]] - python3 scripts/tidy_sweep.py stub-registry [--output FILE] -Common options: [--registry FILE] [--allowlist FILE] [--build-dir DIR] [--no-build-check] - -Tidy computability is a proof device: outside the raw machine constructions of the allowlist -(`scripts/tidy_allowlist.txt`, from #608), no public statement should mention it. Every public -declaration outside the allowlist whose statement (its type, or the exposed body of a definition) -mentions a tidy predicate falls in one case of the S2 design +Common options: [--registry FILE] [--allowlist FILE] [--build-dir DIR]; report also accepts +[--no-build-check] and [--no-plan]. + +Plain computability is the API and tidy computability is how the machine layer proves it: outside +the raw machine constructions of the allowlist (`scripts/tidy_allowlist.txt`, from #608), no +public statement should mention a tidy notion. Every public declaration outside the allowlist +whose statement (its type, or the exposed body of a definition) mentions a tidy predicate falls +in one case of the S2 design (https://github.com/cslib-community/complexitylib/issues/456#issuecomment-6376748411): -1. a theorem with a registered plain twin (`--registry`): proofs that become plain use the twin; +1. a theorem with a committed plain twin: proofs that become plain use the twin, and the + original is left for S1/S3 to internalize; 2. any other theorem: it is renamed `computableTidily…` → `computable…` (the target name must be free) and restated with the plain predicates; 3. a definition, instance or structure field: it is listed for a hand-written plain redefinition. -A declaration that fits none of these is *unclassifiable*: it mentions a tidy notion without a -same-bound plain equivalence, is a plain/tidy bridge or a deprecated alias, or its target name is -taken (a collision). `report` prints the classification with per-area counts (#587's areas) and -each area's rewrite plan, without writing anything. +The twin of a tidy theorem is the public plain theorem named by its plain rename (`exact` when its +statement is the syntactic plain transport, `by name` otherwise, for instance a broader canonical +rule). `--registry` adds pairs from a migration script: a JSON array of +`{"original": name, "plain": name, "module": module}` objects, validated strictly. A declaration +that fits none of the cases is *unclassifiable*: it mentions a tidy notion without a same-bound +plain equivalence, is a plain/tidy bridge or a deprecated alias, or its target name is taken (a +collision). `report` prints the classification with per-area counts (#587's areas) and each +area's rewrite plan, without writing anything. `rewrite --area AREA` restates the area's case 2 declarations and rewrites every reference to them in the three libraries, at the exact ranges recorded in the `.ilean` files (full names, names -relative to namespaces and `open`s, dot notation), and in comments and READMEs. A declaration is -*deferred* (left tidy) when its statement names another tidy declaration, gets a tidy hypothesis -from a `variable` command, or is written inside a tidy namespace. A restated proof is *translated* -when every tidy declaration it names has a plain counterpart (a twin or a restated lemma): those -names are replaced in place. Otherwise it is *wrapped*: the old proof runs on tidy hypotheses -(`have h := h.tidy`) and its conclusion is converted (`refine .of_tidy ?_`); statements that are -not a bare predicate are transported with `simpa only []`. A reference from a proof -that stays tidy keeps its old type: the application becomes `(lemma args).tidy`, with `.of_tidy` -around tidy arguments, and references to case 1 originals stay. `.of_tidy (x.tidy)` round trips -are then removed. Whatever cannot be done mechanically is listed as manual work. - -With `--verify`, the three libraries are built after the rewrite, repeatedly: a translated proof -that fails is wrapped instead, and a wrapped proof or a client declaration that fails (typically -a tidy `fun_prop` that used a restated `@[fun_prop]` lemma) is preceded by -`attribute [local fun_prop] ComputableInPolyTime.tidy in`. Remaining failures are reported. With -`--stub-failures` (measurement only, never commit the result), proofs that still fail become -`sorry`, so that later rounds reach the modules downstream of them. `--diff` writes the plan as a +relative to namespaces and `open`s, dot notation), and in comments and READMEs. No edit is made +at a span whose text does not spell the referenced constant, and a replacement name is written +only if it resolves to its target, and nothing else, from its position (namespaces, `open`s, +private names of the module, local binders); `rewrite` therefore needs current build outputs. + +A declaration is *deferred* (left tidy, with its references unchanged) when its statement names +another tidy declaration, gets a tidy hypothesis from a `variable` command, or is written inside +a tidy namespace, and when a reference to it cannot be converted completely. A restated proof is +*translated* when every tidy declaration it names has a plain counterpart (a twin or a restated +lemma): those names are replaced in place. Otherwise it is *wrapped*: the old proof runs on tidy +hypotheses (`have h := h.tidy`) and its conclusion is converted (`refine .of_tidy ?_`); +statements that are not a bare predicate are transported with `simpa only []`. A +reference from a proof that stays tidy keeps its old type: the application becomes +`(lemma args).tidy`, with `.of_tidy` around tidy arguments; references to case 1 originals stay +there, and the plan counts them. `.of_tidy (x.tidy)` round trips are then removed. + +With `--verify`, the three libraries are built strictly (`--wfail --iofail`) after the rewrite; a +translated proof that fails is wrapped instead and the build repeated. Failures that remain, such +as a tidy `fun_prop` that relied on a lemma the batch made plain, mark plain-calculus gaps: they +are reported, the status is `failed` and the exit code nonzero. `--diff` writes the plan as a patch instead of rewriting files. -The registry is a JSON array of `{"original": name, "plain": name, "module": module}` objects, the -format of #608's `#mirror_pairs`. Until S1 lands, `scripts/tidy_mirror_registry.json` is a stub, -written by `stub-registry`: the existing declarations whose name is the plain rename of a tidy -theorem and whose statement is its plain transport. - Declarations, statements and references come from `scripts/quality_report.py` and `scripts/QualityReport.lean`, which read the build outputs of `lake build Complexity ComplexityTests ComplexityAbstracts`. @@ -71,7 +75,6 @@ from proof_lengths import masks # noqa: E402 ALLOWLIST = ROOT / "scripts/tidy_allowlist.txt" -REGISTRY = ROOT / "scripts/tidy_mirror_registry.json" TM = "Turing.MultiTapeTM." @@ -138,22 +141,77 @@ def load_allowlist(path: Path) -> set[str]: def load_registry(path: Path | None) -> dict[str, str]: - """original → plain twin, from a JSON array of `{"original", "plain", "module"}` objects (the - output of #608's `#mirror_pairs`), or an object holding it under `"pairs"`.""" - if path is None or not path.exists(): + """original → plain twin, from a migration script's JSON: an array of + `{"original": name, "plain": name, "module": module}` objects (`module` optional), or an + object whose only key `"pairs"` holds that array. Malformed or ambiguous input is an error: + a missing file, other keys, empty or blank names, an entry whose names agree, or two entries + giving one original different twins.""" + if path is None: return {} - data = json.loads(path.read_text()) + if not path.is_file(): + raise ValueError(f"{path}: registry file not found") + try: + data = json.loads(path.read_text()) + except json.JSONDecodeError as error: + raise ValueError(f"{path}: not JSON ({error})") from None if isinstance(data, dict): - data = data.get("pairs", []) - registry = {} - for row in data: - if not (isinstance(row, dict) and isinstance(row.get("original"), str) - and isinstance(row.get("plain"), str)): - raise ValueError(f"{path}: malformed registry entry {row!r}") - registry[row["original"]] = row["plain"] + if set(data) != {"pairs"}: + raise ValueError(f"{path}: expected an array of pairs or an object with exactly the " + f"key \"pairs\", found keys {sorted(data)}") + data = data["pairs"] + if not isinstance(data, list): + raise ValueError(f"{path}: expected an array of pairs") + registry: dict[str, str] = {} + for i, row in enumerate(data): + where = f"{path}: entry {i}" + if not isinstance(row, dict): + raise ValueError(f"{where}: expected an object, found {row!r}") + if set(row) - {"original", "plain", "module"} or not {"original", "plain"} <= set(row): + raise ValueError(f"{where}: expected the keys original, plain and optionally module, " + f"found {sorted(row)}") + for key in row: + value = row[key] + if not isinstance(value, str) or not value or value != value.strip() \ + or any(c.isspace() for c in value): + raise ValueError(f"{where}: `{key}` must be a nonempty name, found {value!r}") + original, plain = row["original"], row["plain"] + if original == plain: + raise ValueError(f"{where}: `{original}` is its own twin") + if registry.get(original, plain) != plain: + raise ValueError(f"{where}: `{original}` has two twins, `{registry[original]}` and " + f"`{plain}`") + registry[original] = plain return registry +def discover_twins(constants: dict[str, dict]) -> dict[str, tuple[str, str]]: + """The committed plain twins: for each public tidy theorem of the supported notions, the + public theorem named by its plain rename whose statement mentions no tidy constant. The kind + is `exact` when that statement is the syntactic plain transport and `by name` otherwise (for + instance a broader canonical rule, which S1 checks).""" + out = {} + for name, const in constants.items(): + if const["k"] != "thm" or not const["e"] or not const.get("tidy") or name in BRIDGES: + continue + if any(t not in BY_TIDY for t in const["tidy"]): + continue + twin = plain_name(name) + other = constants.get(twin) + if twin != name and other and other["k"] == "thm" and other["e"] \ + and not other.get("tidy"): + out[name] = (twin, "exact" if other.get("ph") == const.get("ph") else "by name") + return out + + +def twin_map(constants: dict[str, dict], registry: dict[str, str] + ) -> dict[str, tuple[str, str]]: + """Discovered twins, overridden by explicit registry pairs.""" + twins = discover_twins(constants) + for original, plain in registry.items(): + twins[original] = (plain, "registry") + return twins + + # --- Classification ----------------------------------------------------------------------------- @dataclass @@ -166,6 +224,7 @@ class Entry: case: str # "1", "2", "3" or "unclassifiable" reason: str = "" target: str = "" # the twin (case 1) or the new name (case 2) + twin: str = "" # case 1: `exact`, `by name` or `registry` notions: list[str] = field(default_factory=list) unsupported: list[str] = field(default_factory=list) body_only: bool = False # mentions tidy only in its exposed body @@ -186,8 +245,8 @@ def decl_kind(decl: dict) -> str: return "definition" -def classify_decl(decl: dict, const: dict, registry: dict[str, str], constants: dict[str, dict], - private_names: dict[str, set[str]]) -> Entry: +def classify_decl(decl: dict, const: dict, twins: dict[str, tuple[str, str]], + constants: dict[str, dict], private_names: dict[str, set[str]]) -> Entry: """The S2 case of one public declaration whose statement mentions a tidy constant.""" name = decl["name"] tidy = sorted(set(const.get("tidy", [])) | set(const.get("tb", []))) @@ -211,30 +270,30 @@ def classify_decl(decl: dict, const: dict, registry: dict[str, str], constants: f"`{t}`" for t in entry.unsupported) elif entry.kind != "theorem": entry.case = "3" - elif name in registry: - twin = registry[name] - entry.target = twin + elif name in twins: + twin, kind = twins[name] + entry.target, entry.twin = twin, kind if twin not in constants: entry.reason, entry.detail = "registered twin missing", f"`{twin}` is not built" + elif constants[twin].get("tidy"): + entry.reason, entry.detail = "registered twin missing", f"`{twin}` is tidy" else: entry.case = "1" if constants[twin].get("ph") != const.get("ph"): entry.warnings.append("the twin's statement is not the syntactic plain " - "transport (checked only up to definitional equality " - "by S1)") + "transport; proofs that use it are checked by the build") else: target = plain_name(name) entry.target = target taken = target in constants or target in private_names.get(decl["module"], set()) if target != name and taken: existing = constants.get(target) - same = existing is not None and existing.get("ph") == const.get("ph") entry.collision = { "target": target, "module": existing["m"] if existing else decl["module"], - "equivalent": same, "private": existing is None or not existing["e"]} + "private": existing is None or not existing["e"]} entry.reason = "collision" - entry.detail = ("the target has the plain statement but is not a registered twin" - if same else "the target exists with another statement") + entry.detail = ("the target is private" if existing is None or not existing["e"] + else "the target is not a public plain theorem") else: entry.case = "2" return entry @@ -251,7 +310,7 @@ def private_by_module(constants: dict[str, dict]) -> dict[str, set[str]]: return out -def classify_all(model: "Model", registry: dict[str, str]) -> list[Entry]: +def classify_all(model: "Model", twins: dict[str, tuple[str, str]]) -> list[Entry]: entries = [] privates = private_by_module(model.constants) for name, decl in sorted(model.decls.items()): @@ -260,14 +319,13 @@ def classify_all(model: "Model", registry: dict[str, str]) -> list[Entry]: continue if "Complexity/" + decl["path"] in model.allowlist: continue - entries.append(classify_decl(decl, const, registry, model.constants, privates)) + entries.append(classify_decl(decl, const, twins, model.constants, privates)) targets = Counter(e.target for e in entries if e.case == "2" and e.target != e.name) for e in entries: if e.case == "2" and e.target != e.name and targets[e.target] > 1: e.case, e.reason = "unclassifiable", "collision" e.detail = "another declaration renames to the same target" - e.collision = {"target": e.target, "module": e.module, "equivalent": False, - "private": False} + e.collision = {"target": e.target, "module": e.module, "private": False} return entries @@ -341,11 +399,14 @@ def summary(entries: list[Entry]) -> dict: def markdown_report(report: dict, limit: int = 40) -> str: s = report["summary"] dirty = " with uncommitted changes" if report["dirty"] else "" + twins = ", ".join(f"{n} {k}" for k, n in sorted(report["twins"].items())) or "none" + registry = (f" (`{report['registry']}`: {report['registry_size']} pairs)" + if report["registry"] else "") out = [f"Revision `{report['revision']}`{dirty}; build outputs {report['outputs']}. " - f"Allowlist: {report['allowlist_size']} modules. " - f"Registry: {report['registry_size']} pairs (`{report['registry']}`).", "", + f"Allowlist: {report['allowlist_size']} modules. Plain twins of tidy theorems: " + f"{twins}{registry}.", "", "### Public declarations whose statement mentions a tidy predicate", "", - "| Area | Total | (1) Registered twin | (2) Rename and restate | " + "| Area | Total | (1) Plain twin | (2) Rename and restate | " "(3) Definition or field | Unclassifiable |", "|---|--:|--:|--:|--:|--:|"] for area, c in list(s["areas"].items()) + [("Total", s["total"])]: out.append(f"| {area} | {c.get('total', 0):,} | {c.get('1', 0):,} | {c.get('2', 0):,} | " @@ -355,12 +416,10 @@ def markdown_report(report: dict, limit: int = 40) -> str: collisions = [e for e in report["entries"] if e["collision"]] if collisions: out += ["", "### Collisions", "", - "| Declaration | Target | Target module | Same plain statement |", - "|---|---|---|---|"] + "| Declaration | Target | Target module | Why |", "|---|---|---|---|"] for e in collisions[:limit]: c = e["collision"] - out.append(f"| `{e['name']}` | `{c['target']}` | `{c['module']}` | " - f"{'yes' if c['equivalent'] else 'no'} |") + out.append(f"| `{e['name']}` | `{c['target']}` | `{c['module']}` | {e['detail']} |") if len(collisions) > limit: out.append(f"| … {len(collisions) - limit} more in the JSON report | | | |") unsupported = Counter(t for e in report["entries"] for t in e["unsupported"]) @@ -998,33 +1057,42 @@ class FileEdits: class Planner: - """The edits of one area's batch: case 2 declarations restated and renamed, their clients - converted, and case 1 twins used in translated proofs.""" + """The edits of one area's batch: case 2 declarations restated and renamed, the references + to them converted, and case 1 twins used in proofs that become plain. - def __init__(self, model: Model, entries: list[Entry], registry: dict[str, str], area: str, - force_wrap: frozenset[str] = frozenset(), - force_bridge: frozenset[tuple[str, str]] = frozenset(), - stub: frozenset[tuple[str, str]] = frozenset()): + No edit is made at a span whose text does not spell the referenced constant, and a + replacement is written only when it resolves to its intended target, and nothing else, from + its position. A declaration with a reference that cannot be converted completely is deferred + (left tidy), so that skipped references stay unchanged.""" + + def __init__(self, model: Model, entries: list[Entry], twins: dict[str, str], area: str, + force_wrap: frozenset[str] = frozenset()): self.model, self.area, self.force_wrap = model, area, force_wrap - self.force_bridge, self.stub = force_bridge, stub self.entries = {e.name: e for e in entries} self.batch = {e.name: e for e in entries if e.area == area and e.case == "2"} - self.renames = {name: e.target for name, e in self.batch.items()} - self.twins = {o: p for o, p in registry.items() if p in model.constants} - self.files: dict[Path, FileEdits] = defaultdict(FileEdits) + self.twins = {o: p for o, p in twins.items() if p in model.constants} + self.privates = private_by_module(model.constants) + self.known = model.known | {e.target for e in self.batch.values()} + self.namespaces = namespaces_of(self.known) self.sources: dict[Path, SourceFile] = {} + self.deferred: dict[str, list[str]] = {} + self._refs: dict[str, list[Ref]] = {} + self._locals: dict[tuple[str, int, int], set[str]] = {} + self.reset() + + def reset(self) -> None: + """Forget the edits of a planning pass.""" + self.renames = {n: e.target for n, e in self.batch.items() if n not in self.deferred} + self.files: dict[Path, FileEdits] = defaultdict(FileEdits) self.manual: list[Manual] = [] self.decls: dict[str, dict] = {} self.spans: dict[str, list[tuple[int, int, str]]] = defaultdict(list) self.needs: dict[str, dict[str, bool]] = defaultdict(dict) - self.sites = Counter() + self.sites: Counter = Counter() + self.twin_refs: Counter = Counter() self.imports: list[tuple[str, str, bool]] = [] - self.known = model.known | set(self.renames.values()) - self.namespaces = namespaces_of(self.known) + self.blockers: dict[str, list[str]] = defaultdict(list) self.round_trips = 0 - self.deferred: dict[str, list[str]] = {} - self.bridged: list[str] = [] - self.stubbed: list[str] = [] # Sources and references. @@ -1034,13 +1102,15 @@ def source(self, path: Path) -> SourceFile: return self.sources[path] def refs(self, module: str) -> list[Ref]: - src = self.source(qr.source_path(module)) - out = [] - for name, _, info in self.model.lib.references(module): - for u in info["usages"]: - out.append(Ref(name, src.at(u[0], u[1]), src.at(u[2], u[3]), - u[4] if len(u) == 5 else None)) - return out + if module not in self._refs: + src = self.source(qr.source_path(module)) + out = [] + for name, _, info in self.model.lib.references(module): + for u in info["usages"]: + out.append(Ref(name, src.at(u[0], u[1]), src.at(u[2], u[3]), + u[4] if len(u) == 5 else None)) + self._refs[module] = sorted(out, key=lambda x: x.start) + return self._refs[module] def ref_kind(self, name: str) -> str: owner = qr.owner_of(name, self.model.owners) or name @@ -1070,6 +1140,9 @@ def note(self, path: Path, offset: int, decl: str | None, kind: str, detail: str self.manual.append(Manual(str(path.relative_to(ROOT)), src.line_of(offset), decl or "", kind, detail)) + def where(self, path: Path, offset: int) -> str: + return f"{path.relative_to(ROOT)}:{self.source(path).line_of(offset)}" + def need(self, module: str, constant: str, public: bool) -> None: defining = self.model.constants.get(constant, {}).get("m") if defining and defining != module: @@ -1081,56 +1154,109 @@ def notions_of(self, name: str) -> list[Notion]: # Names. - def rename_at(self, src: SourceFile, start: int, end: int, old: str, new: str) -> str | None: - """The written form of `new` replacing the reference to `old` at `start`.""" + def local_names(self, module: str, src: SourceFile, offset: int) -> set[str]: + """Identifiers of the declaration (or command) around `offset` that are not references + to constants: binders, local hypotheses, tactic names. A written name whose first + component is one of them could be captured by a local.""" + ranges = self.model.lib.ileans.get(module, {}).get("decls", {}).values() + span = next(((src.at(r[0], r[1]), src.at(r[2], r[3])) for r in ranges + if src.at(r[0], r[1]) <= offset < src.at(r[2], r[3])), None) + if span is None: + starts = src.commands + [len(src.mask)] + start = max([s for s in starts if s <= offset], default=0) + span = (start, min(s for s in starts if s > offset) if offset < len(src.mask) + else len(src.mask)) + key = (module, *span) + if key not in self._locals: + refs = [(x.start, x.end) for x in self.refs(module) + if span[0] <= x.start < span[1]] + names = set() + for match in IDENT.finditer(src.mask, *span): + if not any(a <= match.start() < b for a, b in refs): + names.add(match[0].split(".")[0]) + self._locals[key] = names - KEYWORDS + return self._locals[key] + + def resolves(self, module: str, src: SourceFile, offset: int, written: str) -> set[str]: + """What `written` (without `@`) can denote at `offset`: constants reached through the + enclosing namespaces and the opened namespaces, private constants of the module, and a + local of the same name (as `""`).""" + names = self.known | self.privates.get(module, set()) + if written.startswith("_root_."): + return {written[len("_root_."):]} & names + hits = {p + "." + written if p else written for p in src.scopes.prefixes(offset)} + out = hits & names + if written.split(".")[0] in self.local_names(module, src, offset): + out.add("") + return out + + def written(self, module: str, src: SourceFile, start: int, end: int, old: str, new: str + ) -> tuple[str | None, str]: + """The text replacing the reference to `old` at `[start, end)` by one to `new`, or None + and the reason it cannot be written.""" token = src.text[start:end] + if not spells(token, old): + return None, f"the reference span `{token}` does not spell `{old}`" if old == new: - return token - if start and src.text[start - 1] == ".": # field or leading-dot notation - if old.rsplit(".", 1)[-1] == new.rsplit(".", 1)[-1]: - return token - if old.rsplit(".", 1)[0] == new.rsplit(".", 1)[0] and "." not in token: - return new.rsplit(".", 1)[-1] - return None - candidate = renamed_token(token, old, new) - if candidate is not None and not candidate.lstrip("@").startswith("_root_."): - return candidate + return token, "" + leading = token.startswith(".") + if leading or (start and src.text[start - 1] == "."): # leading-dot or field notation + last = new.rsplit(".", 1)[-1] + if old.rsplit(".", 1)[-1] == last: + return token, "" + if namespace_of(old) == namespace_of(new) and "." not in token.lstrip("."): + return ("." if leading else "") + last, "" + return None, "dot notation on a declaration whose namespace changes" at = "@" if token.startswith("@") else "" - return at + written_name(new, src.scopes.prefixes(start), self.known) + candidates = [renamed_token(token.removeprefix("@"), old, new)] + parts = new.split(".") + candidates += [".".join(parts[-k:]) for k in range(1, len(parts) + 1)] + candidates.append("_root_." + new) + for candidate in candidates: + if candidate and self.resolves(module, src, start, candidate) == {new}: + return at + candidate, "" + return None, f"no written form of `{new}` resolves to it here" # Declarations. def plan(self) -> "Planner": analyses = {name: self.analyse_decl(self.batch[name]) for name in sorted(self.batch)} + for name, a in analyses.items(): + if a is None: + self.deferred[name] = ["declaration range missing"] + elif a["defer"]: + self.deferred[name] = list(a["defer"]) + while True: + self.defer_statements(analyses) + self.reset() + for name in sorted(self.renames): + self.plan_decl(self.batch[name], analyses[name]) + for name in sorted(self.renames): + self.plan_clients(name) + if not self.blockers: + break + for name, reasons in self.blockers.items(): + self.deferred[name] = sorted(set(reasons)) + for name in sorted(self.deferred): + self.defer(name, analyses.get(name)) + self.plan_comments() + self.plan_imports() + return self + + def defer_statements(self, analyses: dict) -> None: + """Defer, to a fixed point, the declarations whose statements name deferred ones.""" changed = True - while changed: # a statement naming a deferred declaration is deferred too + while changed: changed = False for name, a in analyses.items(): if name in self.deferred or a is None: continue - reasons = list(a["defer"]) + [ - f"statement names deferred `{x.name}`" for x in a["sig_refs"] - if (qr.owner_of(x.name, self.model.owners) or x.name) in self.deferred] + 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) + in self.deferred] if reasons: self.deferred[name] = reasons changed = True - for name, a in analyses.items(): - if a is None: - self.deferred.setdefault(name, ["declaration range missing"]) - for name in self.deferred: - self.renames.pop(name, None) - for name in sorted(self.batch): - if name in self.deferred: - self.defer(name, analyses[name]) - else: - self.plan_decl(self.batch[name], analyses[name]) - for name in sorted(self.renames): - self.plan_clients(name) - self.plan_bridges() - self.plan_stubs() - self.plan_comments() - self.plan_imports() - return self def analyse_decl(self, entry: Entry) -> dict | None: """Parse a declaration and find what prevents restating it.""" @@ -1148,8 +1274,11 @@ def analyse_decl(self, entry: Entry) -> dict | None: a = {"module": module, "path": path, "src": src, "dt": dt, "start": start, "end": end, "sig_refs": [x for x in refs if x.start < split], "proof_refs": [x for x in refs if x.start >= split], "defer": []} - if entry.target != entry.name and renamed_token( - src.text[sel_start:sel_end], entry.name, entry.target) is None: + token = src.text[sel_start:sel_end] + if not spells(token, entry.name): + a["defer"].append(f"the declaration range `{token}` does not spell its name") + elif entry.target != entry.name and renamed_token(token, entry.name, + entry.target) is None: a["defer"].append("name written inside a tidy namespace") for x in a["sig_refs"]: if self.ref_kind(x.name) in ("bridge", "tidy"): @@ -1159,51 +1288,6 @@ def analyse_decl(self, entry: Entry) -> dict | None: a["defer"].append("tidy predicate from a `variable` command or notation") return a - def plan_bridges(self) -> None: - """Let the tidy `fun_prop` calls of the declarations in `force_bridge` use the restated - (plain) certificates: `attribute [local fun_prop] ComputableInPolyTime.tidy in`.""" - notions = {n for name in self.renames for n in self.notions_of(name)} - for module, name in sorted(self.force_bridge): - ranges = self.model.lib.ileans.get(module, {}).get("decls", {}) - path = qr.source_path(module) - src = self.source(path) - if name.startswith("line:"): - start = src.starts[command_start_line(src, int(name[5:]))] - elif name in ranges: - start = src.at(ranges[name][0], ranges[name][1]) - else: - continue - if name in self.batch: - own = set(self.notions_of(name)) - else: - own = notions - lines = "".join( - f"attribute [local fun_prop] " - f"{written_name(n.to_tidy, src.scopes.prefixes(start), self.known)} in\n" - for n in sorted(own, key=lambda n: n.tidy)) - self.files[path].replaces.append(Replace(start, start, lines)) - for n in own: - self.need(module, n.to_tidy, False) - self.bridged.append(name) - - def plan_stubs(self) -> None: - """Measurement only (`--stub-failures`): replace the proofs of `stub` by `sorry`, so that - a build reaches the modules downstream of them.""" - for module, name in sorted(self.stub): - ranges = self.model.lib.ileans.get(module, {}).get("decls", {}) - if name not in ranges: - continue - path = qr.source_path(module) - src, r = self.source(path), ranges[name] - start, end = src.at(r[0], r[1]), src.at(r[2], r[3]) - assign = find_top_level(src.mask, src.at(r[6], r[7]), end, ":=") - if assign < 0: - continue - fe = self.files[path] - fe.regions = [g for g in fe.regions if not (g.start >= start and g.end <= end)] - fe.regions.append(Region(assign + 2, end, lambda _: " by\n sorry", name)) - self.stubbed.append(name) - 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] @@ -1211,73 +1295,85 @@ def defer(self, name: str, a: dict | None) -> None: 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, - "mode": "deferred", "blocking": [], - "issues": self.deferred[name]} + "mode": "deferred", "blocking": [], "issues": self.deferred[name]} for reason in self.deferred[name]: self.note(path, a["start"] if a else 0, name, "deferred", reason) def plan_decl(self, entry: Entry, a: dict) -> None: module, path, src, dt = a["module"], a["path"], a["src"], a["dt"] start, end, sig_refs, proof_refs = a["start"], a["end"], a["sig_refs"], a["proof_refs"] - fe = self.files[path] info = {"name": entry.name, "target": entry.target, "path": str(path.relative_to(ROOT)), "line": src.line_of(start), "mode": "manual", "blocking": [], "issues": []} self.decls[entry.name] = info self.spans[module].append((start, end, entry.name)) - - def issue(kind: str, detail: str = "", offset: int = start) -> None: - info["issues"].append(kind) - self.note(path, offset, entry.name, kind, detail) - + replaces: list[Replace] = [] if entry.target != entry.name: token = src.text[dt.sel_start:dt.sel_end] - fe.replaces.append(Replace(dt.sel_start, dt.sel_end, - renamed_token(token, entry.name, entry.target))) + replaces.append(Replace(dt.sel_start, dt.sel_end, + renamed_token(token, entry.name, entry.target))) for x in sig_refs: if self.ref_kind(x.name) in ("pred", "renamed", "twin"): - new = self.rename_at(src, x.start, x.end, x.name, self.new_name(x.name)) + new, why = self.written(module, src, x.start, x.end, x.name, + self.new_name(x.name)) if new is None: - issue("statement reference in dot notation", x.name, x.start) - continue - fe.replaces.append(Replace(x.start, x.end, new)) - self.need(module, self.new_name(x.name), True) + self.blockers[entry.name].append( + f"{self.where(path, x.start)}: statement reference: {why}") + return + replaces.append(Replace(x.start, x.end, new)) doc = src.text[start:dt.sel_start] if TIDY_WORD.search(doc.split("-/")[0] if "/--" in doc else ""): - issue("docstring mentions tidiness (review wording)") + info["issues"].append("docstring mentions tidiness (review wording)") + self.note(path, start, entry.name, "docstring mentions tidiness (review wording)") info["blocking"] = sorted({x.name for x in proof_refs if self.ref_kind(x.name) in ("bridge", "tidy") and x.name != entry.name}) - wrap, problems = self.wrap_plan(entry, src, dt, sig_refs) + translation = [] if not info["blocking"] and entry.name not in self.force_wrap and dt.assign >= 0: + for x in proof_refs: + if self.ref_kind(x.name) in ("pred", "renamed", "twin"): + new, _ = self.written(module, src, x.start, x.end, x.name, + self.new_name(x.name)) + if new is None: + translation = None + break + translation.append((x, new)) + wrap, problems = self.wrap_plan(entry, src, dt, sig_refs) + if translation is not None and not info["blocking"] \ + and entry.name not in self.force_wrap and dt.assign >= 0: info["mode"] = "translate" elif wrap is not None: info["mode"] = "wrap" else: - for problem in problems: - issue("cannot wrap the proof", problem) - if not info["blocking"] and dt.assign >= 0: - info["mode"] = "translate" + self.blockers[entry.name].append( + f"{self.where(path, start)}: cannot wrap the proof: " + "; ".join(problems)) return - for x in proof_refs: - kind = self.ref_kind(x.name) - if info["mode"] == "translate" and kind in ("pred", "renamed", "twin"): - new = self.rename_at(src, x.start, x.end, x.name, self.new_name(x.name)) - if new is None: - issue("proof reference in dot notation to a renamed twin", x.name, x.start) - elif new != src.text[x.start:x.end]: + fe = self.files[path] + fe.replaces += replaces + for x in sig_refs: + if self.ref_kind(x.name) in ("pred", "renamed", "twin"): + self.need(module, self.new_name(x.name), True) + if info["mode"] == "translate": + for x, new in translation: + if new != src.text[x.start:x.end]: fe.replaces.append(Replace(x.start, x.end, new)) - if kind == "twin": + if self.ref_kind(x.name) == "twin": + self.twin_refs["redirected"] += 1 self.need(module, self.new_name(x.name), False) - elif info["mode"] == "wrap" and kind == "renamed" and x.name != entry.name: + return + for x in proof_refs: + kind = self.ref_kind(x.name) + if kind == "twin": + self.twin_refs["kept on the original"] += 1 + elif kind == "renamed" and x.name != entry.name: if x.name in self.renames: self.convert(path, module, x.start, x.end, x.name, entry.name, "tidy") else: - issue("generated constant of a restated declaration", x.name, x.start) - if info["mode"] == "wrap": - fe.regions.append(Region(dt.assign + 2, end, wrap, entry.name)) - for notion in self.notions_of(entry.name): - self.need(module, notion.of_tidy, False) - self.need(module, notion.iff, False) + self.blockers[entry.name].append( + f"{self.where(path, x.start)}: names generated constant `{x.name}`") + fe.regions.append(Region(dt.assign + 2, end, wrap, entry.name)) + for notion in self.notions_of(entry.name): + self.need(module, notion.of_tidy, False) + self.need(module, notion.iff, False) def hidden_tidy(self, name: str, src: SourceFile, dt: DeclText, sig_refs: list[Ref]) -> bool: """Whether the statement has more tidy binders or conclusions than are written.""" @@ -1356,65 +1452,73 @@ def plan_clients(self, name: str) -> None: self.convert(path, module, start, end, name, u[4] if len(u) == 5 else None, context) def convert(self, path: Path, module: str, start: int, end: int, old: str, - decl: str | None, context: str) -> None: + decl: str | None, context: str) -> bool: """Rename a reference to a restated declaration; in a proof that stays tidy, keep the site's old type with `.tidy` around the application and `.of_tidy` around tidy - arguments.""" - src, fe = self.source(path), self.files[path] + arguments. The edits are made only when the whole conversion is supported; otherwise + `old` is blocked (and will be deferred), and the site stays unchanged.""" + src = self.source(path) new = self.renames[old] - token = src.text[start:end] - written = self.rename_at(src, start, end, old, new) - self.sites[context] += 1 - if written is None: - self.note(path, start, decl, "reference in dot notation", f"`{token}`") - return - if written != token: + written, why = self.written(module, src, start, end, old, new) + wraps: list[Wrap] = [] + if written is not None and context == "tidy": + why, wraps = self.convert_site(src, start, end, old) + if written is None or why: + self.blockers[old].append(f"{self.where(path, start)}: {why}") + return False + fe = self.files[path] + if written != src.text[start:end]: fe.replaces.append(Replace(start, end, written)) - if context != "tidy": - return - problem = self.convert_site(src, fe, start, end, old) - if problem: - self.note(path, start, decl, "reference kept tidy", f"`{token}`: {problem}") - else: + fe.wraps += wraps + self.sites[context] += 1 + if wraps: for notion in self.notions_of(old): self.need(module, notion.of_tidy, False) + return True - def convert_site(self, src: SourceFile, fe: FileEdits, start: int, end: int, - old: str) -> str | None: + def convert_site(self, src: SourceFile, start: int, end: int, old: str + ) -> tuple[str, list[Wrap]]: + """The wraps that keep the old type of the application of `old` at `start`, or the + reason it cannot be converted (and no wraps).""" sg = self.model.constants.get(old, {}).get("sg") if not sg: - return None + return "", [] binders, conclusion = sg mask = src.mask opener = enclosing_opener(mask, start) if opener >= 0 and mask[opener] == "[" and LEMMA_LIST_TACTIC.search( mask[mask.rfind("\n", 0, opener) + 1:opener]): - return "used in a tactic lemma list" + return "used in a tactic lemma list", [] explicit_all = src.text[start:end].startswith("@") or (start and mask[start - 1] == "@") site_start = start - 1 if start and mask[start - 1] == "@" else start positions = [i for i, (bi, _) in enumerate(binders) if explicit_all or bi == 0] if not explicit_all and any(flag and bi != 0 for bi, flag in binders): - return "implicit tidy hypothesis" - if start and mask[start - 1] == ".": + return "implicit tidy hypothesis", [] + if conclusion == 2: + return "conclusion is not a bare tidy predicate", [] + if src.text[start:end].startswith("."): + if conclusion: # the expected type changes with the conclusion + return "leading-dot notation", [] + elif start and mask[start - 1] == ".": before = mask[start - 2] if start >= 2 else " " if before.isspace() or before in OPENERS or before in "<|$,": - return "leading-dot notation" + return "leading-dot notation", [] site_start = receiver_start(mask, start - 1) if not positions or binders[positions[0]][1]: - return "dot notation on a tidy receiver" + return "dot notation on a tidy receiver", [] positions = positions[1:] named: list[tuple[int, int]] = [] args = parse_args(mask, end, len(mask), len(positions), line_indent(mask, start), named) if len(args) < len(positions): - return f"partial application ({len(args)} of {len(positions)} explicit arguments)" + return (f"partial application ({len(args)} of {len(positions)} explicit " + "arguments)"), [] + wraps = [] for (a, b), i in zip(args, positions): if binders[i][1] == 2: - return "tidy hypothesis under binders" + return "tidy hypothesis under binders", [] if binders[i][1] == 1: - fe.wraps.append(Wrap(a, b, "(.of_tidy ", ")", start)) + wraps.append(Wrap(a, b, "(.of_tidy ", ")", start)) site_end = max([end] + [b for _, b in args + named]) - if conclusion == 2: - return "conclusion is not a bare tidy predicate" if conclusion == 1: left = site_start - 1 while left >= 0 and mask[left] in " \t\n": @@ -1423,12 +1527,12 @@ def convert_site(self, src: SourceFile, fe: FileEdits, start: int, end: int, while right < len(mask) and mask[right] in " \t\n": right += 1 if left >= 0 and mask[left] == "(" and match_bracket(mask, left) == right: - fe.wraps.append(Wrap(left, right + 1, "", ".tidy", site_start)) + wraps.append(Wrap(left, right + 1, "", ".tidy", site_start)) elif not args and site_start == start and IDENT.fullmatch(src.text[start:end]): - fe.wraps.append(Wrap(start, end, "", ".tidy", site_start)) + wraps.append(Wrap(start, end, "", ".tidy", site_start)) else: - fe.wraps.append(Wrap(site_start, site_end, "(", ").tidy", site_start)) - return None + wraps.append(Wrap(site_start, site_end, "(", ").tidy", site_start)) + return "", wraps # Documentation. @@ -1550,19 +1654,22 @@ def summary(self) -> dict: kinds = Counter(m.kind for m in self.manual) return {"area": self.area, "declarations": len(self.batch), "modes": dict(modes), "manual": dict(kinds.most_common()), "sites": dict(self.sites), - "imports": [list(i) for i in self.imports], "bridged": sorted(self.bridged), - "stubbed": sorted(self.stubbed)} + "twin_references": dict(self.twin_refs), + "imports": [list(i) for i in self.imports]} -def command_start_line(src: SourceFile, line: int) -> int: - """The first line of the docstring and attributes above the 0-based `line`.""" - while line > 0: - above, above_mask = src.lines[line - 1], src.mask.split("\n")[line - 1] - if above.strip() and (not above_mask.strip() or above_mask.lstrip().startswith("@[")): - line -= 1 - else: - break - return line +def spells(token: str, name: str) -> bool: + """Whether `token`, the text at a reference span, writes `name`: the name itself or a suffix + of it on a component boundary, possibly after `@`, `_root_.` or the `.` of leading-dot + notation (a field name after a receiver's `.` is such a suffix too).""" + bare = token.removeprefix("@").removeprefix("_root_.") + if bare.startswith(".") and not bare.startswith(".."): + bare = bare[1:] + return bool(bare) and (name == bare or name.endswith("." + bare)) + + +def namespace_of(name: str) -> str: + return name.rsplit(".", 1)[0] if "." in name else "" def enclosing_opener(mask: str, pos: int) -> int: @@ -1618,9 +1725,18 @@ def plan_markdown(plan: dict, limit: int = 40) -> str: f"{m['detail']} |") if len(plan["manual"]) > limit: out.append(f"| … {len(plan['manual']) - limit} more in the JSON report | | | | |") + if s.get("twin_references"): + out.append("References to case 1 originals in restated proofs: " + ", ".join( + f"{n} {k}" for k, n in sorted(s["twin_references"].items())) + ".") if plan.get("build"): b = plan["build"] - out += ["", f"Build: {b['status']}. Declarations failing: {len(b['failing'])}."] + errors = [d for d in b["diagnostics"] if d["level"] == "error"] + out += ["", f"**Strict build: {b['status'].upper()}** (round {b['round']}, Lake exit " + f"code {b['exit_code']}, {len(errors)} errors). Restated declarations failing: " + f"{len(b['failing'])}; other declarations with errors: " + f"{len({d['decl'] for d in b['client_errors']})}."] + for d in errors[:limit]: + out.append(f"* `{d['path']}:{d['line']}` `{d['decl']}`: {d['message'][:160]}") return "\n".join(out) @@ -1665,74 +1781,55 @@ def declaration_at(text: str, line: int) -> str: return "" -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] - return text.count("\n", 0, starts[-1]) + 1 if starts else line +STRICT = ("--wfail", "--iofail") # warnings fail the build, as in CI -def lake_build(targets: list[str]) -> tuple[int, str]: - proc = subprocess.run(["lake", "build", *targets], cwd=ROOT, text=True, - capture_output=True) +def lake_build(targets: list[str], runner=subprocess.run) -> tuple[int, str]: + proc = runner(["lake", "build", *STRICT, *targets], cwd=ROOT, text=True, + capture_output=True) return proc.returncode, proc.stdout + proc.stderr -def rewrite(model: Model, entries: list[Entry], registry: dict[str, str], area: str, - verify: bool, rounds: int, stub_failures: bool = False - ) -> tuple[Planner, dict | None]: - """Write the area's rewrite. With `verify`, build the three libraries and retry, up to - `rounds` times: a translated proof that fails is wrapped, and a wrapped proof or a client - declaration that fails gets a local plain → tidy `fun_prop` transition. With - `stub_failures` (measurement only), proofs that still fail become `sorry`, so that the next - round reaches the modules downstream of them.""" +def rewrite(model: Model, entries: list[Entry], twins: dict[str, str], area: str, + verify: bool, rounds: int, build=lake_build) -> tuple[Planner, dict | None]: + """Write the area's rewrite into the checkout. With `verify`, build the three libraries + strictly and, up to `rounds` times, wrap the translated proofs that fail and rebuild. + Remaining failures are reported, never patched over.""" originals: dict[Path, str] = {} force: set[str] = set() - bridge: set[tuple[str, str]] = set() - stub: set[tuple[str, str]] = set() - build, history = None, [] + result, history = None, [] for round_ in range(1, rounds + 1): for path, text in originals.items(): # plan against the sources of the build path.write_text(text, encoding="utf-8") - planner = Planner(model, entries, registry, area, frozenset(force), - frozenset(bridge), frozenset(stub)).plan() + planner = Planner(model, entries, twins, area, frozenset(force)).plan() texts = planner.render() for path, text in texts.items(): originals.setdefault(path, planner.source(path).text) path.write_text(text, encoding="utf-8") if not verify: return planner, None - targets = list(qr.ROOTS) - code, output = lake_build(targets) - build = check_build(planner, texts, output, code, round_, targets) - history.append({k: build[k] for k in ("round", "status", "failing", "forced_wrap", - "failing_clients")}) - retry = {d for d in build["failing"] if planner.decls.get(d, {}).get("mode") - == "translate"} - wrapped = {(planner.model.decls[d]["module"], d) for d in build["failing"] - if planner.decls.get(d, {}).get("mode") == "wrap"} - clients = {tuple(c) for c in build["failing_clients"]} - new_bridges = (wrapped | clients) - bridge - new_stubs = {x for x in (wrapped | clients) & bridge if not x[1].startswith("line:") - } - stub if stub_failures else set() - if not (retry or new_bridges or new_stubs) or round_ == rounds: + code, output = build(list(qr.ROOTS)) + result = check_build(planner, texts, output, code, round_) + history.append({k: result[k] for k in ("round", "status", "failing", "forced_wrap")}) + retry = {d for d in result["failing"] + if planner.decls.get(d, {}).get("mode") == "translate"} + if not retry or round_ == rounds: break force |= retry - bridge |= new_bridges - stub |= new_stubs - if build is not None: - build["history"] = history - return planner, build + result["history"] = history + return planner, result -def check_build(planner: Planner, texts: dict[Path, str], output: str, code: int, round_: int, - targets: list[str]) -> dict: +def check_build(planner: Planner, texts: dict[Path, str], output: str, code: int, + round_: int) -> dict: + """The outcome of a strict build: `passed` only when Lake succeeded and reported no error. + Errors are attributed to the restated declarations (`failing`) or to other declarations + (`client_errors`).""" by_written = {} for name, info in planner.decls.items(): by_written[(info["path"], name.rsplit(".", 1)[-1])] = name by_written[(info["path"], info["target"].rsplit(".", 1)[-1])] = name - failing, clients, failing_clients, problems = set(), [], set(), [] + failing, clients, problems = set(), [], [] for d in diagnostics(output): path = ROOT / d["path"] text = texts.get(path) or (path.read_text() if path.exists() else "") @@ -1745,27 +1842,12 @@ def check_build(planner: Planner, texts: dict[Path, str], output: str, code: int failing.add(decl) planner.decls[decl].setdefault("errors", []).append(d["message"]) elif d["level"] == "error": - 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 len(names) == 1: - failing_clients.add((module, names[0])) - item["decl"] = names[0] - elif text: - at = command_line(text, d["line"]) - 1 - block = text.split("\n")[at:min(at + 3, d["line"])] - original = planner.source(path).lines if path in texts else text.split("\n") - hits = [i for i in range(len(original)) - if original[i:i + len(block)] == block] - if len(hits) == 1: - failing_clients.add((module, f"line:{hits[0]}")) clients.append(item) problems.append(item) - return {"round": round_, "targets": targets, "status": "passed" if code == 0 else "failed", - "failing": sorted(failing), "client_errors": clients, - "failing_clients": sorted(failing_clients), "diagnostics": problems, - "forced_wrap": sorted(planner.force_wrap), - "bridged": sorted(planner.bridged), "stubbed": sorted(planner.stubbed)} + errors = any(d["level"] == "error" for d in problems) + return {"round": round_, "status": "passed" if code == 0 and not errors else "failed", + "exit_code": code, "failing": sorted(failing), "client_errors": clients, + "diagnostics": problems, "forced_wrap": sorted(planner.force_wrap)} def unified_diff(planner: Planner) -> str: @@ -1777,21 +1859,9 @@ def unified_diff(planner: Planner) -> str: return "".join(out) -def stub_registry(model: Model) -> list[dict]: - """Existing plain twins: for each tidy theorem, the declaration named by its plain rename - whose statement is its plain transport.""" - pairs = [] - for name, const in sorted(model.constants.items()): - if const["k"] != "thm" or not const["e"] or not const.get("tidy"): - continue - if any(t not in BY_TIDY for t in const["tidy"]) or name in BRIDGES: - continue - twin = plain_name(name) - other = model.constants.get(twin) - if twin != name and other and other["e"] and other.get("ph") == const.get("ph") \ - and not other.get("tidy"): - pairs.append({"original": name, "plain": twin, "module": const["m"]}) - return pairs +def exit_status(plans: list[dict]) -> int: + """Nonzero when a verified rewrite did not build.""" + return int(any(p["build"] is not None and p["build"]["status"] != "passed" for p in plans)) # --- Command line ------------------------------------------------------------------------------- @@ -1803,26 +1873,23 @@ def entry_json(e: Entry) -> dict: def main(argv: list[str] | None = None) -> int: parser = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) - parser.add_argument("command", choices=("report", "rewrite", "stub-registry")) + parser.add_argument("command", choices=("report", "rewrite")) parser.add_argument("--area", action="append", default=[], help="restrict to an area of #587 (repeatable for report)") - parser.add_argument("--registry", type=Path, default=REGISTRY) + 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("--no-build-check", action="store_true") + parser.add_argument("--no-build-check", action="store_true", + help="report only: do not check that the build outputs are current") parser.add_argument("--json", type=Path, help="write the full report as JSON") parser.add_argument("--markdown", type=Path, help="write the report as Markdown") parser.add_argument("--no-plan", action="store_true", help="report: skip rewrite plans") parser.add_argument("--verify", action="store_true", - help="rewrite: build the touched modules and wrap failing translations") + help="rewrite: build strictly, wrap failing translations, report the rest") parser.add_argument("--diff", type=Path, help="rewrite: write a unified diff of the plan instead of the files") - parser.add_argument("--rounds", type=int, default=6) - parser.add_argument("--stub-failures", action="store_true", - help="rewrite --verify, measurement only: replace proofs that still " - "fail by `sorry` to reach downstream modules (never commit the result)") - parser.add_argument("--output", type=Path, default=REGISTRY, - help="stub-registry: where to write the registry") + parser.add_argument("--rounds", type=int, default=3) parser.add_argument("--limit", type=int, default=40, help="rows per Markdown table") args = parser.parse_args(argv) for area in args.area: @@ -1830,37 +1897,41 @@ def main(argv: list[str] | None = None) -> int: parser.error(f"unknown area {area}; choose from {', '.join(AREA_ORDER)}") if args.command == "rewrite" and len(args.area) != 1: parser.error("rewrite needs exactly one --area") + if args.command == "rewrite" and args.no_build_check: + parser.error("rewrite edits at the recorded reference spans, so it needs current build " + "outputs; --no-build-check is only for report") + try: + registry = load_registry(args.registry) + except ValueError as error: + parser.error(str(error)) outputs = qr.check_outputs(args.build_dir, args.no_build_check) model = Model(args.build_dir, load_allowlist(args.allowlist)) - if args.command == "stub-registry": - pairs = stub_registry(model) - args.output.write_text(json.dumps(pairs, indent=1) + "\n") - print(f"wrote {len(pairs)} pairs to {args.output}") - return 0 - registry = load_registry(args.registry) - entries = classify_all(model, registry) + 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()) report = {"revision": revision, "dirty": dirty, "outputs": outputs, - "allowlist_size": len(model.allowlist), "registry": str(args.registry), + "allowlist_size": len(model.allowlist), + "registry": str(args.registry) if args.registry else None, "registry_size": len(registry), + "twins": dict(Counter(kind for _, kind in twins.values())), "registry_problems": registry_problems(registry, model.constants), "summary": summary(shown), "entries": [entry_json(e) for e in shown]} + plain_twins = {o: p for o, (p, _) in twins.items()} plans = [] if args.command == "rewrite" and args.diff: - planner = Planner(model, entries, registry, args.area[0]).plan() + planner = Planner(model, entries, plain_twins, args.area[0]).plan() args.diff.write_text(unified_diff(planner)) plans.append((planner, None)) elif args.command == "rewrite": - planner, build = rewrite(model, entries, registry, args.area[0], args.verify, - args.rounds, args.stub_failures) - plans.append((planner, build)) + plans.append(rewrite(model, entries, plain_twins, args.area[0], args.verify, + args.rounds)) elif not args.no_plan: for area in args.area or AREA_ORDER: if any(e.area == area and e.case == "2" for e in entries): - planner = Planner(model, entries, registry, area).plan() + planner = Planner(model, entries, plain_twins, area).plan() planner.render() plans.append((planner, None)) report["plans"] = [{"summary": p.summary(), "round_trips": p.round_trips, @@ -1875,7 +1946,7 @@ def main(argv: list[str] | None = None) -> int: print(text) if args.json: args.json.write_text(json.dumps(report, indent=1, ensure_ascii=False) + "\n") - return 0 + return exit_status(report["plans"]) if __name__ == "__main__": From 1312b01a4e5e1ec3574aa71c67a2ca734496b394 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 23:22:25 -0400 Subject: [PATCH 03/10] fix(scripts): establish every binding the tidy sweep writes MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Addresses review 5636433742 on #666: - Section `variable` binders, `open … renaming` and `export` aliases and notation tokens in scope count as captures of a written name, and a name counts as reachable only through an enclosing namespace, `_root_` or an open that is neither selective without it, hiding it nor `scoped`. Names come from the whole import closure (new `QualityReport.lean --names` mode), not only from the referenced ones. - Field and leading-dot references are kept only when the namespace changes with the tidy predicate itself; otherwise a leading-dot reference becomes an explicit, checked name and a field reference defers its declaration, since an abbreviation's own declarations can capture either. The plain-tidy equivalences written into wrapped proofs go through the same check. - A rename whose new name could capture another constant's reference is deferred. - `--diff` and `--verify` are mutually exclusive. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- scripts/QualityReport.lean | 35 +++- scripts/test_tidy_sweep.py | 98 ++++++++++- scripts/tidy_sweep.py | 336 ++++++++++++++++++++++++++++--------- 3 files changed, 376 insertions(+), 93 deletions(-) diff --git a/scripts/QualityReport.lean b/scripts/QualityReport.lean index 6df0804cb2..3adb97a7a2 100644 --- a/scripts/QualityReport.lean +++ b/scripts/QualityReport.lean @@ -36,6 +36,10 @@ 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 +every name the given modules and their transitive imports export: constants and `export` aliases, +one per line, for the name resolution of `scripts/tidy_sweep.py`. + It then prints `{"dup": [...], "k": ...}` lines grouping exported constants of different modules whose types are alpha-equivalent (`k = "thm"`), or whose types and exposed bodies are (`k = "def"`). Universe parameters are renamed positionally before comparing. @@ -197,7 +201,36 @@ unsafe def run (libDir : System.FilePath) (pairs : Option String := none) : IO U -- Keep the regions reachable until every expression has been used. if regions.isEmpty then stdout.flush +/-- Print the exported constants and `export` aliases of `roots` and their transitive imports, +found through the search path that `lake env` sets. -/ +unsafe def names (roots : List Name) : IO Unit := do + initSearchPath (← findSysroot) + let stdout ← IO.getStdout + let mut seen : NameSet := {} + let mut todo := roots.toArray + -- The mapped regions stay alive until the end of the program. + let mut regions : Array CompactedRegion := #[] + while h : todo.size > 0 do + let mod := todo.back + todo := todo.pop + if seen.contains mod then continue + seen := seen.insert mod + let (data, region) ← readModuleData (← findOLean mod) + regions := regions.push region + for i in data.imports do + unless seen.contains i.module do todo := todo.push i.module + for n in data.constNames do + unless n.isInternalDetail do stdout.putStrLn n.toString + for (ext, es) in data.entries do + if ext == `Lean.aliasExtension then + for e in es do + stdout.putStrLn (unsafeCast e : Name × Name).1.toString + if regions.isEmpty then stdout.flush + end ComplexityScripts.QualityReport unsafe def main (args : List String) : IO Unit := - ComplexityScripts.QualityReport.run (args.headD ".lake/build/lib/lean") args[1]? + if args.head? == some "--names" then + ComplexityScripts.QualityReport.names (args.drop 1 |>.map String.toName) + else + ComplexityScripts.QualityReport.run (args.headD ".lake/build/lib/lean") args[1]? diff --git a/scripts/test_tidy_sweep.py b/scripts/test_tidy_sweep.py index 07b9b6224a..7323547ad2 100644 --- a/scripts/test_tidy_sweep.py +++ b/scripts/test_tidy_sweep.py @@ -9,6 +9,7 @@ import sys import tempfile import unittest +from collections import defaultdict from types import SimpleNamespace sys.path.insert(0, str(pathlib.Path(__file__).resolve().parent)) @@ -76,11 +77,11 @@ def test_scopes_track_namespaces_and_opens(self) -> None: "theorem a : True := trivial\n\nend Cslib.Logic\n\nopen Foo in\n" "theorem b : True := trivial\n\ntheorem c : True := trivial\n") scopes = t.Scopes(masks(text)[1], t.namespaces_of([POLY + ".map", "Foo.x"])) - namespace, opens = scopes.at(text.index("theorem a")) - self.assertEqual(namespace, "Cslib.Logic") - self.assertEqual(opens, ("Turing.MultiTapeTM", POLY)) - self.assertEqual(scopes.at(text.index("theorem b")), ("", ("Foo",))) - self.assertEqual(scopes.at(text.index("theorem c")), ("", ())) + scope = scopes.at(text.index("theorem a")) + self.assertEqual(scope.namespace, "Cslib.Logic") + self.assertEqual([o.namespace for o in scope.opens], ["Turing.MultiTapeTM", POLY]) + self.assertEqual(scopes.at(text.index("theorem b")).opens, (t.Open("Foo"),)) + self.assertEqual(scopes.at(text.index("theorem c")), t.Scope("")) self.assertEqual(scopes.prefixes(text.index("theorem a"))[:3], ["Cslib.Logic", "Cslib", ""]) @@ -302,7 +303,7 @@ def test_reindent(self) -> None: def fake_source(text: str, namespaces: set[str]) -> t.SourceFile: src = object.__new__(t.SourceFile) - src.path = t.ROOT / "Fake.lean" + src.path = t.qr.source_path("M") src.text = text src.code, src.mask = masks(text) src.lines = text.split("\n") @@ -327,6 +328,7 @@ def fake_planner(text: str, constants: dict, known=(), privates=None, refs=()): p.sources = {src.path: src} p._refs = {"M": [t.Ref(n, a, b, None) for n, a, b in refs]} p._locals = {} + p._decl_spans = {} p.deferred = {} p.batch = {} p.reset() @@ -334,7 +336,8 @@ def fake_planner(text: str, constants: dict, known=(), privates=None, refs=()): class ConvertTests(unittest.TestCase): - def convert(self, text: str, sg, at: str = "X") -> tuple[str, str]: + def convert(self, text: str, sg, at: str | None = None) -> tuple[str, str]: + at = at or (".X" if ".X" in text else "X") p, src = fake_planner(text, {"X": {"m": "M", "sg": sg, "tidy": [POLY]}}, known={"Y"}) p.renames = {"X": "Y"} @@ -366,8 +369,9 @@ def test_leading_dot_with_a_plain_conclusion(self) -> None: start = src.text.index(".of_foo") self.assertTrue(p.convert(src.path, "M", start, start + 7, "N.of_foo", None, "tidy")) fe = p.files[src.path] + # The new name is written explicitly: see `ResolutionTests.test_dot_notation`. self.assertEqual(t.render(src.text, fe.replaces, fe.wraps, 0, len(src.text)), - " exact .of_bar (.of_tidy hc)") + " exact N.of_bar (.of_tidy hc)") self.assertTrue(t.spells(".of_foo", "N.of_foo")) def test_unconvertible_sites_stay_unchanged(self) -> None: @@ -375,7 +379,7 @@ def test_unconvertible_sites_stay_unchanged(self) -> None: blocks the referenced declaration, which is then deferred.""" cases = [(" map X", [[[0, 0]], 1], "partial"), (" simp [X]", [[[0, 0]], 1], "lemma list"), - (" exact .X a", [[[0, 0]], 1], "dot notation"), + (" exact .X a", [[[0, 0]], 1], "leading-dot"), (" X a", [[[0, 2]], 1], "binders"), (" X a", [[[1, 1], [0, 0]], 1], "implicit"), # The argument is tidy, but the conclusion is not a bare predicate. @@ -438,6 +442,80 @@ def test_stale_spans_are_not_edited(self) -> None: self.assertFalse(t.spells("", POLY)) +class CaptureTests(unittest.TestCase): + """Review 5636433742: section variables, aliases, notations, selective opens and the types + behind dot notation can capture a written name.""" + + def written(self, text: str, token: str, old: str, new: str, known=(), nth: int = 0): + start = -1 + for _ in range(nth + 1): + start = text.index(token, start + 1) + p, src = fake_planner(text, {old: {"m": "M"}, new: {"m": "M"}}, known, + refs=[(old, start, start + len(token))]) + return p.written("M", src, start, start + len(token), old, new)[0] + + def test_section_variables(self) -> None: + text = ("open N\n\nsection\n\nvariable (bar : Nat)\n\ndef before : Nat := foo\n\n" + "end\n\ndef later : Nat := foo\n") + self.assertEqual(self.written(text, "foo", "N.foo", "N.bar"), "N.bar") + # Outside the section the variable no longer binds `bar`. + self.assertEqual(self.written(text, "foo", "N.foo", "N.bar", nth=1), "bar") + self.assertEqual(t.binder_names(" {α : Type} (a b : ℕ) [Fintype α] [h : DecidableEq α]"), + {"α", "a", "b", "h"}) + + def test_aliases_and_notations(self) -> None: + for prefix in ("open M renaming baz → bar\n", "export M (bar)\n", + 'local notation "bar" => 0\n'): + text = prefix + "open N\n\ndef d : Nat := foo\n" + self.assertEqual(self.written(text, "foo", "N.foo", "N.bar"), "N.bar", prefix) + + def test_opens_that_do_not_surely_make_the_target_visible(self) -> None: + for line in ("open N (foo)", "open N hiding bar", "open scoped N"): + text = line + "\n\ndef d : Nat := N.foo\n" + self.assertEqual(self.written(text, "N.foo", "N.foo", "N.bar"), "N.bar", line) + # A selective open that lists the new name makes it visible. + text = "open N (foo bar)\n\ndef d : Nat := foo\n" + self.assertEqual(self.written(text, "foo", "N.foo", "N.bar", nth=1), "bar") + text = "open N (foo)\n\ndef d : Nat := foo\n" + self.assertEqual(self.written(text, "foo", "N.foo", "N.bar", nth=1), "N.bar") + + def test_names_outside_the_references_capture_too(self) -> None: + # `M.bar` exists in the import closure although nothing here refers to it. + text = "open M N\n\ndef d : Nat := foo\n" + self.assertEqual(self.written(text, "foo", "N.foo", "N.bar", known={"M.bar"}), "N.bar") + + def test_new_names_must_not_capture_other_references(self) -> None: + text = "open A B\n\ndef d : Nat := x + B.x + n.x\n" + spans = {"x ": "B.x", "B.x": "B.x", "x\n": "Nat.x"} + usages = defaultdict(list) + for token, name in spans.items(): + start = text.index(token) if token != "x\n" else text.index("n.x") + 2 + usages[name].append(("M", [2, start - text.index("def"), 2, + start - text.index("def") + len(token.strip())])) + p, src = fake_planner(text, {"A.y": {"m": "M"}}, known={"B.x", "Nat.x"}) + p.model.users = lambda name: usages.get(name, []) + p.model.referenced_by_last = lambda last: [n for n in usages if n.endswith("." + last)] + # Renaming `A.y` to `A.x` would make the bare `x` (now `B.x`) ambiguous. + found = p.captures("A.y", "A.x") + self.assertEqual(len(found), 1) + self.assertIn("could capture `x` (`B.x`)", found[0]) + # Without the bare and dotted references, the qualified `B.x` is safe. + usages["B.x"] = usages["B.x"][1:] + del usages["Nat.x"] + self.assertEqual(p.captures("A.y", "A.x"), []) + + def test_dot_notation(self) -> None: + # `abbrev W := Nat` with `W.bar`: `.bar` and `x.bar` would select `W.bar`, not `Nat.bar`. + known = {"W", "W.bar"} + self.assertEqual(self.written("def a : W := .foo\n", ".foo", "Nat.foo", "Nat.bar", + known), "Nat.bar") + self.assertIsNone(self.written("def a := (0 : W).foo\n", "foo", "Nat.foo", "Nat.bar", + known)) + # The tidy predicate's own namespace follows the restated type at the site. + self.assertEqual(self.written("example := hf.comp hg\n", "comp", POLY + ".comp", + PLAIN + ".comp"), "comp") + + class VerificationTests(unittest.TestCase): """Review 5635891057: verification is strict, reports failures and exits nonzero.""" @@ -503,11 +581,13 @@ def test_measurement_stubs_and_unchecked_rewrites_are_refused(self) -> None: contextlib.redirect_stderr(io.StringIO()) as err: for argv in (["rewrite", "--area", "Logics", "--stub-failures"], ["rewrite", "--area", "Logics", "--no-build-check"], + ["rewrite", "--area", "Logics", "--diff", "p.patch", "--verify"], ["report", "--registry", str(pathlib.Path(tmp) / "missing.json")]): with self.assertRaises(SystemExit, msg=argv) as raised: t.main(argv) self.assertEqual(raised.exception.code, 2) self.assertIn("--no-build-check is only for report", err.getvalue()) + self.assertIn("--diff previews without building", err.getvalue()) self.assertIn("registry file not found", err.getvalue()) diff --git a/scripts/tidy_sweep.py b/scripts/tidy_sweep.py index 3579348b6c..5810705a6b 100644 --- a/scripts/tidy_sweep.py +++ b/scripts/tidy_sweep.py @@ -60,6 +60,7 @@ from __future__ import annotations import argparse +import bisect import difflib import json import re @@ -353,6 +354,9 @@ def __init__(self, build_dir: Path, allowlist: set[str]): qr.collect_references(self.lib, self.decls, self.owners) qr.classify(self.decls) self.allowlist = allowlist + out = qr.run(["lake", "env", "lean", "--run", "scripts/QualityReport.lean", "--names", + *qr.ROOTS], capture_output=True).stdout + self.names = set(out.split()) self._users: dict[str, list[tuple[str, list]]] | None = None self._known: set[str] | None = None @@ -364,15 +368,22 @@ def users(self, name: str) -> list[tuple[str, list]]: for ref, _, info in self.lib.references(module): for usage in info["usages"]: self._users[ref].append((module, usage)) + self._by_last = defaultdict(list) + for ref in self._users: + self._by_last[ref.rsplit(".", 1)[-1]].append(ref) return self._users.get(name, []) + def referenced_by_last(self, last: str) -> list[str]: + """The referenced constants whose last component is `last`.""" + self.users("") + return self._by_last.get(last, []) + @property def known(self) -> set[str]: - """Every constant name the build defines or references, for name resolution.""" + """Every public constant and alias the three libraries can see (their import closure), + with the constants they define, for name resolution.""" if self._known is None: - self._known = set(self.constants) - for module in self.lib.ileans: - self._known.update(ref for ref, _, _ in self.lib.references(module)) + self._known = self.names | {n for n, c in self.constants.items() if c["e"]} return self._known @@ -656,7 +667,9 @@ def collapse(text: str) -> str: SCOPE_COMMAND = re.compile( r"^(?P(?:@\[[^\]\n]*\]\s*)?(?:(?:public|private|noncomputable|protected|meta)\s+)*)" - r"(?Pnamespace|section|end|open|mutual)\b(?P[^\n]*)", re.M) + r"(?Pnamespace|section|end|open|mutual|variable|export)\b", re.M) +NOTATION_NAME = re.compile( + r"^(?:@\[[^\]\n]*\]\s*)?(?:(?:local|scoped)\s+)?(?:notation3?|syntax|macro)\b[^\n]*", re.M) def namespaces_of(names) -> set[str]: @@ -669,64 +682,147 @@ def namespaces_of(names) -> set[str]: return out -class Scopes: - """The current namespace and opened namespaces at each offset of a masked source.""" +@dataclass(frozen=True) +class Open: + """An opened namespace: all of it, only the names `only` (`open N (x y)`), or all but the + names `hiding`.""" + namespace: str + only: frozenset[str] | None = None + hiding: frozenset[str] = frozenset() + + +@dataclass(frozen=True) +class Scope: + namespace: str + opens: tuple[Open, ...] = () + aliases: frozenset[str] = frozenset() # short names from `open … renaming` and `export` + variables: frozenset[str] = frozenset() # names bound by `variable` commands + + +def binder_names(text: str) -> set[str]: + """The names bound by the top-level binder groups of a `variable` command (masked).""" + names, i = set(), 0 + while i < len(text): + if text[i] in "([{⦃": + close = match_bracket(text, i) + if close < 0: + break + inner = text[i + 1:close] + colon = find_top_level(inner, 0, len(inner), ":") + if colon >= 0: + names.update(inner[:colon].split()) + elif text[i] != "[": + names.update(inner.split()) + i = close + 1 + else: + i += 1 + return {n for n in names if IDENT.fullmatch(n) and n != "_"} + - def __init__(self, mask: str, namespaces: set[str]): - self.points: list[tuple[int, str, tuple[str, ...]]] = [(0, "", ())] - self.once: list[tuple[int, int, tuple[str, ...]]] = [] - stack: list[tuple[str, str, list[str]]] = [] +class Scopes: + """The namespace, opened namespaces, aliases and section variables at each offset of a + masked source, and the identifier-like tokens its notations and macros declare.""" + + def __init__(self, mask: str, namespaces: set[str], text: str | None = None): + self.points: list[tuple[int, Scope]] = [(0, Scope(""))] + 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)] + self.notation: set[str] = set() + for m in NOTATION_NAME.finditer(text if text is not None else mask): + self.notation.update(re.findall(r'"([^\W\d][\w\'.]*)"', m[0])) + + def namespace() -> str: + return ".".join(f[1] for f in stack if f[0] == "namespace" and f[1]) + + def resolve(word: str, earlier: list[Open]) -> list[str]: + ns = namespace() + parts = ns.split(".") if ns else [] + prefixes = [".".join(parts[:i]) for i in range(len(parts), -1, -1)] + prefixes += [o.namespace for f in stack for o in f[2]] + prefixes += [o.namespace for o in earlier] + found = [p + "." + word if p else word for p in prefixes + if (p + "." + word if p else word) in namespaces] + return list(dict.fromkeys(found)) or [word] + for match in SCOPE_COMMAND.finditer(mask): - kw, rest = match["kw"], match["rest"].split() - namespace = ".".join(n for k, n, _ in stack if k == "namespace" and n) - opens = [o for _, _, os in stack for o in os] - if kw == "namespace" and rest: - stack.append(("namespace", rest[0], [])) + kw = match["kw"] + end = next((x for x in starts if x > match.start()), len(mask)) + rest = mask[match.end():end] + words = rest.split() + if kw == "namespace" and words: + stack.append(["namespace", words[0], [], set(), set()]) elif kw in ("section", "mutual"): - stack.append((kw, rest[0] if rest and kw == "section" else "", [])) + stack.append([kw, words[0] if words and kw == "section" else "", [], set(), + set()]) elif kw == "end": - if stack: + if len(stack) > 1: stack.pop() - elif kw == "open": - one_shot = bool(rest) and rest[-1] == "in" - words = [w for w in (rest[:-1] if one_shot else rest) - if w not in ("scoped", "hiding", "renaming", "→", "private") - and not w.startswith("(") and IDENT.fullmatch(w)] - resolved = [] - for word in words: - prefixes = [".".join(namespace.split(".")[:i]) - for i in range(len(namespace.split(".")), -1, -1)] if namespace \ - else [""] - found = [p + "." + word if p else word for p in prefixes + opens + resolved - if (p + "." + word if p else word) in namespaces] - resolved += found or [word] + elif kw == "variable": + stack[-1][4].update(binder_names(rest)) + elif kw in ("open", "export"): + one_shot = bool(words) and words[-1] == "in" + body = " ".join(words[:-1] if one_shot else words) + opens, aliases = self.parse_open(body, resolve, kw == "export") if one_shot: - after = next((s for s in starts if s > match.end()), len(mask)) - following = next((s for s in starts if s > after), len(mask)) - self.once.append((match.start(), following, tuple(resolved))) + following = next((x for x in starts if x > end), len(mask)) + self.once.append((match.start(), following, tuple(opens), + frozenset(aliases))) continue - if not stack: - stack.append(("file", "", [])) - stack[-1][2].extend(resolved) - namespace = ".".join(n for k, n, _ in stack if k == "namespace" and n) - opens = [o for _, _, os in stack for o in os] - self.points.append((match.end(), namespace, tuple(opens))) - - def at(self, offset: int) -> tuple[str, tuple[str, ...]]: - namespace, opens = "", () - for point, ns, os in self.points: - if point > offset: - break - namespace, opens = ns, os - extra = tuple(o for start, end, os in self.once if start <= offset < end for o in os) - return namespace, opens + extra + stack[-1][2].extend(opens) + stack[-1][3].update(aliases) + self.points.append((match.end(), Scope( + namespace(), tuple(o for f in stack for o in f[2]), + frozenset().union(*(f[3] for f in stack)), + frozenset().union(*(f[4] for f in stack))))) + self.offsets = [point for point, _ in self.points] + + @staticmethod + def parse_open(body: str, resolve, export: bool) -> tuple[list[Open], set[str]]: + """The namespaces an `open` (or `export`) command makes visible, and the short names it + introduces as aliases. `open scoped` opens no names.""" + words = body.replace("(", " ( ").replace(")", " ) ").replace(",", " ").split() + if not words or words[0] == "scoped": + return [], set() + if words[0] == "private": + words = words[1:] + if "renaming" in words: + pairs = words[words.index("renaming") + 1:] + return [], {pairs[i + 2] for i in range(len(pairs) - 2) if pairs[i + 1] == "→"} + if "hiding" in words: + k = words.index("hiding") + return [Open(ns, hiding=frozenset(words[k + 1:])) + for w in words[:k] for ns in resolve(w, [])], set() + if "(" in words: + k = words.index("(") + names = frozenset(w for w in words[k + 1:] if w != ")") + opens = [Open(ns, only=names) for w in words[:k] for ns in resolve(w, [])] + return ([] if export else opens), (set(names) if export else set()) + opens: list[Open] = [] + for w in words: # a later name may be relative to an earlier one + opens += [Open(ns) for ns in resolve(w, opens)] + return opens, set() + + def at(self, offset: int) -> Scope: + i = bisect.bisect_right(self.offsets, offset) - 1 + scope = self.points[i][1] if i >= 0 else Scope("") + for start, end, opens, aliases in self.once: + if start <= offset < end: + scope = Scope(scope.namespace, scope.opens + opens, scope.aliases | aliases, + scope.variables) + return scope + + def chain(self, offset: int) -> list[str]: + """The enclosing namespaces, innermost first, ending with the root `""`.""" + ns = self.at(offset).namespace + parts = ns.split(".") if ns else [] + return [".".join(parts[:i]) for i in range(len(parts), -1, -1)] def prefixes(self, offset: int) -> list[str]: - """Namespaces a written name may be relative to, innermost first (`""` is the root).""" - namespace, opens = self.at(offset) - parts = namespace.split(".") if namespace else [] - return [".".join(parts[:i]) for i in range(len(parts), -1, -1)] + list(opens) + """Namespaces a written name may be relative to, innermost first (`""` is the root); + selective opens count as whole ones (an over-approximation).""" + return self.chain(offset) + [o.namespace for o in self.at(offset).opens] def written_name(target: str, prefixes: list[str], known: set[str]) -> str: @@ -1009,7 +1105,7 @@ def __init__(self, path: Path, namespaces: set[str]): @property def scopes(self) -> Scopes: if self._scopes is None: - self._scopes = Scopes(self.mask, self._namespaces) + self._scopes = Scopes(self.mask, self._namespaces, self.text) return self._scopes def at(self, line: int, column16: int) -> int: @@ -1078,6 +1174,7 @@ def __init__(self, model: Model, entries: list[Entry], twins: dict[str, str], ar self.deferred: dict[str, list[str]] = {} self._refs: dict[str, list[Ref]] = {} self._locals: dict[tuple[str, int, int], set[str]] = {} + self._decl_spans: dict[str, list[tuple[int, int]]] = {} self.reset() def reset(self) -> None: @@ -1158,9 +1255,11 @@ def local_names(self, module: str, src: SourceFile, offset: int) -> set[str]: """Identifiers of the declaration (or command) around `offset` that are not references to constants: binders, local hypotheses, tactic names. A written name whose first component is one of them could be captured by a local.""" - ranges = self.model.lib.ileans.get(module, {}).get("decls", {}).values() - span = next(((src.at(r[0], r[1]), src.at(r[2], r[3])) for r in ranges - if src.at(r[0], r[1]) <= offset < src.at(r[2], r[3])), None) + if module not in self._decl_spans: + ranges = self.model.lib.ileans.get(module, {}).get("decls", {}).values() + self._decl_spans[module] = [(src.at(r[0], r[1]), src.at(r[2], r[3])) + for r in ranges] + span = next(((a, b) for a, b in self._decl_spans[module] if a <= offset < b), None) if span is None: starts = src.commands + [len(src.mask)] start = max([s for s in starts if s <= offset], default=0) @@ -1178,44 +1277,83 @@ def local_names(self, module: str, src: SourceFile, offset: int) -> set[str]: return self._locals[key] def resolves(self, module: str, src: SourceFile, offset: int, written: str) -> set[str]: - """What `written` (without `@`) can denote at `offset`: constants reached through the - enclosing namespaces and the opened namespaces, private constants of the module, and a - local of the same name (as `""`).""" - names = self.known | self.privates.get(module, set()) + """Everything `written` (without `@`) might denote at `offset`, over-approximated: + constants reached through the enclosing namespaces and every opened namespace (selective + and hiding opens counted whole), private constants of the module, and `""` when + its first component is a local binder, a section variable, an alias from + `open … renaming` or `export`, or a notation token. Names come from the whole import + closure, not only the referenced ones.""" + privates = self.privates.get(module, set()) + + def exists(name: str) -> bool: + return name in self.known or name in privates if written.startswith("_root_."): - return {written[len("_root_."):]} & names - hits = {p + "." + written if p else written for p in src.scopes.prefixes(offset)} - out = hits & names - if written.split(".")[0] in self.local_names(module, src, offset): + return {written[len("_root_."):]} if exists(written[len("_root_."):]) else set() + scope = src.scopes.at(offset) + out = {h for p in src.scopes.prefixes(offset) + for h in [p + "." + written if p else written] if exists(h)} + first = written.split(".")[0] + if first in self.local_names(module, src, offset) or first in scope.variables \ + or first in scope.aliases or first in src.scopes.notation: out.add("") return out + def reachable(self, src: SourceFile, offset: int, written: str, target: str) -> bool: + """Whether Lean surely looks `written` up as `target` at `offset`: through `_root_`, an + enclosing namespace, or an open that is not selective or hiding it.""" + if written.startswith("_root_."): + return written[len("_root_."):] == target + if any((p + "." + written if p else written) == target for p in src.scopes.chain(offset)): + return True + first = written.split(".")[0] + return any(o.namespace + "." + written == target and first not in o.hiding + and (o.only is None or written in o.only) for o in src.scopes.at(offset).opens) + + def write_name(self, module: str, src: SourceFile, offset: int, target: str, + first: str | None = None) -> str | None: + """The shortest written form of `target` that Lean surely resolves to it, and to nothing + else, at `offset` (`first` is tried before the suffixes), or None.""" + parts = target.split(".") + candidates = [first] + [".".join(parts[-k:]) for k in range(1, len(parts) + 1)] + for candidate in candidates + ["_root_." + target]: + if candidate and self.reachable(src, offset, candidate, target) \ + and self.resolves(module, src, offset, candidate) == {target}: + return candidate + return None + def written(self, module: str, src: SourceFile, start: int, end: int, old: str, new: str ) -> tuple[str | None, str]: """The text replacing the reference to `old` at `[start, end)` by one to `new`, or None - and the reason it cannot be written.""" + and the reason it cannot be written. + + Field and leading-dot notation resolve through the type of the receiver or the expected + type, which may be an abbreviation with declarations of its own, so their binding is not + established by names alone. They are kept only when the last component is unchanged and + the namespace changes with the tidy predicate itself (`ComputableTidilyInPolyTime.comp` + → `ComputableInPolyTime.comp`), the type at the site being restated alike. Otherwise a + leading-dot reference becomes an explicit name, and a field reference is not + rewritten.""" token = src.text[start:end] if not spells(token, old): return None, f"the reference span `{token}` does not spell `{old}`" if old == new: return token, "" leading = token.startswith(".") - if leading or (start and src.text[start - 1] == "."): # leading-dot or field notation - last = new.rsplit(".", 1)[-1] - if old.rsplit(".", 1)[-1] == last: + if leading or (start and src.text[start - 1] == "."): + if old.rsplit(".", 1)[-1] == new.rsplit(".", 1)[-1] \ + and namespace_of(new) == plain_name(namespace_of(old)) != namespace_of(old): return token, "" - if namespace_of(old) == namespace_of(new) and "." not in token.lstrip("."): - return ("." if leading else "") + last, "" - return None, "dot notation on a declaration whose namespace changes" + if leading: + name = self.write_name(module, src, start, new) + if name is not None: + return name, "" + return None, "field notation whose new binding cannot be established" at = "@" if token.startswith("@") else "" - candidates = [renamed_token(token.removeprefix("@"), old, new)] - parts = new.split(".") - candidates += [".".join(parts[-k:]) for k in range(1, len(parts) + 1)] - candidates.append("_root_." + new) - for candidate in candidates: - if candidate and self.resolves(module, src, start, candidate) == {new}: - return at + candidate, "" - return None, f"no written form of `{new}` resolves to it here" + name = self.write_name(module, src, start, new, + renamed_token(token.removeprefix("@"), old, new)) + if name is None: + return None, f"no written form of `{new}` surely resolves to it here" + return at + name, "" # Declarations. @@ -1286,8 +1424,33 @@ def analyse_decl(self, entry: Entry) -> dict | None: written = sum(1 for x in a["sig_refs"] if x.name in BY_TIDY) if not written or self.hidden_tidy(entry.name, src, dt, a["sig_refs"]): a["defer"].append("tidy predicate from a `variable` command or notation") + if not a["defer"] and entry.target != entry.name: + a["defer"] += self.captures(entry.name, entry.target)[:1] return a + def captures(self, old: str, new: str) -> list[str]: + """References to other constants that the new name `new` could capture: a written name + that would also resolve to `new` from its position, or a field or leading-dot reference + with the same last component (its binding depends on a type the text does not show).""" + out = [] + for other in self.model.referenced_by_last(new.rsplit(".", 1)[-1]): + if other in (old, new): + continue + for module, u in self.model.users(other): + path = qr.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("@") + if token.startswith("_root_."): + continue + dotted = token.startswith(".") or (start and src.text[start - 1] == ".") + if dotted or any((p + "." + token if p else token) == new + for p in src.scopes.prefixes(start)): + out.append(f"the new name `{new}` could capture `{token}` " + f"(`{other}`) at {self.where(path, start)}") + return out + return out + 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] @@ -1423,9 +1586,11 @@ def wrap_plan(self, entry: Entry, src: SourceFile, dt: DeclText, sig_refs: list[ problems.append("tidy hypothesis from a `variable` command or notation") if problems: return None, problems - prefixes = src.scopes.prefixes(dt.start) - iffs = ", ".join(written_name(n.iff, prefixes, self.known) - for n in self.notions_of(entry.name)) + iffs = [self.write_name(self.model.decls[entry.name]["module"], src, dt.assign, n.iff) + for n in self.notions_of(entry.name)] + if None in iffs: + return None, ["no written form of the plain ↔ tidy equivalence resolves here"] + iffs = ", ".join(iffs) body_column = column(src.text, dt.assign + 2) indent = line_indent(src.text, dt.sel_start) args = (body_column, indent, hyps, conclusion, simple, iffs) @@ -1897,6 +2062,11 @@ def main(argv: list[str] | None = None) -> int: parser.error(f"unknown area {area}; choose from {', '.join(AREA_ORDER)}") if args.command == "rewrite" and len(args.area) != 1: parser.error("rewrite needs exactly one --area") + if args.diff and args.verify: + parser.error("--diff previews without building; --verify rewrites and builds, so " + "choose one") + if args.diff and args.command != "rewrite": + parser.error("--diff is a rewrite option") if args.command == "rewrite" and args.no_build_check: parser.error("rewrite edits at the recorded reference spans, so it needs current build " "outputs; --no-build-check is only for report") From fc2f8a0cd6e8e4b96b27747cb3005c0a0e6bb904 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 00:13:55 -0400 Subject: [PATCH 04/10] fix(scripts): treat notation tokens as captures of written names Addresses review 5636686550 and reply 4365874664 on #666. Lean's tokenizer reads a declared token instead of an identifier no longer than it, so a short replacement name can bind to a notation: - `QualityReport.lean --names` also prints the parser tokens of the import closure (global and scoped notations, syntax and macros), read from the parser extension's module entries. - A module's own notation, syntax and macro commands contribute the string literals of the whole command, across continuation lines. - The resolver rejects a written form when such a token matches at least the identifier Lean would read there. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- scripts/QualityReport.lean | 17 ++++++-- scripts/test_tidy_sweep.py | 35 +++++++++++++-- scripts/tidy_sweep.py | 88 ++++++++++++++++++++++++++++---------- 3 files changed, 111 insertions(+), 29 deletions(-) diff --git a/scripts/QualityReport.lean b/scripts/QualityReport.lean index 3adb97a7a2..9a53f95ee6 100644 --- a/scripts/QualityReport.lean +++ b/scripts/QualityReport.lean @@ -37,8 +37,9 @@ flag `1` when the type is an application of a listed tidy predicate, `2` when it constant otherwise, and `0` when it mentions none. Run as `lake env lean --run scripts/QualityReport.lean --names ...`, it instead prints -every name the given modules and their transitive imports export: constants and `export` aliases, -one per line, for the name resolution of `scripts/tidy_sweep.py`. +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`. It then prints `{"dup": [...], "k": ...}` lines grouping exported constants of different modules whose types are alpha-equivalent (`k = "thm"`), or whose types and exposed bodies are @@ -202,7 +203,7 @@ unsafe def run (libDir : System.FilePath) (pairs : Option String := none) : IO U if regions.isEmpty then stdout.flush /-- Print the exported constants and `export` aliases of `roots` and their transitive imports, -found through the search path that `lake env` sets. -/ +found through the search path that `lake env` sets, then `--tokens--` and their parser tokens. -/ unsafe def names (roots : List Name) : IO Unit := do initSearchPath (← findSysroot) let stdout ← IO.getStdout @@ -210,6 +211,7 @@ unsafe def names (roots : List Name) : IO Unit := do let mut todo := roots.toArray -- The mapped regions stay alive until the end of the program. let mut regions : Array CompactedRegion := #[] + let mut tokens : Std.HashSet String := {} while h : todo.size > 0 do let mod := todo.back todo := todo.pop @@ -225,6 +227,15 @@ unsafe def names (roots : List Name) : IO Unit := do if ext == `Lean.aliasExtension then for e in es do stdout.putStrLn (unsafeCast e : Name × Name).1.toString + if ext == `Lean.Parser.parserExtension then + for e in es do + let entry := + match (unsafeCast e : ScopedEnvExtension.Entry Parser.ParserExtension.OLeanEntry) with + | .global a => a + | .scoped _ a => a + if let .token t := entry then tokens := tokens.insert t + stdout.putStrLn "--tokens--" + for t in tokens do stdout.putStrLn t if regions.isEmpty then stdout.flush end ComplexityScripts.QualityReport diff --git a/scripts/test_tidy_sweep.py b/scripts/test_tidy_sweep.py index 7323547ad2..08cafed240 100644 --- a/scripts/test_tidy_sweep.py +++ b/scripts/test_tidy_sweep.py @@ -315,8 +315,8 @@ def fake_source(text: str, namespaces: set[str]) -> t.SourceFile: return src -def fake_planner(text: str, constants: dict, known=(), privates=None, refs=()): - """A planner over one source `Fake.lean` (module `M`) without a build.""" +def fake_planner(text: str, constants: dict, known=(), privates=None, refs=(), tokens=()): + """A planner over one source (module `M`) without a build; `tokens` are imported.""" p = object.__new__(t.Planner) p.model = SimpleNamespace(constants=constants, owners={}, lib=SimpleNamespace(ileans={})) @@ -329,6 +329,7 @@ def fake_planner(text: str, constants: dict, known=(), privates=None, refs=()): p._refs = {"M": [t.Ref(n, a, b, None) for n, a, b in refs]} p._locals = {} p._decl_spans = {} + p.tokens = t.by_first(tokens) p.deferred = {} p.batch = {} p.reset() @@ -446,12 +447,13 @@ class CaptureTests(unittest.TestCase): """Review 5636433742: section variables, aliases, notations, selective opens and the types behind dot notation can capture a written name.""" - def written(self, text: str, token: str, old: str, new: str, known=(), nth: int = 0): + def written(self, text: str, token: str, old: str, new: str, known=(), nth: int = 0, + tokens=()): start = -1 for _ in range(nth + 1): start = text.index(token, start + 1) p, src = fake_planner(text, {old: {"m": "M"}, new: {"m": "M"}}, known, - refs=[(old, start, start + len(token))]) + refs=[(old, start, start + len(token))], tokens=tokens) return p.written("M", src, start, start + len(token), old, new)[0] def test_section_variables(self) -> None: @@ -469,6 +471,31 @@ def test_aliases_and_notations(self) -> None: text = prefix + "open N\n\ndef d : Nat := foo\n" self.assertEqual(self.written(text, "foo", "N.foo", "N.bar"), "N.bar", prefix) + def test_multiline_notation(self) -> None: + """Review 5636686550: the notation's token is on a continuation line.""" + text = ("namespace N\ndef foo : Nat := 1\ndef bar : Nat := 2\nend N\nopen N\n" + 'local notation\n "bar" => (3 : Nat)\n' + "def before : Nat := foo\ndef after : Nat := foo\n") + self.assertEqual(self.written(text, "foo", "N.foo", "N.bar", nth=2), "N.bar") + self.assertEqual(t.notation_tokens(text, masks(text)[1]), {"bar"}) + + def test_imported_notation(self) -> None: + """Reply 4365874664: `notation "bar" => (3 : Nat)` in a dependency.""" + text = "open N\ndef before : Nat := foo\ndef after : Nat := foo\n" + self.assertEqual(self.written(text, "foo", "N.foo", "N.bar", nth=1, tokens={"bar"}), + "N.bar") + self.assertEqual(self.written(text, "foo", "N.foo", "N.bar", nth=1), "bar") + + def test_tokens_win_over_identifiers_no_longer_than_them(self) -> None: + tokens = t.by_first({"bar", "ba", "barx.y", "∑"}) + self.assertEqual(t.token_capture("bar", " + 1", tokens), "bar") + self.assertIsNone(t.token_capture("bars", "", tokens)) # the identifier is longer + self.assertIsNone(t.token_capture("bar", ".baz", tokens)) # `bar.baz` is longer + self.assertEqual(t.token_capture("barx", ".y z", tokens), "barx.y") + text = ('infixl:65 " ⊕⊕ " => f\nmacro "qq" x:term : term => `($x)\n' + 'syntax (name := s) "ss"\n "tt" : tactic\ndef x := "notatoken"\n') + self.assertEqual(t.notation_tokens(text, masks(text)[1]), {"⊕⊕", "qq", "ss", "tt"}) + def test_opens_that_do_not_surely_make_the_target_visible(self) -> None: for line in ("open N (foo)", "open N hiding bar", "open scoped N"): text = line + "\n\ndef d : Nat := N.foo\n" diff --git a/scripts/tidy_sweep.py b/scripts/tidy_sweep.py index 5810705a6b..5703468db0 100644 --- a/scripts/tidy_sweep.py +++ b/scripts/tidy_sweep.py @@ -32,8 +32,11 @@ in the three libraries, at the exact ranges recorded in the `.ilean` files (full names, names relative to namespaces and `open`s, dot notation), and in comments and READMEs. No edit is made at a span whose text does not spell the referenced constant, and a replacement name is written -only if it resolves to its target, and nothing else, from its position (namespaces, `open`s, -private names of the module, local binders); `rewrite` therefore needs current build outputs. +only if Lean surely resolves it to its target, and nothing else could bind it, from its position: +namespaces and `open`s by kind, every constant and alias of the import closure, private names of +the module, local binders, section variables, renaming and `export` aliases, and the notation, +syntax and macro tokens of the import closure and the module. `rewrite` therefore needs current +build outputs. A declaration is *deferred* (left tidy, with its references unchanged) when its statement names another tidy declaration, gets a tidy hypothesis from a `variable` command, or is written inside @@ -356,7 +359,8 @@ def __init__(self, build_dir: Path, allowlist: set[str]): self.allowlist = allowlist out = qr.run(["lake", "env", "lean", "--run", "scripts/QualityReport.lean", "--names", *qr.ROOTS], capture_output=True).stdout - self.names = set(out.split()) + 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 self._known: set[str] | None = None @@ -668,8 +672,41 @@ def collapse(text: str) -> str: SCOPE_COMMAND = re.compile( r"^(?P(?:@\[[^\]\n]*\]\s*)?(?:(?:public|private|noncomputable|protected|meta)\s+)*)" r"(?Pnamespace|section|end|open|mutual|variable|export)\b", re.M) -NOTATION_NAME = re.compile( - r"^(?:@\[[^\]\n]*\]\s*)?(?:(?:local|scoped)\s+)?(?:notation3?|syntax|macro)\b[^\n]*", re.M) +NOTATION_COMMAND = re.compile( + r"(?:@\[[^\]\n]*\]\s*)*(?:(?:local|scoped|private|public|meta)\s+)*" + r"(?:notation3?|infixl?|infixr|prefix|postfix|syntax|macro|elab|binder_predicate)\b") +STRING_LITERAL = re.compile(r'"((?:[^"\\\n]|\\.)*)"') + + +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)] + tokens = set() + for start, end in zip(starts, starts[1:]): + if NOTATION_COMMAND.match(mask, start): + tokens.update(t.strip() for t in STRING_LITERAL.findall(text, start, end)) + return tokens - {""} + + +def token_capture(written: str, following: str, tokens) -> str | None: + """A token that Lean's tokenizer reads instead of the identifier `written` followed by + `following`: a token wins over an identifier at least as short as it. `tokens` maps first + characters to tokens.""" + text = written + following + lexeme = IDENT.match(text) + length = lexeme.end() if lexeme else len(written) + for token in tokens.get(written[:1], ()): + if len(token) >= length and text.startswith(token): + return token + return None + + +def by_first(tokens) -> dict[str, list[str]]: + out: dict[str, list[str]] = defaultdict(list) + for token in tokens: + out[token[:1]].append(token) + return out def namespaces_of(names) -> set[str]: @@ -721,7 +758,7 @@ def binder_names(text: str) -> set[str]: class Scopes: """The namespace, opened namespaces, aliases and section variables at each offset of a - masked source, and the identifier-like tokens its notations and macros declare.""" + masked source, and the tokens its notations, syntax and macros declare.""" def __init__(self, mask: str, namespaces: set[str], text: str | None = None): self.points: list[tuple[int, Scope]] = [(0, Scope(""))] @@ -729,9 +766,7 @@ def __init__(self, mask: str, namespaces: set[str], text: str | None = None): # 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)] - self.notation: set[str] = set() - for m in NOTATION_NAME.finditer(text if text is not None else mask): - self.notation.update(re.findall(r'"([^\W\d][\w\'.]*)"', m[0])) + self.tokens = by_first(notation_tokens(text if text is not None else mask, mask)) def namespace() -> str: return ".".join(f[1] for f in stack if f[0] == "namespace" and f[1]) @@ -1175,6 +1210,7 @@ def __init__(self, model: Model, entries: list[Entry], twins: dict[str, str], ar self._refs: dict[str, list[Ref]] = {} self._locals: dict[tuple[str, int, int], set[str]] = {} self._decl_spans: dict[str, list[tuple[int, int]]] = {} + self.tokens = by_first(model.tokens) self.reset() def reset(self) -> None: @@ -1276,12 +1312,15 @@ def local_names(self, module: str, src: SourceFile, offset: int) -> set[str]: self._locals[key] = names - KEYWORDS return self._locals[key] - def resolves(self, module: str, src: SourceFile, offset: int, written: str) -> set[str]: - """Everything `written` (without `@`) might denote at `offset`, over-approximated: - constants reached through the enclosing namespaces and every opened namespace (selective - and hiding opens counted whole), private constants of the module, and `""` when - its first component is a local binder, a section variable, an alias from - `open … renaming` or `export`, or a notation token. Names come from the whole import + def resolves(self, module: str, src: SourceFile, offset: int, written: str, + following: str = "") -> set[str]: + """Everything `written` (without `@`, followed by `following`) might denote at + `offset`, over-approximated: constants reached through the enclosing namespaces and + every opened namespace (selective and hiding opens counted whole), private constants of + the module, `""` when its first component is a local binder, a section variable + or an alias from `open … renaming` or `export`, and `""` when the tokenizer would + read a notation, syntax or macro token there instead (from the import closure, scoped + ones included, or from the module's own commands). Names come from the whole import closure, not only the referenced ones.""" privates = self.privates.get(module, set()) @@ -1294,8 +1333,11 @@ def exists(name: str) -> bool: for h in [p + "." + written if p else written] if exists(h)} first = written.split(".")[0] if first in self.local_names(module, src, offset) or first in scope.variables \ - or first in scope.aliases or first in src.scopes.notation: + or first in scope.aliases: out.add("") + if token_capture(written, following, self.tokens) \ + or token_capture(written, following, src.scopes.tokens): + out.add("") return out def reachable(self, src: SourceFile, offset: int, written: str, target: str) -> bool: @@ -1310,14 +1352,15 @@ def reachable(self, src: SourceFile, offset: int, written: str, target: str) -> and (o.only is None or written in o.only) for o in src.scopes.at(offset).opens) def write_name(self, module: str, src: SourceFile, offset: int, target: str, - first: str | None = None) -> str | None: - """The shortest written form of `target` that Lean surely resolves to it, and to nothing - else, at `offset` (`first` is tried before the suffixes), or None.""" + first: str | None = None, following: str = "") -> str | None: + """The shortest written form of `target`, followed by `following`, that Lean surely + resolves to it, and to nothing else, at `offset` (`first` is tried before the + suffixes), or None.""" parts = target.split(".") candidates = [first] + [".".join(parts[-k:]) for k in range(1, len(parts) + 1)] for candidate in candidates + ["_root_." + target]: if candidate and self.reachable(src, offset, candidate, target) \ - and self.resolves(module, src, offset, candidate) == {target}: + and self.resolves(module, src, offset, candidate, following) == {target}: return candidate return None @@ -1344,13 +1387,14 @@ def written(self, module: str, src: SourceFile, start: int, end: int, old: str, and namespace_of(new) == plain_name(namespace_of(old)) != namespace_of(old): return token, "" if leading: - name = self.write_name(module, src, start, new) + name = self.write_name(module, src, start, new, None, src.text[end:end + 200]) if name is not None: return name, "" return None, "field notation whose new binding cannot be established" at = "@" if token.startswith("@") else "" name = self.write_name(module, src, start, new, - renamed_token(token.removeprefix("@"), old, new)) + renamed_token(token.removeprefix("@"), old, new), + src.text[end:end + 200]) if name is None: return None, f"no written form of `{new}` surely resolves to it here" return at + name, "" From 5c33ecded9985261a480ac71c034b11b78e2be05 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 00:17:05 -0400 Subject: [PATCH 05/10] feat(scripts): let the tidy sweep report on a partial build A staging tree may not build completely (the S1 canonical-source cutover is staged machine layer first). `report --partial` loads the outputs of the modules the roots' sources import that were built, lists the others per area, and analyses the rest. Loading stays strict by default, and `rewrite` refuses partial outputs. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- scripts/quality_report.py | 31 +++++++++++++++++++++++++++---- scripts/test_tidy_sweep.py | 25 +++++++++++++++++++++++++ scripts/tidy_sweep.py | 35 +++++++++++++++++++++++++---------- 3 files changed, 77 insertions(+), 14 deletions(-) diff --git a/scripts/quality_report.py b/scripts/quality_report.py index c5e70f31db..02113f0407 100644 --- a/scripts/quality_report.py +++ b/scripts/quality_report.py @@ -398,13 +398,35 @@ def check_outputs(build_dir: Path, skip: bool, current=lake_outputs_current, return "checked identical to the current outputs of `lake build --no-build`" -def load_ileans(build_dir: Path) -> dict[str, dict]: +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) -> 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. Every root and every module they import must have - one; a missing file means the build is incomplete. The roots themselves are left out.""" + one; a missing file means the build is incomplete. The 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: + for module in listed_modules(source_path(root).read_text()): + 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 = {}, [(root, None) for root in ROOTS] while todo: module, importer = todo.pop() @@ -467,8 +489,9 @@ def offset(self, line0: int, index: int) -> int: class Library: """Build outputs and sources of the three libraries, loaded lazily where possible.""" - def __init__(self, build_dir: Path, pairs: str | None = None): - self.ileans = load_ileans(build_dir) + def __init__(self, build_dir: Path, pairs: str | None = None, + missing: list[str] | None = None): + 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] = {} diff --git a/scripts/test_tidy_sweep.py b/scripts/test_tidy_sweep.py index 08cafed240..4a568bd075 100644 --- a/scripts/test_tidy_sweep.py +++ b/scripts/test_tidy_sweep.py @@ -641,6 +641,31 @@ def test_module_paths(self) -> None: "ComplexityAbstracts.X") +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"]) + with tempfile.TemporaryDirectory() as tmp: + build = pathlib.Path(tmp) + listed = t.qr.listed_modules(t.qr.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) + self.assertEqual(list(ileans), [present]) + self.assertIn(listed[1], missing) + with self.assertRaises(SystemExit): # strict by default + t.qr.load_ileans(build) + + def test_rewrite_refuses_partial_builds(self) -> None: + with contextlib.redirect_stderr(io.StringIO()) as err, self.assertRaises(SystemExit): + t.main(["rewrite", "--area", "Logics", "--partial"]) + self.assertIn("--partial is only for report", err.getvalue()) + + class SummaryTests(unittest.TestCase): def test_counts_by_area_and_case(self) -> None: entries = [t.Entry("a", "M", "p", "Logics", "theorem", "2"), diff --git a/scripts/tidy_sweep.py b/scripts/tidy_sweep.py index 5703468db0..0e02b8630c 100644 --- a/scripts/tidy_sweep.py +++ b/scripts/tidy_sweep.py @@ -348,17 +348,19 @@ def registry_problems(registry: dict[str, str], constants: dict[str, dict]) -> l class Model: """Declarations, constants and references of the built libraries.""" - def __init__(self, build_dir: Path, allowlist: set[str]): + def __init__(self, build_dir: Path, allowlist: set[str], partial: bool = False): pairs = ",".join(f"{n.tidy}={n.plain}" for n in NOTIONS) - self.lib = qr.Library(build_dir, pairs) + self.missing: list[str] | None = [] if partial else None + self.lib = qr.Library(build_dir, pairs, self.missing) 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.allowlist = allowlist + roots = sorted(self.lib.ileans) if partial else qr.ROOTS out = qr.run(["lake", "env", "lean", "--run", "scripts/QualityReport.lean", "--names", - *qr.ROOTS], capture_output=True).stdout + *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 @@ -419,10 +421,17 @@ def markdown_report(report: dict, limit: int = 40) -> str: if report["registry"] else "") out = [f"Revision `{report['revision']}`{dirty}; build outputs {report['outputs']}. " f"Allowlist: {report['allowlist_size']} modules. Plain twins of tidy theorems: " - f"{twins}{registry}.", "", - "### Public declarations whose statement mentions a tidy predicate", "", - "| Area | Total | (1) Plain twin | (2) Rename and restate | " - "(3) Definition or field | Unclassifiable |", "|---|--:|--:|--:|--:|--:|"] + 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) + 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()) + + "). Their declarations, and references from them, are missing below.", ""] + out += ["### Public declarations whose statement mentions a tidy predicate", "", + "| Area | Total | (1) Plain twin | (2) Rename and restate | " + "(3) Definition or field | Unclassifiable |", "|---|--:|--:|--:|--:|--:|"] for area, c in list(s["areas"].items()) + [("Total", s["total"])]: out.append(f"| {area} | {c.get('total', 0):,} | {c.get('1', 0):,} | {c.get('2', 0):,} | " f"{c.get('3', 0):,} | {c.get('unclassifiable', 0):,} |") @@ -2091,6 +2100,9 @@ def main(argv: list[str] | None = None) -> int: parser.add_argument("--build-dir", type=Path, default=qr.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", + help="report only: accept a partial build (a tree that does not build " + "completely); modules without outputs are listed, not analysed") parser.add_argument("--json", type=Path, help="write the full report as JSON") parser.add_argument("--markdown", type=Path, help="write the report as Markdown") parser.add_argument("--no-plan", action="store_true", help="report: skip rewrite plans") @@ -2111,6 +2123,8 @@ def main(argv: list[str] | None = None) -> int: "choose one") if args.diff and args.command != "rewrite": parser.error("--diff is a rewrite option") + if args.command == "rewrite" and args.partial: + parser.error("rewrite needs complete build outputs; --partial is only for report") if args.command == "rewrite" and args.no_build_check: parser.error("rewrite edits at the recorded reference spans, so it needs current build " "outputs; --no-build-check is only for report") @@ -2118,8 +2132,8 @@ def main(argv: list[str] | None = None) -> int: registry = load_registry(args.registry) except ValueError as error: parser.error(str(error)) - outputs = qr.check_outputs(args.build_dir, args.no_build_check) - model = Model(args.build_dir, load_allowlist(args.allowlist)) + outputs = qr.check_outputs(args.build_dir, args.no_build_check or args.partial) + model = Model(args.build_dir, load_allowlist(args.allowlist), args.partial) 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] @@ -2132,7 +2146,8 @@ def main(argv: list[str] | None = None) -> int: "registry_size": len(registry), "twins": dict(Counter(kind for _, kind in twins.values())), "registry_problems": registry_problems(registry, model.constants), - "summary": summary(shown), "entries": [entry_json(e) for e in shown]} + "summary": summary(shown), "entries": [entry_json(e) for e in shown], + "missing": model.missing} plain_twins = {o: p for o, (p, _) in twins.items()} plans = [] if args.command == "rewrite" and args.diff: From 83549a7b34776b4f167bee1ede6ed7c1147593ed Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 00:40:22 -0400 Subject: [PATCH 06/10] feat(scripts): restore the scoped local transition as a verify repair Following Samuel's clarification on #456 (tidy is fine anywhere inside proofs, never in statements or public types), `rewrite --verify` again precedes a failing wrapped proof or client declaration with `attribute [local fun_prop] ComputableInPolyTime.tidy in`, written through the checked resolver, and reports those declarations for information as plain-calculus gaps. Anonymous commands are located by their first lines. Also: lines the rewrite pushes past 100 characters are listed for reflowing, and `report --partial` checks that every loaded module's outputs are current. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- scripts/test_tidy_sweep.py | 66 +++++++++++++- scripts/tidy_sweep.py | 174 ++++++++++++++++++++++++++++++++----- 2 files changed, 218 insertions(+), 22 deletions(-) diff --git a/scripts/test_tidy_sweep.py b/scripts/test_tidy_sweep.py index 4a568bd075..9ca449057e 100644 --- a/scripts/test_tidy_sweep.py +++ b/scripts/test_tidy_sweep.py @@ -253,6 +253,11 @@ def test_nested_wraps_render_inside_out(self) -> None: reps = [t.Replace(3, 4, "Y")] self.assertEqual(t.render(text, reps, wraps, 0, len(text)), "f (.of_tidy (Y a).tidy) b") + def test_new_long_lines_are_reported(self) -> None: + old = "a\n" + "x" * 120 + "\nshort\n" + new = "a\n" + "x" * 120 + "\n" + "y" * 101 + "\n" + self.assertEqual(t.long_lines(old, new), [3]) + def test_regions_transform_their_edited_text(self) -> None: text = "a := X\nb" out = t.apply_edits(text, [t.Replace(5, 6, "Y")], [], @@ -331,6 +336,7 @@ def fake_planner(text: str, constants: dict, known=(), privates=None, refs=(), t p._decl_spans = {} p.tokens = t.by_first(tokens) p.deferred = {} + p.bridge = frozenset() p.batch = {} p.reset() return p, src @@ -556,7 +562,7 @@ def runner(cmd, **_): self.assertEqual(calls, [["lake", "build", "--wfail", "--iofail", "Complexity"]]) def check(self, output: str, code: int) -> dict: - planner = SimpleNamespace(decls={}, force_wrap=frozenset()) + planner = SimpleNamespace(decls={}, force_wrap=frozenset(), bridged=[]) return t.check_build(planner, {}, output, code, 1) def test_status_is_passed_only_without_errors(self) -> None: @@ -574,7 +580,7 @@ def test_rewrite_writes_reports_and_fails_honestly(self) -> None: class FakePlanner: def __init__(self, *args): - self.decls, self.force_wrap = {}, frozenset() + self.decls, self.force_wrap, self.bridged = {}, frozenset(), [] def plan(self): return self @@ -603,6 +609,51 @@ def build(_): "manual": {}}, "manual": [], "build": result})) self.assertEqual(t.exit_status([{"build": None}]), 0) + def test_failing_clients_get_the_local_transition(self) -> None: + """A client whose tidy `fun_prop` used a restated lemma is preceded by + `attribute [local fun_prop] ComputableInPolyTime.tidy in` in the next round.""" + rounds = [] + + class FakePlanner: + def __init__(self, model, entries, twins, area, force, bridge): + self.decls, self.force_wrap, self.bridged = {}, force, sorted(bridge) + rounds.append(bridge) + + def plan(self): + return self + + def render(self): + return {} + + def build(_): + if len(rounds) == 1: + return 1, "error: Complexity/C.lean:3:2: `fun_prop` was unable to prove\n" + return 0, "" + original, client = t.Planner, t.client_decl + t.Planner = FakePlanner + t.client_decl = lambda *args: ("Complexity.C", "C.lemma") + try: + _, result = t.rewrite(SimpleNamespace(decls={}), [], {}, "Logics", True, 3, build) + finally: + t.Planner, t.client_decl = original, client + self.assertEqual(rounds, [frozenset(), frozenset({("Complexity.C", "C.lemma")})]) + self.assertEqual(result["status"], "passed") + self.assertEqual(result["bridged"], [("Complexity.C", "C.lemma")]) + + def test_transition_is_inserted_with_a_checked_name(self) -> None: + text = ("namespace Turing.MultiTapeTM\n\n/-- doc -/\n@[fun_prop]\n" + "theorem c : True := by\n fun_prop\n\nend Turing.MultiTapeTM\n") + decl_line = text.split("\n").index("/-- doc -/") + p, src = fake_planner(text, {"T": {"m": "M", "tidy": [POLY]}}, known={PLAIN + ".tidy"}) + p.renames = {"T": "U"} + p.bridge = frozenset({("M", f"line:{decl_line + 2}")}) + p.plan_bridges() + fe = p.files[src.path] + out = t.render(text, fe.replaces, fe.wraps, 0, len(text)) + self.assertIn("\nattribute [local fun_prop] ComputableInPolyTime.tidy in\n/-- doc -/", + out) + self.assertEqual(t.command_start_line(src, decl_line + 2), decl_line) + def test_measurement_stubs_and_unchecked_rewrites_are_refused(self) -> None: with tempfile.TemporaryDirectory() as tmp, \ contextlib.redirect_stderr(io.StringIO()) as err: @@ -660,6 +711,17 @@ def test_partial_outputs_are_listed(self) -> None: with self.assertRaises(SystemExit): # strict by default t.qr.load_ileans(build) + def test_partial_outputs_must_be_current(self) -> None: + calls = [] + + def runner(cmd, **_): + calls.append(cmd) + return SimpleNamespace(returncode=calls[-1][-1] == "Stale") + t.check_partial_outputs(["A", "B"], runner) + with self.assertRaises(SystemExit): + t.check_partial_outputs(["A", "Stale"], runner) + self.assertEqual(calls[0], ["lake", "build", "--no-build", "A", "B"]) + def test_rewrite_refuses_partial_builds(self) -> None: with contextlib.redirect_stderr(io.StringIO()) as err, self.assertRaises(SystemExit): t.main(["rewrite", "--area", "Logics", "--partial"]) diff --git a/scripts/tidy_sweep.py b/scripts/tidy_sweep.py index 0e02b8630c..bc06c3c429 100644 --- a/scripts/tidy_sweep.py +++ b/scripts/tidy_sweep.py @@ -4,7 +4,7 @@ Usage: python3 scripts/tidy_sweep.py report [--area AREA]... [--json OUT] [--markdown OUT] python3 scripts/tidy_sweep.py rewrite --area AREA [--diff OUT | --verify [--rounds N]] Common options: [--registry FILE] [--allowlist FILE] [--build-dir DIR]; report also accepts -[--no-build-check] and [--no-plan]. +[--no-build-check], [--partial] and [--no-plan]. Plain computability is the API and tidy computability is how the machine layer proves it: outside the raw machine constructions of the allowlist (`scripts/tidy_allowlist.txt`, from #608), no @@ -49,11 +49,15 @@ `(lemma args).tidy`, with `.of_tidy` around tidy arguments; references to case 1 originals stay there, and the plan counts them. `.of_tidy (x.tidy)` round trips are then removed. -With `--verify`, the three libraries are built strictly (`--wfail --iofail`) after the rewrite; a -translated proof that fails is wrapped instead and the build repeated. Failures that remain, such -as a tidy `fun_prop` that relied on a lemma the batch made plain, mark plain-calculus gaps: they -are reported, the status is `failed` and the exit code nonzero. `--diff` writes the plan as a -patch instead of rewriting files. +With `--verify`, the three libraries are built strictly (`--wfail --iofail`) after the rewrite, +and repaired and rebuilt a few times: a translated proof that fails is wrapped instead, and a +wrapped proof or another declaration that fails (typically a tidy `fun_prop` that used a lemma +the batch made plain) is preceded by `attribute [local fun_prop] ComputableInPolyTime.tidy in`. +Tidy reasoning inside proofs is fine; the report lists these declarations for information, as +gaps of the plain calculus. Failures that remain are reported, the status is `failed` and the +exit code nonzero. Lines the rewrite pushes past 100 characters are listed for reflowing. +`--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 @@ -345,13 +349,25 @@ def registry_problems(registry: dict[str, str], constants: dict[str, dict]) -> l # --- Loading ------------------------------------------------------------------------------------ +def check_partial_outputs(modules: list[str], runner=subprocess.run) -> None: + """Exit unless Lake finds the outputs of the given (built) modules current.""" + check = runner(["lake", "build", "--no-build", *modules], cwd=ROOT, capture_output=True, + 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") + + class Model: """Declarations, constants and references of the built libraries.""" - def __init__(self, build_dir: Path, allowlist: set[str], partial: bool = False): + 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) + 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) @@ -1206,8 +1222,10 @@ class Planner: (left tidy), so that skipped references stay unchanged.""" def __init__(self, model: Model, entries: list[Entry], twins: dict[str, str], area: str, - force_wrap: frozenset[str] = frozenset()): + force_wrap: frozenset[str] = frozenset(), + bridge: frozenset[tuple[str, str]] = frozenset()): self.model, self.area, self.force_wrap = model, area, force_wrap + self.bridge = bridge self.entries = {e.name: e for e in entries} self.batch = {e.name: e for e in entries if e.area == area and e.case == "2"} self.twins = {o: p for o, p in twins.items() if p in model.constants} @@ -1234,6 +1252,7 @@ def reset(self) -> None: self.twin_refs: Counter = Counter() self.imports: list[tuple[str, str, bool]] = [] self.blockers: dict[str, list[str]] = defaultdict(list) + self.bridged: list[str] = [] self.round_trips = 0 # Sources and references. @@ -1430,6 +1449,7 @@ def plan(self) -> "Planner": self.deferred[name] = sorted(set(reasons)) for name in sorted(self.deferred): self.defer(name, analyses.get(name)) + self.plan_bridges() self.plan_comments() self.plan_imports() return self @@ -1504,6 +1524,40 @@ def captures(self, old: str, new: str) -> list[str]: return out return out + def plan_bridges(self) -> None: + """Precede the declarations of `bridge` (a module and a declaration name, or `line:N` + for the 0-based line of an anonymous command) by + `attribute [local fun_prop] ComputableInPolyTime.tidy in`: their tidy `fun_prop` calls + may then use restated plain certificates. Tidy reasoning stays inside proofs; needing + this marks a gap in the plain calculus.""" + notions = {n for name in self.renames for n in self.notions_of(name)} + for module, name in sorted(self.bridge): + if name in self.deferred: + continue + path = qr.source_path(module) + src = self.source(path) + ranges = self.model.lib.ileans.get(module, {}).get("decls", {}) + if name.startswith("line:"): + start = src.starts[command_start_line(src, int(name[5:]))] + elif name in ranges: + start = src.at(ranges[name][0], ranges[name][1]) + else: + continue + own = set(self.notions_of(name)) if name in self.renames else notions + lines = [] + for notion in sorted(own, key=lambda n: n.tidy): + written = self.write_name(module, src, start, notion.to_tidy, None, " in") + if written is None: + self.note(path, start, name, "local transition not written", + f"no written form of `{notion.to_tidy}` resolves here") + continue + lines.append(f"attribute [local fun_prop] {written} in\n") + self.need(module, notion.to_tidy, False) + if lines: + self.files[path].replaces.append(Replace(start, start, "".join(lines))) + self.bridged.append(name if not name.startswith("line:") + else f"{path.relative_to(ROOT)}:{int(name[5:]) + 1}") + 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] @@ -1855,7 +1909,9 @@ def imports_of(module: str) -> set[str]: # Output. def render(self) -> dict[Path, str]: + """The rewritten texts; lines the rewrite pushes past the style limit are noted.""" out = {} + self.manual = [m for m in self.manual if m.kind != LONG_LINE] for path, fe in self.files.items(): if not (fe.replaces or fe.wraps or fe.regions): continue @@ -1865,6 +1921,9 @@ def render(self) -> dict[Path, str]: self.round_trips += removed if text != src.text: out[path] = text + for line in long_lines(src.text, text) if path.suffix == ".lean" else (): + self.manual.append(Manual(str(path.relative_to(ROOT)), line, "", LONG_LINE, + "reflow by hand")) return out def summary(self) -> dict: @@ -1873,7 +1932,17 @@ def summary(self) -> dict: return {"area": self.area, "declarations": len(self.batch), "modes": dict(modes), "manual": dict(kinds.most_common()), "sites": dict(self.sites), "twin_references": dict(self.twin_refs), - "imports": [list(i) for i in self.imports]} + "imports": [list(i) for i in self.imports], "bridged": sorted(self.bridged)} + + +LONG_LINE = "line longer than 100 characters after rewriting" + + +def long_lines(old: str, new: str, limit: int = 100) -> list[int]: + """The 1-based lines of `new` longer than `limit` that are not lines of `old`.""" + before = set(old.split("\n")) + return [i for i, line in enumerate(new.split("\n"), 1) + if len(line) > limit and line not in before] def spells(token: str, name: str) -> bool: @@ -1890,6 +1959,18 @@ def namespace_of(name: str) -> str: return name.rsplit(".", 1)[0] if "." in name else "" +def command_start_line(src: SourceFile, line: int) -> int: + """The first line of the docstring and attributes above the 0-based `line`.""" + mask_lines = src.mask.split("\n") + while line > 0: + above, above_mask = src.lines[line - 1], mask_lines[line - 1] + if above.strip() and (not above_mask.strip() or above_mask.lstrip().startswith("@[")): + line -= 1 + else: + break + return line + + def enclosing_opener(mask: str, pos: int) -> int: """The unmatched opening bracket before `pos`, or -1.""" depth = 0 @@ -1943,6 +2024,10 @@ def plan_markdown(plan: dict, limit: int = 40) -> str: f"{m['detail']} |") if len(plan["manual"]) > limit: out.append(f"| … {len(plan['manual']) - limit} more in the JSON report | | | | |") + if s.get("bridged"): + out.append(f"Declarations given `attribute [local fun_prop] ComputableInPolyTime.tidy " + f"in` (plain-calculus gaps, for information): {len(s['bridged'])}: " + + ", ".join(f"`{n}`" for n in s["bridged"][:limit]) + ".") if s.get("twin_references"): out.append("References to case 1 originals in restated proofs: " + ", ".join( f"{n} {k}" for k, n in sorted(s["twin_references"].items())) + ".") @@ -2011,15 +2096,20 @@ def lake_build(targets: list[str], runner=subprocess.run) -> tuple[int, str]: def rewrite(model: Model, entries: list[Entry], twins: dict[str, str], area: str, verify: bool, rounds: int, build=lake_build) -> tuple[Planner, dict | None]: """Write the area's rewrite into the checkout. With `verify`, build the three libraries - strictly and, up to `rounds` times, wrap the translated proofs that fail and rebuild. - Remaining failures are reported, never patched over.""" + strictly and, up to `rounds` times, repair and rebuild: a translated proof that fails is + wrapped, and a wrapped proof or another declaration that fails is preceded by + `attribute [local fun_prop] ComputableInPolyTime.tidy in` (proof-local tidy reasoning; its + use is reported as a plain-calculus gap). Remaining failures are reported, never patched + over with `sorry`.""" originals: dict[Path, str] = {} force: set[str] = set() + bridge: set[tuple[str, str]] = set() result, history = None, [] for round_ in range(1, rounds + 1): for path, text in originals.items(): # plan against the sources of the build path.write_text(text, encoding="utf-8") - planner = Planner(model, entries, twins, area, frozenset(force)).plan() + planner = Planner(model, entries, twins, area, frozenset(force), + frozenset(bridge)).plan() texts = planner.render() for path, text in texts.items(): originals.setdefault(path, planner.source(path).text) @@ -2028,12 +2118,17 @@ def rewrite(model: Model, entries: list[Entry], twins: dict[str, str], area: str return planner, None code, output = build(list(qr.ROOTS)) result = check_build(planner, texts, output, code, round_) - history.append({k: result[k] for k in ("round", "status", "failing", "forced_wrap")}) + history.append({k: result[k] for k in ("round", "status", "failing", "forced_wrap", + "failing_clients")}) retry = {d for d in result["failing"] if planner.decls.get(d, {}).get("mode") == "translate"} - if not retry or round_ == rounds: + wrapped = {(model.decls[d]["module"], d) for d in result["failing"] + if planner.decls.get(d, {}).get("mode") == "wrap"} + new_bridges = (wrapped | {tuple(c) for c in result["failing_clients"]}) - bridge + if not (retry or new_bridges) or round_ == rounds: break force |= retry + bridge |= new_bridges result["history"] = history return planner, result @@ -2047,7 +2142,7 @@ def check_build(planner: Planner, texts: dict[Path, str], output: str, code: int for name, info in planner.decls.items(): by_written[(info["path"], name.rsplit(".", 1)[-1])] = name by_written[(info["path"], info["target"].rsplit(".", 1)[-1])] = name - failing, clients, problems = set(), [], [] + failing, clients, problems, failing_clients = set(), [], [], set() for d in diagnostics(output): path = ROOT / d["path"] text = texts.get(path) or (path.read_text() if path.exists() else "") @@ -2060,12 +2155,43 @@ def check_build(planner: Planner, texts: dict[Path, str], output: str, code: int failing.add(decl) planner.decls[decl].setdefault("errors", []).append(d["message"]) elif d["level"] == "error": + client = client_decl(planner, path, text, texts, d["line"], header) + if client: + failing_clients.add(client) + item["decl"] = client[1] if not client[1].startswith("line:") else header clients.append(item) problems.append(item) errors = any(d["level"] == "error" for d in problems) return {"round": round_, "status": "passed" if code == 0 and not errors else "failed", "exit_code": code, "failing": sorted(failing), "client_errors": clients, - "diagnostics": problems, "forced_wrap": sorted(planner.force_wrap)} + "failing_clients": sorted(failing_clients), "diagnostics": problems, + "forced_wrap": sorted(planner.force_wrap), "bridged": sorted(planner.bridged)} + + +def client_decl(planner: Planner, path: Path, text: str, texts: dict[Path, str], line: int, + header: str) -> tuple[str, str] | None: + """The declaration (module and name) of an error outside the restated declarations, or + `line:N` for an anonymous command, located in the sources the plan was made from.""" + if not text or not path.is_relative_to(ROOT): + 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 len(names) == 1: + return module, names[0] + at = command_line(text, line) - 1 + block = text.split("\n")[at:min(at + 3, line)] + original = planner.source(path).lines if path in texts else text.split("\n") + hits = [i for i in range(len(original)) if original[i:i + len(block)] == block] + return (module, f"line:{hits[0]}") if len(hits) == 1 else None + + +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] + return text.count("\n", 0, starts[-1]) + 1 if starts else line def unified_diff(planner: Planner) -> str: @@ -2102,7 +2228,8 @@ def main(argv: list[str] | None = None) -> int: help="report only: do not check that the build outputs are current") parser.add_argument("--partial", action="store_true", help="report only: accept a partial build (a tree that does not build " - "completely); modules without outputs are listed, not analysed") + "completely); modules without outputs are listed, not analysed, and " + "the others must be current") parser.add_argument("--json", type=Path, help="write the full report as JSON") parser.add_argument("--markdown", type=Path, help="write the report as Markdown") parser.add_argument("--no-plan", action="store_true", help="report: skip rewrite plans") @@ -2110,7 +2237,7 @@ def main(argv: list[str] | None = None) -> int: help="rewrite: build strictly, wrap failing translations, report the rest") parser.add_argument("--diff", type=Path, help="rewrite: write a unified diff of the plan instead of the files") - parser.add_argument("--rounds", type=int, default=3) + parser.add_argument("--rounds", type=int, default=6) parser.add_argument("--limit", type=int, default=40, help="rows per Markdown table") args = parser.parse_args(argv) for area in args.area: @@ -2132,8 +2259,15 @@ def main(argv: list[str] | None = None) -> int: registry = load_registry(args.registry) except ValueError as error: parser.error(str(error)) - outputs = qr.check_outputs(args.build_dir, args.no_build_check or args.partial) - model = Model(args.build_dir, load_allowlist(args.allowlist), args.partial) + 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() \ + and not args.no_build_check: + parser.error("--partial checks the default build directory; pass --no-build-check " + "to report on another one unchecked") + model = Model(args.build_dir, load_allowlist(args.allowlist), args.partial, + not args.no_build_check) 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] From c1222c9b6015a896a980cdb82dc9ccd59c3691b6 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 00:51:59 -0400 Subject: [PATCH 07/10] fix(scripts): check rooted and inserted spellings for notation tokens Addresses review 5636889827 on #666: a `_root_.` candidate returned before the token checks, so a notation token spelling the whole rooted name could capture it. Rooted candidates now go through the same check, and a rewrite with no safe spelling is deferred. The spellings the rewrite inserts itself (`.tidy`, `.of_tidy`) are checked as well. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- scripts/test_tidy_sweep.py | 24 ++++++++++++++++++++++++ scripts/tidy_sweep.py | 30 +++++++++++++++++++++--------- 2 files changed, 45 insertions(+), 9 deletions(-) diff --git a/scripts/test_tidy_sweep.py b/scripts/test_tidy_sweep.py index 9ca449057e..dd7236d986 100644 --- a/scripts/test_tidy_sweep.py +++ b/scripts/test_tidy_sweep.py @@ -485,6 +485,30 @@ def test_multiline_notation(self) -> None: self.assertEqual(self.written(text, "foo", "N.foo", "N.bar", nth=2), "N.bar") self.assertEqual(t.notation_tokens(text, masks(text)[1]), {"bar"}) + def test_rooted_names_are_checked_for_tokens_too(self) -> None: + """Review 5636889827: tokens for `bar`, `N.bar` and `_root_.N.bar` capture every + spelling of `N.bar`, so the rewrite must be deferred, not written as `_root_.N.bar`.""" + text = ('namespace N\ndef foo : Nat := 1\ndef bar : Nat := 2\nend N\nopen N\n' + 'local notation "bar" => (3 : Nat)\nlocal notation "N.bar" => (4 : Nat)\n' + 'local notation "_root_.N.bar" => (5 : Nat)\ndef before : Nat := foo\n') + self.assertIsNone(self.written(text, "foo", "N.foo", "N.bar", nth=1)) + # Without the rooted token, the rooted spelling is the safe one. + text = text.replace('local notation "_root_.N.bar" => (5 : Nat)\n', "") + self.assertEqual(self.written(text, "foo", "N.foo", "N.bar", nth=1), "_root_.N.bar") + + def test_inserted_bridge_spellings_are_checked(self) -> None: + p, src = fake_planner("def d : Nat := foo\n", {}, tokens={"of_tidy"}) + self.assertTrue(p.bridge_spellings_captured(src)) + p, src = fake_planner("def d : Nat := foo\n", {}) + self.assertFalse(p.bridge_spellings_captured(src)) + # A conversion site in such a file stays unchanged and blocks its declaration. + text = " exact X enc hc" + p, src = fake_planner(text, {"X": {"m": "M", "sg": [[[0, 0], [0, 1]], 1], + "tidy": [POLY]}}, known={"Y"}, tokens={"tidy"}) + p.renames = {"X": "Y"} + self.assertFalse(p.convert(src.path, "M", 8, 9, "X", None, "tidy")) + self.assertIn("captures", p.blockers["X"][0]) + def test_imported_notation(self) -> None: """Reply 4365874664: `notation "bar" => (3 : Nat)` in a dependency.""" text = "open N\ndef before : Nat := foo\ndef after : Nat := foo\n" diff --git a/scripts/tidy_sweep.py b/scripts/tidy_sweep.py index bc06c3c429..006e2cdeb4 100644 --- a/scripts/tidy_sweep.py +++ b/scripts/tidy_sweep.py @@ -1354,15 +1354,17 @@ def resolves(self, module: str, src: SourceFile, offset: int, written: str, def exists(name: str) -> bool: return name in self.known or name in privates - if written.startswith("_root_."): - return {written[len("_root_."):]} if exists(written[len("_root_."):]) else set() - scope = src.scopes.at(offset) - out = {h for p in src.scopes.prefixes(offset) - for h in [p + "." + written if p else written] if exists(h)} - first = written.split(".")[0] - if first in self.local_names(module, src, offset) or first in scope.variables \ - or first in scope.aliases: - out.add("") + if written.startswith("_root_."): # absolute, but a token may still capture it + name = written[len("_root_."):] + out = {name} if exists(name) else set() + else: + scope = src.scopes.at(offset) + out = {h for p in src.scopes.prefixes(offset) + for h in [p + "." + written if p else written] if exists(h)} + first = written.split(".")[0] + if first in self.local_names(module, src, offset) or first in scope.variables \ + or first in scope.aliases: + out.add("") if token_capture(written, following, self.tokens) \ or token_capture(written, following, src.scopes.tokens): out.add("") @@ -1379,6 +1381,12 @@ def reachable(self, src: SourceFile, offset: int, written: str, target: str) -> return any(o.namespace + "." + written == target and first not in o.hiding and (o.only is None or written in o.only) for o in src.scopes.at(offset).opens) + def bridge_spellings_captured(self, src: SourceFile) -> bool: + """Whether a token could capture the fixed spellings the rewrite inserts, the field + `.tidy` and the leading-dot `.of_tidy` of the plain predicates.""" + return any(token_capture(word, " ", tokens) for word in ("tidy", "of_tidy") + for tokens in (self.tokens, src.scopes.tokens)) + def write_name(self, module: str, src: SourceFile, offset: int, target: str, first: str | None = None, following: str = "") -> str | None: """The shortest written form of `target`, followed by `following`, that Lean surely @@ -1691,6 +1699,8 @@ def wrap_plan(self, entry: Entry, src: SourceFile, dt: DeclText, sig_refs: list[ problems.append("termination or `where` clauses") if self.hidden_tidy(entry.name, src, dt, sig_refs): problems.append("tidy hypothesis from a `variable` command or notation") + if self.bridge_spellings_captured(src): + problems.append("a notation token captures `.tidy` or `.of_tidy`") if problems: return None, problems iffs = [self.write_name(self.model.decls[entry.name]["module"], src, dt.assign, n.iff) @@ -1755,6 +1765,8 @@ def convert_site(self, src: SourceFile, start: int, end: int, old: str sg = self.model.constants.get(old, {}).get("sg") if not sg: return "", [] + if self.bridge_spellings_captured(src): + return "a notation token captures `.tidy` or `.of_tidy`", [] binders, conclusion = sg mask = src.mask opener = enclosing_opener(mask, start) From af2e3ba428a254563a8c962abfc81fcfa2ae04f8 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 00:53:45 -0400 Subject: [PATCH 08/10] fix(scripts): rename quoted names in `#guard_msgs` text The full-name pattern for comments refused a name followed by `'`, to spare primed constants, which also skipped quoted names such as `info: 'Old.name' depends on axioms`, so restated lemmas left their axiom guards failing. A following `'` is now accepted unless the name is unquoted and its primed form is a constant. Found in the Logics sweep. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- scripts/test_tidy_sweep.py | 25 +++++++++++++++++++++++++ scripts/tidy_sweep.py | 8 +++++++- 2 files changed, 32 insertions(+), 1 deletion(-) diff --git a/scripts/test_tidy_sweep.py b/scripts/test_tidy_sweep.py index dd7236d986..0f7f754725 100644 --- a/scripts/test_tidy_sweep.py +++ b/scripts/test_tidy_sweep.py @@ -752,6 +752,31 @@ def test_rewrite_refuses_partial_builds(self) -> None: self.assertIn("--partial is only for report", err.getvalue()) +class CommentTests(unittest.TestCase): + def test_full_names_in_comments(self) -> None: + """`#guard_msgs` text quotes renamed names; primed constants are other names.""" + text = ("/--\ninfo: 'A.computableTidilyInPolyTime_x' depends on axioms: [propext]\n-/\n" + "-- see A.computableTidilyInPolyTime_x' and `A.computableTidilyInPolyTime_x`\n") + 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 + 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 + try: + p.plan_comments() + finally: + t.qr.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( + "`A.computableTidilyInPolyTime_x`", "`A.computableInPolyTime_x`")) + + class SummaryTests(unittest.TestCase): def test_counts_by_area_and_case(self) -> None: entries = [t.Entry("a", "M", "p", "Logics", "theorem", "2"), diff --git a/scripts/tidy_sweep.py b/scripts/tidy_sweep.py index 006e2cdeb4..5e0c424d8b 100644 --- a/scripts/tidy_sweep.py +++ b/scripts/tidy_sweep.py @@ -1828,7 +1828,7 @@ def plan_comments(self) -> None: for old in renamed: by_last[old.rsplit(".", 1)[-1]].append(old) full = re.compile(r"(? None: fe.replaces.append(Replace(a, a + len(token), new)) done.append((a, a + len(token))) for m in full.finditer(src.text, lo, hi): + # `'Old.name' depends on axioms` quotes the name; `Old.name'` may also be a + # different, primed constant. + quoted = m.start() > 0 and src.text[m.start() - 1] == "'" + if src.text.startswith("'", m.end()) and not quoted \ + and m[1] + "'" in self.known: + continue if not any(s <= m.start() < e for s, e in done): fe.replaces.append(Replace(m.start(), m.end(), renamed[m[1]])) From 4db8b1ab21273caaa7397dbcc384243c3667a672 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 00:59:16 -0400 Subject: [PATCH 09/10] fix(scripts): report only long lines with code The long-line report flagged `#guard_msgs` text renamed inside comments, which the style checks accept. Found in the Logics sweep. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- scripts/test_tidy_sweep.py | 2 ++ scripts/tidy_sweep.py | 6 ++++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/scripts/test_tidy_sweep.py b/scripts/test_tidy_sweep.py index 0f7f754725..b95d9f901a 100644 --- a/scripts/test_tidy_sweep.py +++ b/scripts/test_tidy_sweep.py @@ -257,6 +257,8 @@ def test_new_long_lines_are_reported(self) -> None: old = "a\n" + "x" * 120 + "\nshort\n" new = "a\n" + "x" * 120 + "\n" + "y" * 101 + "\n" self.assertEqual(t.long_lines(old, new), [3]) + # Comment-only lines, such as `#guard_msgs` text, are not reported. + self.assertEqual(t.long_lines("", "/--\ninfo: '" + "x" * 120 + "'\n-/\n"), []) def test_regions_transform_their_edited_text(self) -> None: text = "a := X\nb" diff --git a/scripts/tidy_sweep.py b/scripts/tidy_sweep.py index 5e0c424d8b..0244f11d9e 100644 --- a/scripts/tidy_sweep.py +++ b/scripts/tidy_sweep.py @@ -1957,10 +1957,12 @@ def summary(self) -> dict: def long_lines(old: str, new: str, limit: int = 100) -> list[int]: - """The 1-based lines of `new` longer than `limit` that are not lines of `old`.""" + """The 1-based lines of `new` with code, longer than `limit`, that are not lines of `old` + (comment-only lines, such as `#guard_msgs` text, are left out).""" before = set(old.split("\n")) + code = masks(new)[0].split("\n") return [i for i, line in enumerate(new.split("\n"), 1) - if len(line) > limit and line not in before] + if len(line) > limit and line not in before and code[i - 1].strip()] def spells(token: str, name: str) -> bool: From 2b847828f7d4233e1e49d2f32e974052d74451f1 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 01:22:22 -0400 Subject: [PATCH 10/10] fix(scripts): check the dotted spellings the rewrite inserts Thread 4366077232 on #666: the guard for the inserted `.tidy` and `.of_tidy` checked them only as identifiers, but a notation token such as `".of_tidy"` or `postfix ".tidy"` captures them literally. At a `.` no identifier competes, so any token other than `.` that starts the inserted text now counts as a capture, and the conversion is deferred. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- scripts/test_tidy_sweep.py | 18 ++++++++++++++++++ scripts/tidy_sweep.py | 13 ++++++++++--- 2 files changed, 28 insertions(+), 3 deletions(-) diff --git a/scripts/test_tidy_sweep.py b/scripts/test_tidy_sweep.py index b95d9f901a..3b7d0dfe93 100644 --- a/scripts/test_tidy_sweep.py +++ b/scripts/test_tidy_sweep.py @@ -511,6 +511,24 @@ def test_inserted_bridge_spellings_are_checked(self) -> None: self.assertFalse(p.convert(src.path, "M", 8, 9, "X", None, "tidy")) self.assertIn("captures", p.blockers["X"][0]) + def test_dotted_bridge_spellings_are_checked(self) -> None: + """Thread 4366077232: notations `.of_tidy` and `.tidy` capture the inserted spellings + literally, so the conversion is not made and its declaration is deferred.""" + sg = [[[0, 1]], 1] + for notation in ('local notation ".of_tidy" => (fun _ : Tidy => Plain.mk 5)\n', + 'local postfix:max ".tidy" => (fun _ : Plain => Tidy.mk 7)\n'): + text = notation + "def after : Tidy := X h\n" + p, src = fake_planner(text, {"X": {"m": "M", "sg": sg, "tidy": [POLY]}}, + known={"Y"}) + p.renames = {"X": "Y"} + self.assertTrue(p.bridge_spellings_captured(src), notation) + start = text.index("X h") + self.assertFalse(p.convert(src.path, "M", start, start + 1, "X", None, "tidy")) + self.assertEqual(p.files[src.path].replaces, []) + self.assertIn("captures", p.blockers["X"][0]) + p, src = fake_planner("def after : Tidy := X h\n", {}, tokens={".", ".."}) + self.assertFalse(p.bridge_spellings_captured(src)) + def test_imported_notation(self) -> None: """Reply 4365874664: `notation "bar" => (3 : Nat)` in a dependency.""" text = "open N\ndef before : Nat := foo\ndef after : Nat := foo\n" diff --git a/scripts/tidy_sweep.py b/scripts/tidy_sweep.py index 0244f11d9e..ca9284f45f 100644 --- a/scripts/tidy_sweep.py +++ b/scripts/tidy_sweep.py @@ -1383,9 +1383,16 @@ def reachable(self, src: SourceFile, offset: int, written: str, target: str) -> def bridge_spellings_captured(self, src: SourceFile) -> bool: """Whether a token could capture the fixed spellings the rewrite inserts, the field - `.tidy` and the leading-dot `.of_tidy` of the plain predicates.""" - return any(token_capture(word, " ", tokens) for word in ("tidy", "of_tidy") - for tokens in (self.tokens, src.scopes.tokens)) + `.tidy` and the leading-dot `.of_tidy` of the plain predicates: as identifiers, or + literally. At a `.` no identifier competes, so any token other than `.` that starts the + inserted text is read instead.""" + for tokens in (self.tokens, src.scopes.tokens): + if any(token_capture(word, " ", tokens) for word in ("tidy", "of_tidy")): + return True + if any(token != "." and (spelling + " ").startswith(token) + for spelling in (".tidy", ".of_tidy") for token in tokens.get(".", ())): + return True + return False def write_name(self, module: str, src: SourceFile, offset: int, target: str, first: str | None = None, following: str = "") -> str | None: