Heartbeats and imports

Stream: new members

[Paul Nelson]

I'm curious why in this example, as we import more of the library, the heartbeat count goes up and then down. This is just supposed to be educational; I'm hitting heartbeat issues in more complicated situations than this.

8674 heartbeats:

import Mathlib.Algebra.Algebra.Subalgebra.Basic

variable {V : Type*} [AddCommGroup V] (t : Set (Module.End ℤ V))

set_option synthInstance.maxHeartbeats 200000

count_heartbeats in
#check (inferInstance : AddCommGroup (Subring.centralizer t))

30345 heartbeats:

import Mathlib.Analysis.Complex.Polynomial
import Mathlib.Algebra.Algebra.Subalgebra.Basic

variable {V : Type*} [AddCommGroup V] (t : Set (Module.End ℤ V))

set_option synthInstance.maxHeartbeats 200000

count_heartbeats in
#check (inferInstance : AddCommGroup (Subring.centralizer t))

2538 heartbeats:

import Mathlib

variable {V : Type*} [AddCommGroup V] (t : Set (Module.End ℤ V))

set_option synthInstance.maxHeartbeats 200000

count_heartbeats in
#check (inferInstance : AddCommGroup (Subring.centralizer t))

[Alex J. Best]

If you use set_option trace.Meta.synthInstance true you can see the path instance synthesis takes, this could be faster or slower depending on what instances are in the imported files, but isn't monotonic necessarily. For example an instance in a later file might more quickly lead to a solution to the synthesis problem.

[Kevin Buzzard]

That 30345 heartbeats example is bad because it actually goes over Lean's time limit. So it's interesting to see what is going wrong. You can do it like this:

import Mathlib.Analysis.Complex.Polynomial
import Mathlib.Algebra.Algebra.Subalgebra.Basic

variable {V : Type*} [AddCommGroup V] (t : Set (Module.End ℤ V))

set_option synthInstance.maxHeartbeats 200000

set_option trace.Meta.synthInstance true in
set_option trace.profiler true in
#check (inferInstance : AddCommGroup (Subring.centralizer t))

Within the output is

[Elab.command] [0.757608s] #check (inferInstance : AddCommGroup (Subring.centralizer t)) ▶

and that's a long time for typeclass inference to do something which looks so straightforward. Clicking on the ▶ unfolds it and you can chase the number until you find the following 800+ line long beauty here. Mathematically that's just Lean being really stupid for a long time. It turns out that typeclass inference is phenomenally difficult though, and this is basically the computer just trying lots of possibilities in a really stupid order (if we could figure out how to say "Lean obviously don't think about anything involving linear orders because they're not going to help" then we would, but as far as I know we can't).