fix: cslib +typeChanged on the ReflGen.symmGen_symm deprecation - #53
Closed
Kha wants to merge 1 commit into
Closed
Conversation
The `downstream: update repo cslib` merge rewrote `Cslib/Foundations/Relation/Confluence.lean` and deprecated `Relation.ReflGen.symmGen_symm` in favour of the `Std.Symm (ReflGen r)` instance `Relation.ReflGen.stdSymm`. Since `lean4#14600` the deprecation linter compares the two types, and an instance is not the lemma it replaces, so it warns; `cslib` builds with `--wfail`, so that is a build failure. The type difference is intended — mark it with `+typeChanged` (syntax from `lean4#14570`).
Contributor
Build report for fix: cslib
|
| Repo | Critical | Build | Test | Lint |
|---|---|---|---|---|
| reference-manual | ✅ | 🟥 in 24s | ⏭️ | ⏭️ |
| cslib | 🟥 in 8s | ⏭️ | ⏭️ |
Stayed green
| Repo | Critical | Build | Test | Lint |
|---|---|---|---|---|
| aesop | ✅ | ✅ in 7s | ✅ in 4s | ⏭️ |
| batteries | ✅ | ✅ in 4s | ✅ in 4s | ✅ in 2s |
| import-graph | ✅ | ✅ in 2s | ✅ in 3s | ⏭️ |
| lean4-cli | ✅ | ✅ in 1s | ✅ in 0s | ⏭️ |
| mathlib4 | ✅ | ✅ in 183s | ✅ in 41s | ✅ in 90s |
| plausible | ✅ | ✅ in 1s | ✅ in 2s | ⏭️ |
| ProofWidgets4 | ✅ | ✅ in 3s | ✅ in 1s | ⏭️ |
| quote4 | ✅ | ✅ in 2s | ✅ in 1s | ⏭️ |
| BibtexQuery | ✅ in 1s | ⏭️ | ⏭️ | |
| comparator | ✅ in 2s | ⏭️ | ⏭️ | |
| doc-gen4 | ✅ in 6s | ⏭️ | ⏭️ | |
| illuminate | ✅ in 3s | ✅ in 10s | ⏭️ | |
| lean4-unicode-basic | ✅ in 2s | ⏭️ | ⏭️ | |
| lean4export | ✅ in 0s | ✅ in 8s | ⏭️ | |
| LeanSearchClient | ✅ in 1s | ✅ in 0s | ⏭️ | |
| leansqlite | ✅ in 4s | ✅ in 20s | ⏭️ | |
| nerodia | ✅ in 2s | ✅ in 21s | ⏭️ | |
| repl | ✅ in 1s | ✅ in 58s | ⏭️ | |
| verso | ✅ in 36s | ✅ in 86s | ⏭️ | |
| verso-slides | ✅ in 50s | ✅ in 6s | ⏭️ | |
| verso-web-components | ✅ in 30s | ⏭️ | ⏭️ |
Member
Author
|
Superseded by #54. The |
Kha
added a commit
that referenced
this pull request
Sep 8, 2026
Adapts `cslib` to two deprecations that the `downstream: update repo cslib` merge (ffe4553, the head of [run 34142798876](https://github.com/leanprover/downstream-lean4/actions/runs/34142798876)) brought in. Supersedes #53, which carried one of these two hunks and has been made `CONFLICTING` by that same merge. ### cslib (noncritical, `--wfail --iofail`) The merge added ```lean @[deprecated _root_.refl (since := "2026-09-07")] theorem MJoin.refl (a : α) : MJoin r a a := _root_.refl a ``` in `Cslib/Foundations/Relation/Basic.lean`, and moved the existing `@[deprecated Relation.ReflGen.stdSymm]` on `ReflGen.symmGen_symm` out of `Confluence.lean` into that same file. In both cases the replacement is a `Std.Refl`/`Std.Symm` *instance* rather than the lemma it replaces, so since lean4#14600 the deprecation linter reports a type mismatch: ``` warning: Cslib/Foundations/Relation/Basic.lean:60:2: The updated constant has a different type: ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] (a : α), r a a instead of ∀ {α : Type u_1} {r : α → α → Prop} (a : α), MJoin r a a ``` `cslib` builds with `--wfail`, so both warnings are build failures. The type difference is intended — callers are meant to go through `_root_.refl` and `Std.Symm.symm`, which is also how the two lemmas are proved — so this marks both with `+typeChanged` (syntax from lean4#14570). Because #53 fixed the `ReflGen.symmGen_symm` site at its old location in `Confluence.lean`, it no longer applies and this PR replaces it. The `MJoin.refl` site is new in this run. **Verified** on `nightly-2026-09-06`: `lake build --wfail --iofail` (3212 jobs), `lake test --wfail --iofail` (9094 jobs) and `lake lint` all pass for `cslib`. The build/test/lint runs also had #50's one-line `rwa` hunk applied in the working copy, because without it the build stops at `Cslib.Computability.Languages.MyhillNerode` before the later phases can run; the two changes are in different files and independent. With this commit alone, `Cslib.Foundations.Relation.Basic` builds clean and `MyhillNerode` is the only remaining logged failure. ### Not fixed here — already covered by open PRs **`cslib`'s other failure**, `Cslib.Computability.Languages.MyhillNerode` under mathlib's `rwaSuggestion` linter, is #50, still `MERGEABLE` and still applying to the current sources. Both it and this PR are needed for `cslib` to build. **`reference-manual`**, the one critical repo in the red set, is #51, still `MERGEABLE`. Its only logged failure in this run is `Manual.BuildTools.Lake.Config` at exactly the six `Mismatched elaborated configuration output` sites that #51 fills in for `lean4#15015`'s new `precompileImports` / `precompileLibrary` fields. Nothing added here. <!-- downstream-watch: unattended -->
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.
Adapts
cslibto a deprecation that thedownstream: update repo cslibmerge(29d3da3, the head of run 34133371360)
brought in.
cslib (noncritical,
--wfail --iofail)That merge rewrote
Cslib/Foundations/Relation/Confluence.leanand deprecatedin favour of
Relation.ReflGen.stdSymm— mathlib's[Std.Symm r] : Std.Symm (ReflGen r)instance (
Mathlib/Logic/Relation.lean:367). Since lean4#14600 the deprecation lintercompares the replacement's type with the deprecated declaration's, and an instance is not
the lemma it replaces:
cslibbuilds with--wfail, so the warning is a build failure. The difference isintended — the instance is both the lemma's own proof and what callers are meant to use
via
Std.Symm.symm— so this marks it with+typeChanged(syntax from lean4#14570).Verified on
nightly-2026-09-06:lake build --wfail --iofail(3211 jobs),lake test --wfail --iofail(9092 jobs) andlake lintall pass forcslib. The testand lint runs also had #50's one-line
rwahunk applied in the working copy, becausewithout it the build stops at
Cslib.Computability.Languages.MyhillNerodebefore thosephases can run; the two hunks are in different files and independent. With this commit
alone,
Cslib.Foundations.Relation.Confluencebuilds clean andMyhillNerodeis theonly remaining logged failure.
Not fixed here — already covered by open PRs
cslib's other failure,Cslib.Computability.Languages.MyhillNerodeunder therwaSuggestionlinter, is #50, stillMERGEABLEand still applying. Both it and this PRare needed for
cslibto build.reference-manual, the one critical repo in the red set, is #51, stillMERGEABLE.This run is the first in which CI actually built it —
verso,verso-slidesandverso-web-componentsare all green again now thatsubversois out ofrepos.toml, sothe skip chain that had hidden it since 2026-09-03 is gone — and it failed at exactly the
six
Manual/BuildTools/Lake/Config.leansites that #51 fills in, withManual.BuildTools.Lake.Configthe only logged failure. Nothing added here.