chore: update to v4.28.0#313
Conversation
🤖 Gemini PR SummaryThis PR performs a major version bump of the project’s toolchain and core dependencies (Mathlib, CompPoly, and VCV) to Features
Fixes
Refactoring
Documentation
Analysis of Changes
Lean Declarations ✅ **Removed:** 1 declaration(s)
🎨 **Style Guide Adherence**Based on the provided style guide, here are the violations found in the code changes:
📄 **Per-File Summaries**
Last updated: 2026-02-25 02:14 UTC. |
|
I think this should be set to merge as soon as someone gets a chance to review and approve it. |
dhsorens
left a comment
dhsorens
left a comment
There was a problem hiding this comment.
This looks mostly fine to me, everything compiles locally for me fine. Most of these changes are fixing proofs, there are a couple introduced TODOs (in comments), no introduced sorry's afaict, and a couple deletions. The only real concern I have that may affect soundness is the introduction of the line set_option debug.skipKernelTC true in in the definition of proximityChecksSpec.
Reviewed for:
- correctness
- soundness
- added/resolved TODOs and
sorrys - proof repair
| -- NOTE(dtumad): Compilation time without this is painfully slow right now | ||
| set_option debug.skipKernelTC true in |
There was a problem hiding this comment.
does this do what I think it does- skip the type checker? is this a soundness problem for proximityChecksSpec?
There was a problem hiding this comment.
yep
(I assume in this case it does actually go through without this option and Devon added it for the sake of compiling faster?)
There was a problem hiding this comment.
I will make many big updates on Binius later and I will fix type checking/slow compilation problems on my side when I do rebase, one of the reason might be due to the strict index design. So you can go ahead with some temporary solutions that you have to get the PR merged if that's acceptable, like #exit or so.
There was a problem hiding this comment.
Well not exactly not type-checked, the interpreter still checks it and you can step through it in VSCode for example. The only reason this is ever useful is that there is an error in how the interpreter models the kernel, which is why this error seemed very strange to me.
I've pushed a fix now, I have no idea why it works, it should be exactly equivalent but for some reason the kernel accepts this version. Some combination of not de-structuring the sub-domain element explicitly, using the change statement, and not using omega for the bounds was the problem. Seems like potentially something to do with having subtype elements as Fin arguments but I can't get any kind of MWE of the problem.
| theorem support_C {r : R} [h : Decidable (r = 0)] : | ||
| (@C R σ _ r).support = if r = 0 then ∅ else { 0 } := by | ||
| rw [←monomial_zero', support_monomial] | ||
|
|
There was a problem hiding this comment.
just making a note that this was removed bc it is now in mathlib
| instance : NoZeroSMulDivisors (R := F) (M := A) := Module.Free.noZeroSMulDivisors F A | ||
|
|
||
| instance : NoZeroSMulDivisors (R := F) (M := Word A ι) := _root_.Function.noZeroSMulDivisors | ||
|
|
There was a problem hiding this comment.
what's the story here? I noticed that reintroducing them gave me errors, looks like some of the definitions in mathlib changed. are there alternative definitions? if we don't need them, I'm happy to have them removed too
There was a problem hiding this comment.
It is because of this change to mathlib which seems to let Module.Free produce the required instances on its own now I think.
|
can we speed this up? I would like this to be merged by tomorrow so I can begin work on the refactor |
…dtumad/4-28-0-update
@quangvdao I've fixed the merge conflicts again but I really have no control over merging this. Unlike VCV I don't have permissions to merge without approval so I've been waiting for someone to sign off. |
Update: FinalSumcheck fixed (verified) — but the Binius cone has extensive in-flight #317 API-drift breakage beyond itFinalSumcheck.lean: FIXED and verified. Commit But the focused cone build still fails — a real
Worst-hit files: Honest disposition of closeout item 1: the cone build is not a stale-cache artifact (my first audit was wrong) nor a single break (my FinalSumcheck-only framing was incomplete) — it is the in-progress #317 cone refactor, currently broken across the whole tree as the renamed-signature changes propagate. Fixing it is the active #317 effort (multiple agents committing pre-compile WIP), not closeable by isolated patches while the refactor is mid-flight. My FinalSumcheck fix is one verified file repaired; the remaining ~40 files are the live #317 propagation. Recommend #313 item 1 be tracked as "blocked on #317 cone refactor completion + a green |
6 participants
This PR updates Mathlib, CompPoly, and VCV to
v.4.28.0and fixes downstream proofs that break.The only remaining regression is in
QueryPhase.leanwhere the specificationPropnow compiles very slowly so I've enableddebug.skipKernelTCthere for now.