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

[carlok]

A deprecation is a warning under the pinned Mathlib and becomes an error after a later one, so every admitted use is a future break in the upgrade audit. #224 had to fix 13 by hand, and 2 of them were in a module merged an hour earlier.

Receiver: DEPRECATED_API

After a successful lake build, the receiver rejects any deprecation warning Lean reports about the submission's own files, quoting Lean's message, which names the replacement. For example:

DEPRECATED_API | warning: LeanFrontier/Algebra/New.lean:3:40: `if_pos` has been deprecated: Use `ite_eq_left` instead
warning: LeanFrontier/Algebra/New.lean:1:0: 'Mathlib.Data.Real.Basic' has been deprecated: please replace this import by

import Mathlib.Basic.Real.Basic

• Deprecations in other modules are ignored: under the add-only rule (fix: reject build- and import-time code, and make submissions add-only #216) the submitter can't edit them.
• Style lints (unused simp argument, <;> and so on) aren't affected.
• The rejection stops before the kernel recheck, and the message has the same 4000-character cap as build errors.
• CONTRACT.md §4 states the rule, and the code joins the stable list.

Upgrade audit: corpus_deprecations

A new Mathlib release can deprecate things the existing corpus uses. The upgrade audit now lists those deprecations in its report without blocking the upgrade. The list is the follow-up maintenance/ work. It's sorted, because Lake's parallel build order isn't deterministic and the re-audit in test.yml compares the report byte for byte.

State of main

main has 0 deprecation warnings. #224 left the corpus at 0 on a full build of exactly what it merged, and no Lean source has landed since.

Tests

• A rejection test built from real v4.34.0 warning text: two deprecations in the submission, one in another module and one style lint. Only the first two are reported.
• The real captured build log from fix: report the submitter's own Lean errors, not the tail of the build #193 contains a Furstenberg deprecation, and it doesn't reject an unrelated submission.
• Contract tests pin the code in the validator and CONTRACT.md, and pin that the upgrade audit reports deprecations without blocking.

The new tests failed before the change. The full suite passes: 140 tests, 6 skipped.

🤖 Generated with Claude Code