feat: reject deprecated APIs in submissions, report them in upgrades

CONTRACT.md

@@ -53,6 +53,11 @@ support a possible future migration. Source MUST use explicit imports where
 practical and MUST NOT organize mathematical modules by producer, model, or
 submission identifier.
 
+The submitted modules MUST build without deprecation warnings under the pinned
+Lean/Mathlib pair. A deprecation is a warning today and an error after a later
+upgrade, so the receiver rejects each one in the submission's own files as
+`DEPRECATED_API`; Lean's warning names the replacement.
+
 Every declared public entrypoint MUST elaborate and be accepted by Lean. The
 receiver additionally replays each submitted module through the kernel with
 `leanchecker`, so admission does not rest on the elaborator's word alone. A
@@ -185,7 +190,7 @@ Stable rejection categories include `SCHEMA_INVALID`,
 `SORRY_DETECTED`, `UNAUTHORIZED_AXIOM`, `DUPLICATE_STATEMENT`,
 `TRIVIAL_BASELINE_RESULT`, `DEGENERATE_THEOREM_FAMILY`, `CORPUS_REGRESSION`,
 `KERNEL_RECHECK_FAILED`, `CONJECTURE_PROVABLE`, `CONJECTURE_REFUTED`,
-`CONJECTURE_QUOTA_EXCEEDED`, and `SECURITY_POLICY_VIOLATION`.
+`CONJECTURE_QUOTA_EXCEEDED`, `DEPRECATED_API`, and `SECURITY_POLICY_VIOLATION`.
 
 A submission the receiver accepts is merged without human action when its
 author appears in `policy/auto_merge_allowlist.json`. Nobody reads the

tests/test_mathlib_upgrade.py

@@ -111,6 +111,12 @@ class Result:
         self.assertEqual(result["code"], "BUILD_FAILED")
         self.assertIn("unknown constant 'Nat.choose_symm_diff'", result["error"])
 
+    def test_upgrade_audit_reports_corpus_deprecations_without_blocking(self) -> None:
+        source = (ROOT / "tools" / "audit_mathlib_upgrade.py").read_text()
+        self.assertIn('"corpus_deprecations": deprecated', source)
+        self.assertIn("sorted(deprecations(build, corpus_files))", source)
+        self.assertNotIn("DEPRECATED_API", source, "an upgrade must not be blocked by deprecations")
+
     def test_upgrade_audit_rechecks_the_corpus_against_the_kernel(self) -> None:
         """A release bump must not land with proofs nobody re-verified."""
         source = (ROOT / "tools" / "audit_mathlib_upgrade.py").read_text()

tests/test_validator.py

@@ -394,6 +394,57 @@ class Result:
             self.assertNotIn(noise, message)
         self.assertLessEqual(len(message), frontier_validate.DIAGNOSTIC_LIMIT)
 
+    def test_a_deprecated_api_in_the_submission_is_rejected(self) -> None:
+        """A deprecation is a warning today and an error after a later Mathlib upgrade.
+
+        Every one admitted became a future break in the upgrade audit; eleven
+        had to be fixed by hand in #224.
+        """
+        calls: list[list[str]] = []
+
+        class Result:
+            returncode = 0
+            stdout = (
+                "✔ [2530/2541] Built LeanFrontier.NumberTheory.SternDiatomic (2.4s)\n"
+                "⚠ [2531/2541] Built LeanFrontier.Algebra.New (1.2s)\n"
+                "warning: LeanFrontier/Algebra/New.lean:3:40: `if_pos` has been deprecated: Use `ite_eq_left` instead\n"
+                "warning: LeanFrontier/Algebra/New.lean:1:0: 'Mathlib.Data.Real.Basic' has been deprecated: please replace this import by\n"
+                "\n"
+                "import Mathlib.Basic.Real.Basic\n"
+                "warning: LeanFrontier/Algebra/New.lean:9:2: this tactic is never executed\n"
+                "warning: LeanFrontier/Topology/Furstenberg.lean:162:25: `Set.mem_setOf_eq` has been deprecated: Use `Set.mem_ofPred_eq` instead\n"
+            )
+            stderr = ""
+
+        original = frontier_validate.run
+        frontier_validate.run = lambda cmd, cwd, timeout: (calls.append(cmd), Result())[1]
+        try:
+            report = frontier_validate.Report()
+            frontier_validate.lean_audit(
+                None, self.candidate, [], ["LeanFrontier.Algebra.New"], {}, {},
+                {"build_timeout_seconds": 300, "kernel_recheck_timeout_seconds": 180}, {}, {}, set(), report,
+            )
+        finally:
+            frontier_validate.run = original
+        self.assertEqual([item.code for item in report.diagnostics], ["DEPRECATED_API"])
+        message = report.diagnostics[0].message
+        self.assertIn("`if_pos` has been deprecated: Use `ite_eq_left` instead", message)
+        self.assertIn("import Mathlib.Basic.Real.Basic", message)
+        self.assertNotIn("never executed", message, "only deprecations are rejected, not style lints")
+        self.assertNotIn("Furstenberg", message, "another module's deprecation is not the submitter's to fix")
+        self.assertEqual(calls, [["lake", "build"]], "a rejected build stops before the kernel recheck")
+
+    def test_deprecations_elsewhere_do_not_reject_a_submission(self) -> None:
+        fixtures = ROOT / "tests" / "fixtures" / "receiver"
+
+        class Result:
+            returncode = 0
+            stdout = (fixtures / "broken-build.stdout").read_text(encoding="utf-8")
+            stderr = ""
+
+        self.assertIn("has been deprecated", Result.stdout)
+        self.assertEqual(frontier_validate.deprecations(Result(), {"LeanFrontier/Algebra/New.lean"}), [])
+
     def test_a_pathological_build_is_capped(self) -> None:
 
         class Result:

tests/test_workflow_contract.py

@@ -130,6 +130,8 @@ def test_receiver_replays_submitted_modules_through_the_kernel(self) -> None:
         validator = (ROOT / "tools" / "frontier_validate.py").read_text()
         self.assertIn('"lake", "env", "leanchecker"', validator)
         self.assertIn("KERNEL_RECHECK_FAILED", validator)
+        self.assertIn("DEPRECATED_API", validator)
+        self.assertIn("`DEPRECATED_API`", (ROOT / "CONTRACT.md").read_text(encoding="utf-8"))
         self.assertIn("kernel_recheck_timeout_seconds", validator)
 
     def test_receiver_smoke_tests_downstream_imports(self) -> None:

tools/audit_mathlib_upgrade.py

@@ -11,7 +11,7 @@
 from pathlib import Path
 from typing import Any
 
-from frontier_validate import failure_output, lean_errors, run as run_bounded
+from frontier_validate import deprecations, failure_output, lean_errors, run as run_bounded
 from mathlib_release import ROOT, load_release_policy
 
 
@@ -97,6 +97,12 @@ def main(argv: list[str] | None = None) -> int:
         build = run(["lake", "build"], cwd=root, timeout=480)
         if build.returncode:
             raise RuntimeError(lean_errors(build, None) or "lake build failed")
+        # Reported, not blocking: a release that deprecates something the corpus
+        # uses should still land, and the list is the follow-up maintenance work.
+        # Sorted because Lake's parallel build order is not deterministic, and
+        # the re-audit compares this report byte for byte.
+        corpus_files = {f"{module.replace('.', '/')}.lean" for module in corpus_modules(root)}
+        deprecated = sorted(deprecations(build, corpus_files))
         for module in corpus_modules(root):
             recheck = run(["lake", "env", "leanchecker", module], cwd=root, timeout=300)
             if recheck.returncode:
@@ -120,6 +126,7 @@ def main(argv: list[str] | None = None) -> int:
             "entrypoint_count": len(entrypoints),
             "downstream_import_smoke": "pass",
             "kernel_recheck": "pass",
+            "corpus_deprecations": deprecated,
             "collisions": collisions,
             "accepted": not collisions,
             "code": "MATHLIB_UPSTREAM_COLLISION" if collisions else "ACCEPTED",

tools/frontier_validate.py

@@ -667,6 +667,20 @@ def lean_errors(result: subprocess.CompletedProcess[str], files: set[str] | None
     return text[: limit - len(note)] + note
 
 
+def deprecations(result: subprocess.CompletedProcess[str], files: set[str]) -> list[str]:
+    """Deprecation warnings Lean reported about `files`.
+
+    A deprecation is a warning under the pinned Mathlib and an error after a
+    later one, so each admitted use is a future break in the upgrade audit.
+    Other modules' deprecations are left alone: under the add-only rule the
+    submitter cannot edit them.
+    """
+    return [
+        text for severity, file, text in lean_messages(result.stdout or "")
+        if severity == "warning" and file in files and "has been deprecated" in text.splitlines()[0]
+    ]
+
+
 def parse_audit(output: str) -> dict[str, Any]:
     findings: dict[str, Any] = {}
     for line in output.splitlines():
@@ -959,10 +973,18 @@ def lean_audit(base: Path | None, candidate: Path, modules: list[str], submitted
     except (OSError, subprocess.TimeoutExpired) as error:
         report.reject("BUILD_FAILED", f"Lake build did not complete: {error}")
         return
+    own = {module.replace(".", "/") + ".lean" for module in submitted}
     if build.returncode:
-        own = {module.replace(".", "/") + ".lean" for module in submitted}
         report.reject("BUILD_FAILED", lean_errors(build, own) or "Lake build failed")
         return
+    deprecated = deprecations(build, own)
+    if deprecated:
+        text = "\n".join(deprecated)
+        if len(text) > DIAGNOSTIC_LIMIT:
+            note = f"\n[{len(text) - DIAGNOSTIC_LIMIT} more characters elided]"
+            text = text[: DIAGNOSTIC_LIMIT - len(note)] + note
+        report.reject("DEPRECATED_API", text)
+        return
     kernel_recheck(candidate, submitted, limits, report)
     if not report.accepted:
         return