fix: cslib breakage from the mathlib rwaSuggestion linter - #50
Open
Kha wants to merge 1 commit into
Open
Conversation
The `rwaSuggestion` tactic-analysis linter that arrived with the mathlib master merge emits a `Try this:` info on `Language.dfa_num_state_min`; `cslib` builds and tests with `--wfail --iofail`, so that info is a build failure. Applied the suggestion: `rw … at h1; assumption` becomes `rwa … at h1`. Same hunk as the one in #48, which has since gone CONFLICTING — `master` picked up upstream's own version of that PR's three `mathlib4` files, and `mathlib4` is green through lint without them.
Contributor
Build report for fix: cslib breakage from the mathlib
|
| Repo | Critical | Build | Test | Lint |
|---|---|---|---|---|
| cslib | ✅ in 5s | ✅ in 8s | ✅ in 3s |
Stayed red
| Repo | Critical | Build | Test | Lint |
|---|---|---|---|---|
| reference-manual | ✅ | ⏭️ | ⏭️ | ⏭️ |
| verso | 🟥 in 62s | ⏭️ | ⏭️ | |
| verso-slides | ⏭️ | ⏭️ | ⏭️ | |
| verso-web-components | ⏭️ | ⏭️ | ⏭️ |
Stayed green
| Repo | Critical | Build | Test | Lint |
|---|---|---|---|---|
| aesop | ✅ | ✅ in 7s | ✅ in 4s | ⏭️ |
| batteries | ✅ | ✅ in 4s | ✅ in 4s | ✅ in 2s |
| import-graph | ✅ | ✅ in 2s | ✅ in 4s | ⏭️ |
| lean4-cli | ✅ | ✅ in 1s | ✅ in 0s | ⏭️ |
| mathlib4 | ✅ | ✅ in 183s | ✅ in 42s | ✅ in 94s |
| plausible | ✅ | ✅ in 1s | ✅ in 2s | ⏭️ |
| ProofWidgets4 | ✅ | ✅ in 3s | ✅ in 1s | ⏭️ |
| quote4 | ✅ | ✅ in 2s | ✅ in 1s | ⏭️ |
| BibtexQuery | ✅ in 3s | ⏭️ | ⏭️ | |
| comparator | ✅ in 2s | ⏭️ | ⏭️ | |
| doc-gen4 | ✅ in 9s | ⏭️ | ⏭️ | |
| illuminate | ✅ in 3s | ✅ in 11s | ⏭️ | |
| lean4-unicode-basic | ✅ in 2s | ⏭️ | ⏭️ | |
| lean4export | ✅ in 0s | ✅ in 8s | ⏭️ | |
| LeanSearchClient | ✅ in 1s | ✅ in 0s | ⏭️ | |
| leansqlite | ✅ in 7s | ✅ in 19s | ⏭️ | |
| nerodia | ✅ in 2s | ✅ in 21s | ⏭️ | |
| repl | ✅ in 1s | ✅ in 59s | ⏭️ | |
| subverso | ✅ in 6s | ⏭️ | ⏭️ |
This was referenced Sep 6, 2026
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 -->
Kha
added a commit
that referenced
this pull request
Sep 10, 2026
Fixes the red [run 34341290563](https://github.com/leanprover/downstream-lean4/actions/runs/34341290563) on `master` (`leanprover/lean4:nightly-2026-09-09`). One commit per repo. ## reference-manual (critical) Two failures, the second only visible once the first was fixed. 1. `Manual/BuildTools/Lake/CLI.lean:835: Mismatched 'lake --help' output` — lean4#15005 re-sandboxed `lake challenge` with `bwrap` instead of `landrun`, changing the `lake challenge --help` text that the `lakeHelp challenge` block embeds verbatim. The block now carries the current output, and the surrounding prose follows it: the `bubblewrap` link and its unprivileged-user-namespaces/setuid requirement, `COMPARATOR_BWRAP` in place of `COMPARATOR_LANDRUN`, and a rewritten "Sandbox" section — the old one described Landlock's write/TCP bounds and the `AF_UNIX` escape, neither of which applies to `bwrap`. 2. `Manual/BuildTools/Lake.lean:377: Docstring on `#guard_msgs` does not match generated message` — the package facet that lean4#14990 adds is called `defaultModules`; the manual had been adapted against that PR's pr-release toolchain, where it was still `modules`. Renamed in the `initPackageFacetConfigs` list. CI never reached this module: it imports `Manual.BuildTools.Lake.CLI`, which failed first. Verified: `lake build` passes in full. The repo defines no test or lint driver (`lake check-test` / `lake check-lint` both fail), so those phases are skipped, as in CI. The new `defaultModules` facet still has no prose entry under "The facets available for packages are", unlike its neighbours. Left for the manual's authors — the block's `-- Always keep this in sync with the description below` comment was already out of sync for `modules`. ## Not changed * **cslib** and **repl** were red only downstream of mathlib4 (cslib skipped, repl's `lake test` builds Mathlib). With the mathlib4 fix in place, `cslib` passes `lake build --wfail --iofail`, `lake test --wfail --iofail` and `lake lint`, and `repl` passes `lake build` and `lake test`, all unmodified. * PR #50 is now redundant — its `rwa` in `Cslib/Computability/Languages/MyhillNerode.lean` is already in `master`. It carries no unattended marker and has a comment on it, so it has been left open.
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
1 participant
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 therwaSuggestiontactic-analysis linter that came in with themathlib master merge.
cslibbuilds and tests with--wfail --iofail, so thelinter's single
Try this:info inCslib/Computability/Languages/MyhillNerode.leanis a build failure:Applied the suggestion:
rw … at h1; assumptionbecomesrwa … at h1.Verified locally on
nightly-2026-09-06:lake build --wfail --iofail,lake test --wfail --iofailandlake lintall pass forcslib.This is the same one-line hunk as in #48, which has since become
CONFLICTING:its other three files are
mathlib4adaptations thatmasterhas meanwhileacquired from upstream (
mathlib4is green — build, test and lint — inrun 34027830326).
So #48 and #49 can be closed once this lands.
Not fixed here
verso— andreference-manual,verso-slides,verso-web-componentsskippedbehind it — remain red on the shared-
subverso-build-directory problem, sixth dayrunning.
.downstream/downstream/updater.pyredirects thesubversorequirementof
verso/test-projects/*to the one sharedsubverso/checkout, and the nestedelan run … lake buildprocesses thatVerso.Code.Externalspawns thenmaterialize and prune
subverso/.lake/buildwhile the outerversobuild readsoleans out of it:
That is not a source adaptation — 1106 of
verso's 1114 targets built — and thefix belongs in
.downstream/orrepos.toml, which this PR does not touch.reference-manualwas skipped by CI and has not been built againstnightly-2026-09-06by anyone, here or in CI.