From 35a2ca075f90734d731299070245b08e41ccf7b1 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Sat, 10 Oct 2026 03:03:43 +0000 Subject: [PATCH] fix: cslib breakage from the mathlib4 nightly-testing merge MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `downstream: update repo mathlib4` (bf1783d6) brought in [mathlib4#44387](https://github.com/leanprover-community/mathlib4/pull/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 --- cslib/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cslib/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean b/cslib/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean index 1148ef3ef..8efd58c88 100644 --- a/cslib/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean +++ b/cslib/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean @@ -74,7 +74,7 @@ def Proposition.expand (a : Proposition Atom) : ⇓({a, a⫠} : Sequent Atom):= |> Proof.rwConclusion (by grind) termination_by a decreasing_by - all_goals simp <;> grind + all_goals grind /-- A `Proof` has only atomic axioms if all its instances of the axiom treat atomic propositions. -/ @[scoped grind =]