Skip to content

fix: cslib +typeChanged on the ReflGen.symmGen_symm deprecation - #53

Closed
Kha wants to merge 1 commit into
masterfrom
push-krzuknnvttnn
Closed

fix: cslib +typeChanged on the ReflGen.symmGen_symm deprecation#53
Kha wants to merge 1 commit into
masterfrom
push-krzuknnvttnn

Conversation

@Kha

@Kha Kha commented Sep 7, 2026

Copy link
Copy Markdown
Member

Adapts cslib to a deprecation that the downstream: update repo cslib merge
(29d3da3, the head of run 34133371360)
brought in.

cslib (noncritical, --wfail --iofail)

That merge rewrote Cslib/Foundations/Relation/Confluence.lean and deprecated

lemma ReflGen.symmGen_symm : ReflGen (SymmGen r) a b → ReflGen (SymmGen r) b a

in 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 linter
compares the replacement's type with the deprecated declaration's, and an instance is not
the lemma it replaces:

warning: Cslib/Foundations/Relation/Confluence.lean:420:2: The updated constant has a different type:
  ∀ {α : Type u_1} {r : α → α → Prop} [Std.Symm r], Std.Symm (ReflGen r)
instead of
  ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, ReflGen (SymmGen r) a b → ReflGen (SymmGen r) b a

cslib builds with --wfail, so the warning is a build failure. The difference is
intended — 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) and lake lint all pass for cslib. The test
and 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 those
phases can run; the two hunks are in different files and independent. With this commit
alone, Cslib.Foundations.Relation.Confluence 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 the
rwaSuggestion linter, is #50, still MERGEABLE and still applying. 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.
This run is the first in which CI actually built it — verso, verso-slides and
verso-web-components are all green again now that subverso is out of repos.toml, so
the skip chain that had hidden it since 2026-09-03 is gone — and it failed at exactly the
six Manual/BuildTools/Lake/Config.lean sites that #51 fills in, with
Manual.BuildTools.Lake.Config the only logged failure. Nothing added here.

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`).
@downstream-lean4

Copy link
Copy Markdown
Contributor

Build report for fix: cslib +typeChanged on the ReflGen.symmGen_symm deprecation

Stayed red
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 ⏭️ ⏭️

View run

@Kha

Kha commented Sep 7, 2026

Copy link
Copy Markdown
Member Author

Superseded by #54. The downstream: update repo cslib merge ffe4553 moved the @[deprecated Relation.ReflGen.stdSymm] attribute out of Confluence.lean into Cslib/Foundations/Relation/Basic.lean, which made this branch CONFLICTING. #54 carries the same +typeChanged at the new location, plus the second site (MJoin.refl) that the same merge added.

@Kha Kha closed this Sep 7, 2026
@Kha
Kha deleted the push-krzuknnvttnn branch September 7, 2026 16:52
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 -->
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant