fix: mathlib4 breakage from nightly-2026-09-03 - #40
Merged
Conversation
The merge with mathlib master brought in new `@[deprecated]` aliases in `Mathlib.Order.Filter.EventuallyConst` (`EventuallyConst` on sets renamed to `EventuallyEmptyOrUniv`) and `Mathlib.LinearAlgebra.Contraction` (`dualDistribEquivOfBasis`/`dualTensorHomEquivOfBasis` superseded by their basis-free counterparts). Since lean4#14600 an `@[deprecated X]` whose replacement has a different type warns, and mathlib4 builds with `--wfail` downstream, so both modules failed. The type differences are intentional, so mark all 18 sites with `+typeChanged`. Mathlib master builds on a release toolchain where this warning does not exist yet, so such batches keep arriving downstream with deprecation waves.
Contributor
Build report for fix: mathlib4 breakage from nightly-2026-09-03Turned green:
Stayed red
Stayed green
|
TwoFX
approved these changes
Sep 4, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes the
mathlib4half of the red run 33829572992 onmaster.mathlib4
Root cause. The
downstream: update repo mathlib4merge brought in three deprecation waves from mathlib master:Mathlib.Order.Filter.EventuallyConst—EventuallyConstspecialised to sets was renamed toEventuallyEmptyOrUniv, so the@[deprecated]aliases state the old lemmas in terms of a different predicate.Mathlib.LinearAlgebra.Contraction—dualTensorHomEquivOfBasis_eq_dualTensorHomEquivreverses the direction of the equation it replaces, anddualDistribEquivOfBasis(and its@[simps!]lemmas) were superseded by the basis-freedualDistribEquiv.Since lean4#14600 an
@[deprecated X]whose replacement has a different type warns (The updated constant has a different type: …, with the+typeChangedsyntax from lean4#14570).mathlib4builds with--wfailhere, so both modules count as failed and everything downstream of them — includingcslib— was skipped.Mathlib master builds on a release toolchain, where this warning does not exist yet, so batches like this keep arriving downstream whenever a deprecation wave lands upstream.
Fix.
+typeChangedon all 18 sites; the type differences are all intentional. The marker is not recorded in the environment, so the.oleans are unchanged and dependents replay from cache.Verified locally on
nightly-2026-09-03:mathlib4:lake build Mathlib Archive Counterexamples Wanted --wfail,lake test --iofail,lake lint— all green.cslib(skipped behindmathlib4in CI):lake build --wfail --iofail,lake test --wfail --iofail,lake lint— all green with no source change needed.Not covered by this PR
The rest of the red set (
subverso,verso,verso-slides,verso-web-components, andreference-manualbehind them) is unchanged from the previous round: thesubversoadaptation is in #39, andversothen fails on the nested-test-project/toolchain issue already reported on Zulip. Nothing here touches it.