[#15066] feat: virtual one-field structures - #59
Draft
downstream-lean4[bot] wants to merge 15 commits into
Draft
downstream-lean4[bot] wants to merge 15 commits into
downstream-lean4[bot] wants to merge 15 commits into
Conversation
downstream-lean4
Bot
added
adaptation
Contributor
Author
Build report for Merge remote-tracking branch 'bot/adaptation-15066' into adaptation-15066Turned red:
Stayed green
|
Kha
added a commit
that referenced
this pull request
Sep 11, 2026
Fixes the red `master` after the bump to `nightly-2026-09-11` ([run 34590361152](https://github.com/leanprover/downstream-lean4/actions/runs/34590361152)). One commit, `mathlib4` only. ## mathlib4 **Cause.** The bump commit changes only `lean-toolchain`, yet `Mathlib.FieldTheory.Galois.IsGaloisGroup` stops compiling: ``` error: Mathlib/FieldTheory/Galois/IsGaloisGroup.lean:225:6: failed to synthesize Algebra K ↥(IsScalarTower.toAlgHom K F L).fieldRange (deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached ``` It is a small drift. With Mathlib's `leanOptions` (`maxSynthPendingDepth := 3`), `synthInstance.maxHeartbeats 21000` is already enough on `nightly-2026-09-11`. The adaptation branches for lean4#15090 (#64) and lean4#15066 (#59) hit the same error once their pr-releases were based on lean4 master past `nightly-2026-09-10`; `pr-release-15090-0d7390f` (based on the `nightly-2026-09-10` commit) was fine and `pr-release-15090-61a42c0` (based on lean4#15098) was not. That puts the cause among lean4#15001, #15093, #15060, #15048, #15107 and #15098. None of these obviously changes allocation counts inside instance synthesis, so I have not pinned it to one PR. **Fix.** `set_option synthInstance.maxHeartbeats 80000 in` on `IsGaloisGroup.of_isScalarTower`, with the justifying comment the style linter asks for. This copies #64's hunk verbatim (the resulting blob is identical to the one on `adaptation-15090`), so merging #64 later stays clean. #59 raises the same limit to 40000 and will conflict on this line either way. **Verified locally** on `nightly-2026-09-11`: `lake build Mathlib Archive Counterexamples Wanted --wfail`, `lake test --iofail` and `lake lint` all pass. ## cslib CI skipped it behind mathlib4, so it has not been built on this nightly. **Verified locally**, no change needed: `lake build --wfail --iofail`, `lake test --wfail --iofail` and `lake lint` all pass. ## repl Its `lake test` failed only as a knock-on: `test.sh` builds real Mathlib in `test/Mathlib`, which stopped at the same `IsGaloisGroup` error, and `H20231110` then failed because `Real` was unavailable. No change needed. **Verified locally**: `lake build` and `lake test` pass with this fix. ## Unfinished Nothing. <!-- downstream-watch: unattended -->
This branch has not been deployed
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.
This is the adaptation PR for leanprover/lean4#15066.