ci: ratchet public tidy statements per module (#456 S3)

.github/workflows/lean_action_ci.yml

@@ -84,6 +84,17 @@ jobs:
         with:
           path: ./.lake
           key: ${{ steps.lake-cache.outputs.cache-primary-key }}
+      # Source hygiene that needs the build outputs: each module's count of public statements that
+      # mention tidy computability (#456) must equal its baseline; proofs may use it. See
+      # scripts/check_tidy_surface.py. Its tests on a compiled module need Lean, so the Python
+      # tests at the start skip them; they run here.
+      - name: "Tidy statement ratchet"
+        run: |
+          set -e
+          command -v lake
+          test -d .lake/packages
+          python3 -B -m unittest scripts/test_check_tidy_surface.py
+          python3 -B scripts/check_tidy_surface.py
       - name: "lake exe mk_all --check"
         run: |
           set -e

CONTRIBUTING.md

@@ -71,6 +71,17 @@ also loads private information, so such edits do reach its clients.
   unfold a definition by name. Reduction by `rfl` or `decide` is not recorded, and its counts are
   review signals, not rules.
 
+Tidy computability (`ComputableTidily…`, `ComputesTidily…`, `IsTidy…`) may appear anywhere inside
+proofs, through `.tidy`, `.of_tidy`, a proof-local `attribute [local fun_prop] … in` or a tidy
+`have`. It never appears in a public statement: a theorem's type, or a definition's type, exposed
+body or fields. Only the raw machine constructions in `scripts/tidy_allowlist.txt` are exempt.
+CI enforces this with `scripts/check_tidy_surface.py`. The existing tidy statements, which #456 is
+restating, are counted per module in `scripts/tidy_surface_baseline.json`, and CI fails when a
+module's count differs from its entry. When you remove some, lower the baseline in the same PR
+with `python3 scripts/check_tidy_surface.py --update`, so that they cannot come back. Until your
+PR lands, any other merge that removes tidy statements makes your baseline stale: rebase and
+rerun `--update`.
+
 ## AI assistance and review
 
 AI-assisted and human-written contributions follow the same standards. Disclose which AI tools

scripts/QualityReport.lean

@@ -21,7 +21,11 @@ constant:
   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;
+  `tb`: for an exported definition, those in its exposed body outside proofs. Proofs are the
+  subterms whose type is a proposition, together with the statements of proof-local `have`s (a
+  `let` whose type is a proposition): tidy computability is allowed there (#456). Telling them
+  apart needs types, so the modules of the definitions whose body mentions a tidy constant are
+  imported (at the exported level) for this, and their rows are printed last;
 * `u`: for an exported constant, the other constants of the same module that its exported
   statement or exposed body mentions (these cannot become private while it stays public);
 * `r`: its declaration range `[line, column, endLine, endColumn, selLine, selColumn, selEndLine,
@@ -66,6 +70,47 @@ def isTidy (n : Name) : Bool :=
       s.startsWith "IsTidy"
   | _ => false
 
+def mentionsTidy (e : Expr) : Bool :=
+  e.getUsedConstants.any isTidy
+
+/-- Add to `found` the tidy constants of `e` outside proofs: subterms whose type is a proposition,
+and the type and value of a `let` or `have` whose type is a proposition. A subterm whose type
+cannot be inferred counts as a non-proof. -/
+partial def tidyOutsideProofs (found : IO.Ref NameSet) (e : Expr) : MetaM Unit := do
+  unless mentionsTidy e do return
+  if ← (try Meta.isProof e catch _ => pure false) then return
+  match e with
+  | .const n _ => if isTidy n then found.modify (·.insert n)
+  | .app f a => tidyOutsideProofs found f; tidyOutsideProofs found a
+  | .mdata _ b | .proj _ _ b => tidyOutsideProofs found b
+  | .lam n t b bi | .forallE n t b bi =>
+    tidyOutsideProofs found t
+    Meta.withLocalDecl n bi t fun x => tidyOutsideProofs found (b.instantiate1 x)
+  | .letE n t v b _ =>
+    unless ← (try Meta.isProp t catch _ => pure false) do
+      tidyOutsideProofs found t
+      tidyOutsideProofs found v
+    Meta.withLetDecl n t v fun x => tidyOutsideProofs found (b.instantiate1 x)
+  | _ => pure ()
+
+/-- `tidyOutsideProofs` for the exposed bodies of the definitions `names` of `modules`, which are
+imported (at the exported level, as by a client) from the search path of `lake env` and
+`libDir`. -/
+unsafe def tidyBodies (libDir : System.FilePath) (modules : Array Name) (names : Array Name) :
+    IO (NameMap (Array String)) := do
+  if names.isEmpty then return {}
+  initSearchPath (← findSysroot) [libDir]
+  let env ← importModules (modules.map ({ module := · })) {} (level := .exported)
+  let ctx : Core.Context := { fileName := "<QualityReport>", fileMap := default }
+  let mut result : NameMap (Array String) := {}
+  for n in names do
+    let some (.defnInfo v) := env.find? n
+      | throw <| IO.userError s!"cannot find the exposed body of {n}"
+    let found ← IO.mkRef {}
+    discard <| (tidyOutsideProofs found v.value).toIO ctx { env }
+    result := result.insert n ((← found.get).toArray.map toString)
+  return result
+
 /-- The declarations named by entries of the extensions whose names end in one of `suffixes`.
 Every such extension is a `MapDeclarationExtension`, whose entries are pairs headed by a name. -/
 unsafe def entryNames (entries : Array (Name × Array EnvExtensionEntry)) (suffixes : List String) :
@@ -143,6 +188,9 @@ unsafe def run (libDir : System.FilePath) (pairs : Option String := none) : IO U
   let mut defs : Std.HashMap (Expr × Expr) (Array (String × Name)) := {}
   -- The mapped regions must stay alive while `theorems` and `defs` refer to their expressions.
   let mut regions : Array CompactedRegion := #[]
+  -- Rows of exposed definitions whose body mentions a tidy constant wait for `tidyBodies`.
+  let mut deferred : Array (Name × List (String × Json)) := #[]
+  let mut bodyModules : NameSet := {}
   repeat
     let line ← stdin.getLine
     if line.isEmpty then break
@@ -168,12 +216,9 @@ unsafe def run (libDir : System.FilePath) (pairs : Option String := none) : IO U
         | some ec => ec.type.getUsedConstants
         | none => #[]
       let uses := uses.filter (fun n => n != c.name && sameModule.contains n) |>.toList.eraseDups
-      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), ("tb", toJson tidyBody),
+        ("doc", docs.contains c.name), ("tidy", toJson tidy),
         ("u", toJson (uses.map (·.toString))),
         ("r", (ranges.find? c.name).map rangeJson |>.getD .null)]
       if pairs.isSome then
@@ -182,7 +227,14 @@ unsafe def run (libDir : System.FilePath) (pairs : Option String := none) : IO U
           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
+      let tidyBody := match e with
+        | some (.defnInfo v) => mentionsTidy v.value
+        | _ => false
+      if tidyBody then
+        deferred := deferred.push (c.name, row)
+        bodyModules := bodyModules.insert mod.toName
+      else
+        stdout.putStrLn <| Json.compress <| Json.mkObj (row ++ [("tb", Json.arr #[])])
       if let some ec := e then
         unless c.name.isInternalDetail do
           match c, ec with
@@ -193,6 +245,10 @@ unsafe def run (libDir : System.FilePath) (pairs : Option String := none) : IO U
             let key := (normalize ec ec.type, normalize ec v.value)
             defs := defs.insert key ((defs.getD key #[]).push (mod, c.name))
           | _, _ => pure ()
+  let bodies ← tidyBodies libDir bodyModules.toArray (deferred.map (·.1))
+  for (n, row) in deferred do
+    let tb := (bodies.find? n).getD #[]
+    stdout.putStrLn <| Json.compress <| Json.mkObj (row ++ [("tb", toJson tb)])
   let emit (kind : String) (group : Array (String × Name)) : IO Unit := do
     if (group.map (·.1)).toList.eraseDups.length > 1 then
       stdout.putStrLn <| Json.compress <| Json.mkObj [

scripts/check_tidy_surface.py

@@ -0,0 +1,151 @@
+#!/usr/bin/env python3
+"""Stop tidy computability from spreading into public statements (S3 of #456).
+
+Usage: python3 scripts/check_tidy_surface.py [--update [--allow-increase]] [--no-build-check]
+
+Tidy computability (`ComputableTidily…`, `ComputesTidily…`, `IsTidy…`) is a proof device: it may
+appear anywhere inside proofs, never in a public statement. A public declaration of the
+`Complexity` library has a *tidy statement* when a tidy constant occurs in its type (a theorem's
+statement, a definition's type, a structure field) or in the exposed body of a definition.
+Proofs, bodies that are not exposed and private declarations do not count, and neither do the raw
+machine constructions listed in `scripts/tidy_allowlist.txt` (#608).
+
+The check counts tidy statements per module and compares the counts with
+`scripts/tidy_surface_baseline.json`, which records those that #456's sweep has yet to restate.
+Every count must equal its baseline entry (a module without an entry, such as a new one, has
+none). A count above its entry is a new tidy statement. A count below it fails too, until the
+baseline is lowered in the same change: otherwise the unused allowance would let a removed
+statement come back later. `--update` rewrites the baseline with the current counts; it refuses
+to raise an entry unless `--allow-increase` is given, for instance when a module that has tidy
+statements is moved.
+
+Declarations written in source come from the `.ilean` files and statements from the `.olean`
+files, read by `scripts/quality_report.py` and `scripts/QualityReport.lean`. The check needs the
+build outputs of `lake build Complexity ComplexityTests ComplexityAbstracts` (`lake build` and
+`lake test`), and refuses stale ones unless `--no-build-check` is given.
+"""
+
+from __future__ import annotations
+
+import argparse
+import json
+import sys
+from collections import defaultdict
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[1]
+sys.path.insert(0, str(ROOT / "scripts"))
+import quality_report as qr  # noqa: E402
+
+ALLOWLIST = ROOT / "scripts/tidy_allowlist.txt"
+BASELINE = ROOT / "scripts/tidy_surface_baseline.json"
+UPDATE = "python3 scripts/check_tidy_surface.py --update"
+
+# A tidy statement: the declaration, its line, and the tidy constants it mentions.
+Statement = tuple[str, int, list[str]]
+
+
+def load_allowlist(path: Path) -> set[str]:
+    """Source paths relative to the repository root, one per line; `#` starts a comment."""
+    return {line.split("#", 1)[0].strip() for line in path.read_text().splitlines()} - {""}
+
+
+def tidy_statements(lib: qr.Library, allowlist: set[str]) -> dict[str, list[Statement]]:
+    """The tidy statements of each module outside the allowlist, by source path. Declarations
+    written in source count, structure fields included; constants generated from them (`simps`
+    lemmas, equation lemmas, recursors) do not."""
+    decls, _, _ = qr.collect_declarations(lib)
+    found: dict[str, list[Statement]] = defaultdict(list)
+    for name, decl in decls.items():
+        if decl["role"] == "generated":
+            continue
+        const = lib.constants[name]
+        mentions = sorted(set(const["tidy"]) | set(const.get("tb", ())))
+        path = "Complexity/" + decl["path"]
+        if mentions and path not in allowlist:
+            found[path].append((name, decl["range"][0] if decl["range"] else 0, mentions))
+    return {path: sorted(rows, key=lambda row: (row[1], row[0])) for path, rows in found.items()}
+
+
+def load_baseline(path: Path) -> dict[str, int]:
+    data = json.loads(path.read_text())
+    if not isinstance(data, dict) or not all(
+            isinstance(k, str) and type(v) is int and v > 0 for k, v in data.items()):
+        sys.exit(f"{path}: expected a JSON object from source paths to positive counts")
+    return data
+
+
+def baseline_text(counts: dict[str, int]) -> str:
+    return json.dumps({k: v for k, v in sorted(counts.items()) if v}, indent=1) + "\n"
+
+
+def compare(counts: dict[str, int], baseline: dict[str, int]
+            ) -> tuple[dict[str, tuple[int, int]], dict[str, tuple[int, int]]]:
+    """`(over, under)`: the modules whose count exceeds or falls short of their baseline entry,
+    as `path -> (count, entry)`. A module without an entry has entry 0."""
+    over, under = {}, {}
+    for path in sorted(set(counts) | set(baseline)):
+        count, entry = counts.get(path, 0), baseline.get(path, 0)
+        if count > entry:
+            over[path] = (count, entry)
+        elif count < entry:
+            under[path] = (count, entry)
+    return over, under
+
+
+def over_report(over: dict[str, tuple[int, int]], found: dict[str, list[Statement]]) -> str:
+    out = ["Public statements may not mention tidy computability, only proofs may (#456). Restate "
+           "these with plain computability (`ComputableInPolyTime`, `ComputableInTimeAndSpace`, "
+           "…) and switch inside the proofs (`.tidy`, `.of_tidy`).", ""]
+    for path, (count, entry) in over.items():
+        out.append(f"{path}: {count} tidy statement(s), baseline {entry}:")
+        out += [f"  {path}:{line}: {name} mentions {', '.join(mentions)}"
+                for name, line, mentions in found.get(path, [])]
+    return "\n".join(out)
+
+
+def main(argv: list[str] | None = None) -> int:
+    parser = argparse.ArgumentParser(description=__doc__,
+                                     formatter_class=argparse.RawDescriptionHelpFormatter)
+    parser.add_argument("--update", action="store_true",
+                        help="rewrite the baseline with the current counts")
+    parser.add_argument("--allow-increase", action="store_true",
+                        help="with --update, allow raising entries and adding modules")
+    parser.add_argument("--no-build-check", action="store_true",
+                        help="do not check that the build outputs are current")
+    parser.add_argument("--allowlist", type=Path, default=ALLOWLIST)
+    parser.add_argument("--baseline", type=Path, default=BASELINE)
+    args = parser.parse_args(argv)
+    if args.allow_increase and not args.update:
+        parser.error("--allow-increase needs --update")
+    qr.check_outputs(qr.DEFAULT_BUILD_DIR, args.no_build_check)
+    found = tidy_statements(qr.Library(qr.DEFAULT_BUILD_DIR), load_allowlist(args.allowlist))
+    counts = {path: len(rows) for path, rows in found.items()}
+    baseline = load_baseline(args.baseline) if args.baseline.exists() else {}
+    over, under = compare(counts, baseline)
+    summary = f"{sum(counts.values())} public tidy statement(s) in {len(counts)} module(s)"
+    if args.update:
+        if over and not args.allow_increase:
+            print(over_report(over, found), file=sys.stderr)
+            print("\nThe baseline only goes down; pass --allow-increase to raise it on purpose, "
+                  "for instance for a moved module.", file=sys.stderr)
+            return 1
+        args.baseline.write_text(baseline_text(counts))
+        print(f"Wrote {args.baseline}: {summary}.")
+        return 0
+    if over:
+        print(over_report(over, found), file=sys.stderr)
+    if under:
+        print(("\n" if over else "") + "Tidy statements were removed, so the baseline is stale. "
+              f"Lower it with `{UPDATE}` and commit the result, so that they cannot come back:",
+              file=sys.stderr)
+        print("\n".join(f"  {path}: {count} (baseline {entry})"
+                        for path, (count, entry) in under.items()), file=sys.stderr)
+    if over or under:
+        return 1
+    print(f"{summary}, matching the baseline.")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())