JacobiZariski in lean4lean

Stream: mathlib4

[Mario Carneiro]

on mathlib v4.20.1:

$ lean4lean Mathlib.RingTheory.Kaehler.JacobiZariski
Mathlib.RingTheory.Kaehler.JacobiZariski:defnDecl Algebra.Generators.CotangentSpace.compEquiv: lean4lean took 2124
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.CotangentSpace.compEquiv_symm_inr: lean4lean took 5826
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.CotangentSpace.fst_compEquiv: lean4lean took 4979
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.H1Cotangent.δAux_toAlgHom: lean4lean took 11320
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.H1Cotangent.δAux_ofComp: lean4lean took 4601
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.H1Cotangent.exact_map_δ': lean4lean took 4770
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.H1Cotangent.δ_map: lean4lean took 5080
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.H1Cotangent.δ_comp_equiv: lean4lean took 6669
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.CotangentSpace.compEquiv.eq_1: lean4lean took 3253
checked 82 declarations
took 81.418 sec

After cherry picking #26008:

$ lean4lean Mathlib.RingTheory.Kaehler.JacobiZariski
Mathlib.RingTheory.Kaehler.JacobiZariski:defnDecl Algebra.Generators.CotangentSpace.compEquiv: lean4lean took 2375
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.CotangentSpace.compEquiv_symm_inr: lean4lean took 5738
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.CotangentSpace.fst_compEquiv: lean4lean took 3739
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.H1Cotangent.δAux_ofComp: lean4lean took 4950
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.H1Cotangent.exact_map_δ': lean4lean took 2243
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.CotangentSpace.compEquiv.eq_1: lean4lean took 1784
checked 82 declarations
took 80.437 sec

Not a huge difference...

[Mario Carneiro]

Here's another version of that test, where I slapped a bunch of tick calls all over the kernel so e.g. each call of inferType or each step of whnf takes one tick per subterm.

on mathlib v4.20.1:

$ lean4lean Mathlib.RingTheory.Kaehler.JacobiZariski
Mathlib.RingTheory.Kaehler.JacobiZariski:defnDecl Algebra.Generators.CotangentSpace.compEquiv: lean4lean took 1490 ms, 864277 ticks
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.CotangentSpace.compEquiv_symm_inr: lean4lean took 5284 ms, 2128966 ticks
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.CotangentSpace.fst_compEquiv: lean4lean took 5316 ms, 1769704 ticks
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.H1Cotangent.δAux_toAlgHom: lean4lean took 7666 ms, 2773355 ticks
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.H1Cotangent.δAux_ofComp: lean4lean took 3284 ms, 1629806 ticks
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.H1Cotangent.exact_map_δ': lean4lean took 3229 ms, 1981826 ticks
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.H1Cotangent.δ_map: lean4lean took 3323 ms, 1933503 ticks
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.H1Cotangent.δ_comp_equiv: lean4lean took 3347 ms, 1816177 ticks
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.CotangentSpace.compEquiv.eq_1: lean4lean took 1386 ms, 866884 ticks
checked 82 declarations in 16830555 time units

After cherry picking #26008:

$ lean4lean Mathlib.RingTheory.Kaehler.JacobiZariski
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.Cotangent.exact: lean4lean took 1912 ms, 94028 ticks
Mathlib.RingTheory.Kaehler.JacobiZariski:defnDecl Algebra.Generators.CotangentSpace.compEquiv: lean4lean took 5880 ms, 864299 ticks
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.CotangentSpace.compEquiv_symm_inr: lean4lean took 12952 ms, 2128994 ticks
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.CotangentSpace.fst_compEquiv: lean4lean took 5083 ms, 1769362 ticks
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.H1Cotangent.δAux_ofComp: lean4lean took 3437 ms, 1629424 ticks
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.H1Cotangent.exact_map_δ': lean4lean took 1779 ms, 999115 ticks
Mathlib.RingTheory.Kaehler.JacobiZariski:thmDecl Algebra.Generators.CotangentSpace.compEquiv.eq_1: lean4lean took 1507 ms, 866906 ticks
checked 82 declarations in 9430757 time units

[Mario Carneiro]

these numbers seem pretty large just in absolute value... For comparison, Mathlib.Data.List.Basic takes 131978 ticks

[Mario Carneiro]

the most noticable change is exact_map_δ', which got halved from 1933503 to 999115 ticks

[Mario Carneiro]

although if this is really just a change of universe name order then it's surprising things change at all

[Mario Carneiro]

(#26008 isn't just a change of universe names though)

[Mario Carneiro]

is anyone willing to edit this into a cleaner test case where the only thing changed is universe names?

[Matthew Ballard]

The timing seems much less than the OG kernel (from memory).

What is the most common tick?

[Mario Carneiro]

what do you mean by that?

[Mario Carneiro]

these ticks are unrelated to lean kernel heartbeats

[Matthew Ballard]

Sorry two completely separate sentences.

What is most often getting whnf’ed?

[Mario Carneiro]

Here is the information about all declarations (no cutoff):

Cotangent.exact._proof_1: 6 ms, 3290 ticks
H1Cotangent.δ._proof_27: 5 ms, 2697 ticks
H1Cotangent.δ._proof_22: 2 ms, 418 ticks
H1Cotangent.δ._proof_28: 7 ms, 2879 ticks
H1Cotangent.δ._proof_29: 21 ms, 4948 ticks
H1Cotangent.δ._proof_26: 0 ms, 183 ticks
Cotangent.surjective_map_ofComp: 41 ms, 16793 ticks
CotangentSpace.compEquiv._proof_2: 8 ms, 2809 ticks
CotangentSpace.compEquiv._proof_11: 4 ms, 2385 ticks
H1Cotangent.δAux._proof_13: 0 ms, 352 ticks
CotangentSpace.compEquiv._proof_8: 1 ms, 6 ticks
H1Cotangent.δ._proof_23: 6 ms, 2455 ticks
CotangentSpace.compEquiv._proof_4: 1 ms, 386 ticks
H1Cotangent.δ._proof_30: 50 ms, 14647 ticks
Cotangent.exact._proof_7: 0 ms, 10 ticks
Cotangent.exact._proof_2: 4 ms, 3304 ticks
Cotangent.exact._proof_4: 1 ms, 98 ticks
Cotangent.exact._proof_10: 1 ms, 88 ticks
Cotangent.exact._proof_6: 1 ms, 8 ticks
Cotangent.exact._proof_5: 0 ms, 98 ticks
Cotangent.exact._proof_9: 0 ms, 0 ticks
Cotangent.exact._proof_8: 0 ms, 0 ticks
Cotangent.exact._proof_3: 0 ms, 122 ticks
Cotangent.exact: 255 ms, 104899 ticks
H1Cotangent.δ._proof_24: 2 ms, 461 ticks
CotangentSpace.compEquiv._proof_10: 3 ms, 2385 ticks
CotangentSpace.compEquiv._proof_1: 2 ms, 386 ticks
H1Cotangent.δ._proof_31: 1 ms, 400 ticks
CotangentSpace.compEquiv._proof_5: 6 ms, 2407 ticks
CotangentSpace.compEquiv._proof_6: 8 ms, 2809 ticks
CotangentSpace.compEquiv._proof_3: 2 ms, 386 ticks
CotangentSpace.compEquiv._proof_9: 0 ms, 6 ticks
CotangentSpace.compEquiv._proof_7: 6 ms, 2739 ticks
CotangentSpace.compEquiv._proof_12: 1 ms, 183 ticks
CotangentSpace.compEquiv: 1176 ms, 864277 ticks
CotangentSpace.compEquiv_symm_inr: 3396 ms, 2128966 ticks
CotangentSpace.fst_compEquiv: 2508 ms, 1769704 ticks
CotangentSpace.exact: 57 ms, 21989 ticks
H1Cotangent.δ._proof_32: 11 ms, 4717 ticks
H1Cotangent.δ._proof_33: 15 ms, 5707 ticks
CotangentSpace.map_toComp_injective: 44 ms, 17691 ticks
H1Cotangent.map_comp_cotangentComplex_baseChange: 128 ms, 43303 ticks
H1Cotangent.δ._proof_34: 19 ms, 7241 ticks
H1Cotangent.δ._proof_25: 2 ms, 1864 ticks
H1Cotangent.δ: 199 ms, 62108 ticks
H1Cotangent.δ.eq_1: 243 ms, 61738 ticks
H1Cotangent.δAux._proof_16: 1 ms, 352 ticks
H1Cotangent.δAux._proof_14: 3 ms, 2557 ticks
H1Cotangent.δAux._proof_17: 13 ms, 4004 ticks
H1Cotangent.δAux._proof_21: 4 ms, 2134 ticks
H1Cotangent.δAux._proof_18: 3 ms, 1931 ticks
H1Cotangent.δAux._proof_19: 6 ms, 3080 ticks
H1Cotangent.δAux._proof_20: 1 ms, 332 ticks
H1Cotangent.δAux._proof_15: 6 ms, 3163 ticks
H1Cotangent.δAux: 21 ms, 10262 ticks
H1Cotangent.δAux_monomial: 32 ms, 11022 ticks
H1Cotangent.δAux_mul: 55 ms, 23267 ticks
H1Cotangent.δAux_C: 20 ms, 11080 ticks
H1Cotangent.δAux_ofComp._proof_22: 140 ms, 70982 ticks
H1Cotangent.exact_map_δ: 286 ms, 67454 ticks
CotangentSpace.compEquiv_symm_zero: 84 ms, 23462 ticks
H1Cotangent.δAux_X: 21 ms, 9803 ticks
H1Cotangent.δAux_toAlgHom._proof_22: 118 ms, 70982 ticks
H1Cotangent.δAux_toAlgHom: 6186 ms, 2773355 ticks
H1Cotangent.exact_δ_map: 437 ms, 125513 ticks
H1Cotangent.δAux_ofComp._proof_23: 0 ms, 8 ticks
H1Cotangent.δAux_ofComp: 2827 ms, 1629806 ticks
H1Cotangent.δ_eq: 257 ms, 72130 ticks
H1Cotangent.δ_eq_δAux: 260 ms, 81404 ticks
H1Cotangent.δ_eq_δ: 75 ms, 23091 ticks
H1Cotangent.δ_map._proof_35: 1 ms, 90 ticks
H1Cotangent.δ_map._proof_36: 1 ms, 88 ticks
H1Cotangent.exact_map_δ': 2890 ms, 1981826 ticks
δ: 5 ms, 2346 ticks
exact_map_δ: 8 ms, 2933 ticks
H1Cotangent.δ_map: 2724 ms, 1933503 ticks
H1Cotangent.δ_comp_equiv: 2472 ms, 1816177 ticks
CotangentSpace.fst_compEquiv_apply: 79 ms, 21248 ticks
CotangentSpace.map_ofComp_surjective: 35 ms, 13801 ticks
CotangentSpace.compEquiv.eq_1: 1203 ms, 866884 ticks
Hom.toAlgHom.eq_1: 8 ms, 2862 ticks
exact_δ_mapBaseChange: 11 ms, 3281 ticks
checked 82 declarations in 16830555 time units

[Mario Carneiro]

Matthew Ballard said:

What is most often getting whnf’ed?

I don't know how to test that in a way that doesn't result in way too much data

[Matthew Ballard]

Ok. Can you tell me the steps you needed to do get l4l running on this so I can try poking when I have some free time?

[Mario Carneiro]

I check out v4.20.1 of mathlib, then run

lake build lean4lean
lake -d=../mathlib4 env .lake/build/bin/lean4lean Mathlib.RingTheory.Kaehler.JacobiZariski

from lean4lean repo. You will need some unpushed stuff in order to get the statistics

[Mario Carneiro]

here are some stats on how many times each definition is unfolded in this file:

639572 * unfolded Algebra.Extension.Ring
259248 * unfolded NonUnitalNonAssocSemiring.toAddCommMonoid
177311 * unfolded CommSemiring.toSemiring
152330 * unfolded Ring.toSemiring
95530 * unfolded DFunLike.coe
45181 * unfolded Algebra.Generators.Ring
44394 * unfolded Equiv.toFun
27713 * unfolded HAdd.hAdd
25293 * unfolded AddHom.toFun
25009 * unfolded Add.add
19528 * unfolded MulAction.toSMul
19390 * unfolded HSMul.hSMul
19366 * unfolded Membership.mem
18462 * unfolded SMul.smul
17842 * unfolded Setoid.r
16471 * unfolded ZeroHom.toFun
16129 * unfolded MvPolynomial.algebra
16129 * unfolded AddMonoidAlgebra.algebra
16106 * unfolded Algebra.Extension.instRingOfIsScalarTower
16106 * unfolded Algebra.compHom
14910 * unfolded HMul.hMul
14757 * unfolded AddCon.toSetoid
13826 * unfolded Mul.mul
12336 * unfolded HAppend.hAppend
12336 * unfolded Append.append
12283 * unfolded AddSemigroup.toAdd
10670 * unfolded Semiring.toNonAssocSemiring
8974 * unfolded SetLike.coe
8736 * unfolded HasEquiv.Equiv

[Notification Bot]

16 messages were moved here from #mathlib4 > Task 26: Replace Type u by Type* wherever possible by Johan Commelin.