Bump mathlib #273
Bump mathlib #273
Conversation
| import Mathlib.FieldTheory.Separable | ||
| import Mathlib.NumberTheory.RamificationInertia.Basic | ||
| import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing | ||
| import Mathlib.RingTheory.DedekindDomain.IntegralClosure | ||
| import Mathlib.Topology.Algebra.Algebra | ||
| import Mathlib.Topology.Algebra.Module.ModuleTopology | ||
| import FLT.Mathlib.Algebra.Algebra.Subalgebra.Pi | ||
| import FLT.Mathlib.Algebra.Order.Hom.Monoid |
There was a problem hiding this comment.
The algebra instance started timing out with import Mathlib
| import Mathlib.FieldTheory.Separable | ||
| import Mathlib.NumberTheory.RamificationInertia.Basic | ||
| import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing | ||
| import Mathlib.RingTheory.DedekindDomain.IntegralClosure | ||
| import Mathlib.Topology.Algebra.Algebra | ||
| import Mathlib.Topology.Algebra.Module.ModuleTopology | ||
| import FLT.Mathlib.Algebra.Algebra.Subalgebra.Pi | ||
| import FLT.Mathlib.Algebra.Order.Hom.Monoid |
YaelDillies
force-pushed
the
bump_2024_12_08
branch
from
2c44261 to
edf7291
Compare
|
What the heck does "uncaught exception: parser 'subscript' was not found" (when compiling some random analysis file in mathlib) mean? Independent of that, are you happy @pitmonticone with the changes to lake-manifest.json? |
Yes, happy with those. I wasn't aware of that version pin and I don't think is justified, so I endorse the changes by Yaël. |
See https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/lean4checker.20failure/near/485826350 . Short version is that mathlib is currently borked and this will have to be fixed in mathlib and/or lean. |
YaelDillies
force-pushed
the
bump_2024_12_08
branch
from
edf7291 to
cce1182
Compare
|
Still "uncaught exception: parser 'subscript' was not found |
|
The issue to watch is leanprover/lean4#6325 |
Closes #271