fix: reference-manual breakage from nightly-2026-09-06 - #51
Closed
Kha wants to merge 1 commit into
Closed
Conversation
`lean4#15015` added the `precompileImports` field to Lake's `LeanConfig` and `precompileLibrary` to `LeanLibConfig`. The manual embeds elaborated package configurations verbatim in `expected` blocks, so all of them were missing the new fields and `Manual.BuildTools.Lake.Config` failed with `Mismatched elaborated configuration output`. Added `precompileImports := false` after `platformIndependent` in every embedded `LeanConfig`, and `precompileLibrary := false` in the `lean_lib` configurations, in `Manual/BuildTools/Lake/Config.lean` and `Manual/BuildTools/Lake.lean`. CI never saw this: `reference-manual` has been skipped behind the `verso` failure since the shared-`subverso` build-directory problem started. Verified: `lake build` completes (1180/1180). The repo defines no test or lint driver, so `lake check-test`/`lake check-lint` fail and CI skips both phases.
Contributor
Build report for fix: reference-manual breakage from nightly-2026-09-06Stayed red
Stayed green
|
This was referenced Sep 7, 2026
Member
Author
|
Superseded: |
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
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
reference-manualtolean4#15015("lake:precompileLibrary&precompileImports", merged 2026-09-05, first innightly-2026-09-06).reference-manual (critical)
Lake's
LeanConfiggained aprecompileImportsfield andLeanLibConfigaprecompileLibraryfield. The manual embeds elaborated package configurationsverbatim in
```expectedblocks, so every one of them was two linesshort and
Manual.BuildTools.Lake.Configfailed withat six sites. Added
precompileImports := falseafterplatformIndependentinevery embedded
LeanConfig, andprecompileLibrary := falsein thelean_libconfigurations (
lean_execonfigurations do not have the field), inManual/BuildTools/Lake/Config.leanandManual/BuildTools/Lake.lean. Thelatter had not even been reached by the build, since it imports the former.
Only the embedded outputs are updated here; the two new fields are not yet
described in the TOML field documentation, which is an editorial decision for
the manual's authors.
Verified:
lake buildcompletes, 1180/1180 jobs, onnightly-2026-09-06.reference-manualdefines neither a test nor a lint driver —lake check-testand
lake check-lintboth exit 1 — solake buildis the whole of its CI.CI has not seen this failure at all, and will not see the fix either:
reference-manualhas been skipped behindversosince 2026-09-03, so thisPR's own run will skip it too. The verification above is local.
Also verified locally, unchanged
verso-web-components(build) andverso-slides(build,lake test -- --no-playwright) are green onnightly-2026-09-06. Likereference-manualthey are red in CI only through the skip chain behind
verso; unlike it, theyneeded no adaptation.
Not fixed here
cslibis already covered by #50 (MERGEABLE), which carries exactly theone-line
rwafix for therwaSuggestionlinter failure that this run stillshows. Nothing added here.
verso— the shared-subverso-build-directory problem, fourth day. All 61diagnostics in this run's
versosection arefailed to read file '…/subverso/.lake/build/lib/lean/SubVerso/Highlighting/Highlighted.olean', incompatible header; 1106 of 1114 targets built and the remaining diagnosticsare non-fatal warnings, so there is no source adaptation to make. The
incompatible headerwording pins the mechanism down further than before:.downstream/downstream/updater.pywrites apackage-overrides.jsonforevery
lake-manifest.jsonunder a subrepo, includingverso/test-projects/*/, all redirectingsubversoto the one sharedsubverso/checkout;leanprover/lean4:v4.31.0(
anchor-examples,documented-package,website-examples,website-literate) while the monorepo builds onnightly-2026-09-06;Verso.Code.Externalbuilds those projects withelan run --install …during the outer
versobuild, so a v4.31.0 Lake writes v4.31.0 oleansinto
subverso/.lake/buildwhile the outer nightly build reads them.Two toolchains sharing one build directory cannot be serialized out of this;
the fix belongs in
.downstream/orrepos.toml(stop sharing the directoryfor the nested projects), which unattended runs must not touch.