diff --git a/CONTRACT.md b/CONTRACT.md index a756733c..e3ed9d00 100644 --- a/CONTRACT.md +++ b/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 diff --git a/tests/test_mathlib_upgrade.py b/tests/test_mathlib_upgrade.py index 3ac23932..0dc00645 100644 --- a/tests/test_mathlib_upgrade.py +++ b/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() diff --git a/tests/test_validator.py b/tests/test_validator.py index d0f59b67..39554075 100644 --- a/tests/test_validator.py +++ b/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: diff --git a/tests/test_workflow_contract.py b/tests/test_workflow_contract.py index 0fe17872..e1ad3f4b 100644 --- a/tests/test_workflow_contract.py +++ b/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: diff --git a/tools/audit_mathlib_upgrade.py b/tools/audit_mathlib_upgrade.py index f78f68cd..6124888f 100644 --- a/tools/audit_mathlib_upgrade.py +++ b/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", diff --git a/tools/frontier_validate.py b/tools/frontier_validate.py index c387dd53..93bc5284 100644 --- a/tools/frontier_validate.py +++ b/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