Zulip Chat Archive
Stream: mathlib4
Topic: !4#5294 help wanted
David Ang (Jun 21 2023 at 22:36):
This is my first time porting an entire file and I'm trying to port AlgebraicGeometry.EllipticCurve.Weierstrass
in !4#5294. I encountered multiple issues and solved most of them but still need some help. I added a few porting notes but here are the main ones:
CoordinateRing
used to be adef
withderive [inhabited, comm_ring]
, but the correspondingderiving Inhabited, CommRing
doesn't work, and I had to replace it with anabbrev
. This might cause the same slowness problem mentioned in theclass_group.mk
topic in #maths, which is not present in this file but will show up in the futureAlgebraicGeometry.EllipticCurve.Point
file. I'm not sure how to add thelocal attribute
as mentioned in the comments so I can't say if this is fine.quotientXYIdealEquiv
is a series of three algebra equivalences linked bytrans
that gives a deterministic timeout. I tried separating it into threedef
s but the first one required ~800k heartbeats to compile, and I can't get the second one to compile at all../scripts/fix-lints.py
seems to be broken for me locally, and upon inspecting manually I don't know how to fix many of the linter problems. For instance, the linter tells me that thesimps
tag invariableChange
andbaseChange
should besimps!
, butsimps!
doesn't generate lemmas likevariableChange_Δ'
, which I needed to provevariableChange_j
.
Eric Wieser (Jun 22 2023 at 00:46):
fix-lints only fixes a very small set of linter issues
Last updated: Dec 20 2023 at 11:08 UTC