Kernel type checking performance depends on lexicographic ordering of universe variables

Observation

The number of instructions required to build Mathlib/RingTheory/Kaehler/JacobiZariski.lean depends on the lexicographic order of the universe variables. The maximal observed variation is 15 * 10^10 instructions. For context, at the time of writing this issue, this variation alone would put a file in the top 100 slowest files of mathlib.

Hypothesis

When the kernel type checks declarations and there is a (syntactic) mismatch in universe levels, it seems to unfold everything even if the left and right hand side are otherwise syntactically equal. A slightly minimized example of this effect can be seen here (This minimized problem can be fixed by changing a transparency setting, but not the original one. See below for more details.)

Possible causes

• Universe levels are associated (hence normalized) differently, depending on context, see https://github.com/leanprover/lean4/issues/5695. Some evidence that changing associativity changes performance here: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/JacobiZariski.20is.20slow.2E/near/497971914 and here: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/JacobiZariski.20is.20slow.2E/near/499335973.
• Lean normalizes universe expressions and this normalization depends on the lexicographic order of the variable names (evidence for the alphabetical sorting: https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2321099.20use.20unification.20hints.20for.20generators/near/496131379).

Attempts at improving the performance

Change lexicographic order of universe variables

By changing the lexicographic order of universe variables in #21129, the instruction count changed by - 21 * 10^10 (- 29%), later measurements in #26008 show reduced absolute gains of - 13 * 10^10 and comparable relative gains - 26% instructions.

Make Extension.CotangentSpace less reducible

It was repeatedly raised that Extension.CotangentSpace should be a def instead of an abbrev. This was tried here (#21364) and reported here: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/kernel.20universe.20normalization.20issue/near/497399181. The effect is negligible.

As of now, all minimization could be fixed by replacing the abbrev by def though.

Unbundle type fields from Generators and Extension

• The bundled type fields in Algebra.Generators and Algebra.Extension caused suspicion. Subsequently, the type fields of Algebra.Generators were unbundled in #25085 with overall performance change of - 9 * 10 ^ 10 instructions, but with no effect on JacobiZariski.lean.
• In a follow-up attempt, unbundling the remaining type variable from Algebra.Extension was made in #25191. The performance effect was catastrophic featuring a change of + 55 * 10 ^ 10 (+ 90%) instructions in JacobiZariski.lean.

Other, possibly unrelated performance issues in JacobiZariski

There are most certainly various performance issues appearing in this file and not all of them are related to universes. The file remains slow even if replacing all universe variables by the same one.

• simp being slow, probably caused by unfolding typeclass instances all the way down: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/JacobiZariski.20is.20slow.2E/near/505893790 (most likely the issue here is that Algebra.Extension.Ring and Algebra.Generators.Ring are not syntactically equal, although they are reducibly def-eq).

Discussions on this

• Zulip thread (Lean4/kernel universe normalization issue): https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/kernel.20universe.20normalization.20issue/with/496355201
• Zulip thread (mathlib4/JacobiZariski is slow): https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/JacobiZariski.20is.20slow.2E/with/514149742
• Zulip thread (PR reviews/use unification hints for generators). Skip the first few messages, they are unrelated: https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2321099.20use.20unification.20hints.20for.20generators/with/496095368
• Github PR to change the ordering, gaining a 29% speedup.
  Before the fork migration: https://github.com/leanprover-community/mathlib4/pull/21129
  After the fork migration: https://github.com/leanprover-community/mathlib4/pull/26008
• Performance test after unbundling type parameters in Generators and Extension: https://github.com/leanprover-community/mathlib4/pull/25191#issuecomment-2907889612 (+ 55 * 10^10 instructions !)
• Performance test after replacing all universe variables by a single one: https://github.com/leanprover-community/mathlib4/pull/21165#issuecomment-2618741580 (- 44 * 10 ^10 instructions !)
• Performance test after making CotangentSpace a def: https://github.com/leanprover-community/mathlib4/pull/21364. Speedcenter does not give the measurements, but local measurements show: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/kernel.20universe.20normalization.20issue/near/497399181 ( +- 0 * 10 ^ 10 instructions)

Instructions for testing performance locally

Run lake env perf stat lean Mathlib/RingTheory/Kaehler/JacobiZariski.lean. The most relevant number is cpu_core/instructions which on master at the time of writing is at ~ 54 * 10^10.

Start by running lake env perf stat lean Mathlib/RingTheory/Kaehler/JacobiZariski.lean and compare the cpu_core/instructions result under different universe-variable orderings. Read the linked Lean kernel and Zulip discussions, then identify and address the kernel type-checking behavior causing the performance variation; done means the ordering-dependent cost is reduced or eliminated.