Repository navigation
fix: cslib breakage from the mathlib4 nightly-testing merge - #155
Closed
downstream-lean4[bot] wants to merge 1 commit into
Closed
downstream-lean4[bot] wants to merge 1 commit into
downstream-lean4[bot] wants to merge 1 commit into
Conversation
`downstream: update repo mathlib4` (bf1783d) brought in [mathlib4#44387](leanprover-community/mathlib4#44387), which extends Mathlib's `unusedTactic` linter to the `<;>` combinator: a `<;>` whose left-hand tactic leaves at most one goal is reported as redundant, because `;` — or nothing at all — would do the same. (The PR also turns off batteries' `UnnecessarySeqFocus`, which linted the same thing, for the speedup.) The `decreasing_by` block of `Proposition.expand` in `Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean` was `all_goals simp <;> grind`, and `simp` leaves at most one goal on every termination branch, so the new warning fires there: warning: Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean:77:17: Unused tactic linter: `<;>` should be replaced with `;` or be removed. It is the only site in the whole library, and with `--wfail` the one warning is the whole failure — there is no `✖` anywhere. `;` is not in fact a valid replacement here: `simp` closes two of the branches outright, and `all_goals simp; grind` therefore fails with two `No goals to be solved`. `simp` alone does not close any of the remaining `sizeOf` inequalities. `grind` on its own discharges all of them, and `all_goals grind` is the idiom the rest of cslib already uses for `decreasing_by`-style goals, so use that. Verified on `nightly-2026-10-09` with the options CI uses: `lake build --wfail --iofail` (6664 jobs, no warnings anywhere), `lake test --wfail --iofail` (18651 jobs, which compiles all of Mathlib) and `lake lint` all pass. Upstream `cslib` `main` still carries the `<;>`; its own CI cannot see this, as it builds against a release toolchain and a released Mathlib. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Contributor
Author
Build report for fix: cslib breakage from the mathlib4 nightly-testing mergeTurned green:
Stayed red
Stayed green
|
Contributor
Author
|
Superseded upstream: cslib#1109 ( |
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
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.
Run 38017379965 on
nightly-2026-10-09.cslibis the only repo of the red set that is not already covered by an open PR — see "The rest of the red set" below.cslib
downstream: update repo mathlib4(bf1783d) brought in mathlib4#44387, which extends Mathlib'sunusedTacticlinter to the<;>combinator: a<;>whose left-hand tactic leaves at most one goal is reported as redundant, since;— or nothing at all — would do the same. (The PR also switches off batteries'UnnecessarySeqFocus, which linted the same property at much greater cost.)The
decreasing_byblock ofProposition.expandinCslib/Logics/LinearLogic/CLL/EtaExpansion.leanwasall_goals simp <;> grind, andsimpleaves at most one goal on every termination branch, so the new warning fires there:It is the only site in the whole library, and
cslibbuilds with--wfail, so that one warning is the entire failure — there is no✖anywhere in the CI log.;is not actually a valid replacement here:simpcloses two of the branches outright, soall_goals simp; grindfails with twoNo goals to be solved.simpalone does not close any of the remainingsizeOfinequalities.grindon its own discharges all of them, andall_goals grindis the idiom the rest ofcslibalready uses, so the fix dropssimp <;>.Upstream
cslibmainstill carries the<;>, and its own CI cannot see this: it builds against a release toolchain and a released Mathlib, while mathlib4#44387 landed on 2026-10-09.Verified on
nightly-2026-10-09with the options CI uses:lake build --wfail --iofail(6664 jobs, no warning anywhere),lake test --wfail --iofail(18651 jobs, which compiles all of Mathlib) andlake lintall pass.The rest of the red set
Unchanged here, each already carried by an open PR whose subrepo directory is byte-identical to
master's:test,MathlibTest.AssertImported) — fix: mathlib4 breakage from the import-graph main merge #149build,DemoSite.Blog.Subprojects) — fix: verso breakage from the verso main merge (supersedes #142) #145verso) — fix: reference-manual breakage from nightly-2026-10-08 #148verso, no failure of their ownmasterneeds all four PRs to go green.