-
Notifications
You must be signed in to change notification settings - Fork 350
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
with
in class instances can cause surprising slowdowns
#2387
Comments
Note there is useful discussion of this issue on zulip also, in particular Matthew and Eric's suggestions. |
It has been suggested that I try to minimise the problem. My immediate reaction to this is "this would be a perfect job for a machine" (I believe Coq has an MWE-maker). But in practice I am going on holiday in a few days and will not have any time to think about this for the next two weeks. I made a preliminary start on the manual approach in this repo, which collects together a bunch of minimised hierarchies which I found lying around my computer from previous minimisation projects. Given the nature of this issue, I suspect that it would be possible to minimise. Sometimes things in mathlib are slow because there are hundreds of instances which are confusing typeclass inference or whatever -- but here I suspect that a few |
I think the problem is the following. Take structure A where
x : Bool
structure B extends A where
structure C extends A where
def a : A := ⟨true⟩
def c : C := {toA := ⟨true⟩}
def b : B := {a with}
def b' : B := {c with}
#print b
-- extra eta
-- let src := a;
-- { toA := { x := src.x } }
#print b'
-- no extra eta
-- let src := c;
-- { toA := src.toA } Note that def mkProjStx? (s : Syntax) (structName : Name) (fieldName : Name) : TermElabM (Option Syntax) := do
if (findField? (← getEnv) structName fieldName).isNone then
return none
return some <| mkNode ``Parser.Term.proj #[s, mkAtomFrom s ".", mkIdentFrom s fieldName] is used to construct the syntax for the fields from the user provided structure instances in A consequence of this is extra work during unification since it will unfold the eta expanded terms that result. On Zulip I gave a toy example of this behavior based on actual examples given by @eric-wieser and @AntoineChambert-Loir where these speed penalties pile up to start causing some of the timeouts we see throughout mathlib. In my fork, I modified structure A where
x : Bool
structure B extends A where
def a : A := ⟨true⟩
def b : B := {a with}
#print b
-- let src := a;
-- { toA := src } Let me know if PR is appropriate. |
@mattrobball, what's your opinion on this issue in light of #2451? My impression was that the problem still exists (as getting the wrong order in |
Oh I thought this was closed already. The issue was addressed. The ordering is a new problem. |
Prerequisites
Description
The following different ways to make instances of a class result in different terms:
In Mathlib's algebra hierarchy, these
let src
terms (the terms produced bywith
) seem to greatly increase the amount of time taken by typeclass inference to prove that various terms are defeq. Here are two case studies from mathlib.In mathlib PR [Merged by Bors] - perf: change to CommGroup instance on units leanprover-community/mathlib4#6398 I remove one
with
from a definition and according to the speedcenter, another file now compiles 42% faster. In the Zulip post by Xavier Roblot which prompted the PR, the change makes the first example compile an order of magnitude faster. This is just one change to onewith
.In Mathlib PR perf (MonoidAlgebra.Basic): reduce withs in structure terms leanprover-community/mathlib4#6319 , Matt Ballard removes all the
with
s in just one file in mathlib, and the benchmark results are extraordinary: http://speedcenter.informatik.kit.edu/mathlib4/compare/c7852218-4442-4a5f-8923-2062c59fbe45/to/ad01e2d7-e057-449b-b3f2-2769bf28d4e0 . A sea of green.If something could be changed in core which would save us the bother of removing many many occurrences of
with
in mathlib, that would be helpful.Versions
Lean (version 4.0.0-nightly-2023-08-03, commit 125a0ba, Release)
Additional Information
Here is a comparison of the instance traces with
trace.profiler true
andpp.proofs.withType false
in Xavier Roblot's Zulip example (case study 1 above). The diff in mathlib is this:Before the change things looked like this:
with
...
meaning that I removed a bunch of other lines all of which were of the formX =?= X
where X and X look syntactically equal.Lean wants to assign
?m.2672 := torsion K
(torsion K
is a group) and then has to check that two group structures coincide.Units.instCommGroupUnitsToMonoid
is the instance which has been dewith
ed. Before the change, Lean goes into interminable checks that various "obviously defeq" fields fromGroup
are defeq, each costing up to 0.1 seconds. After the change the same trace (in full) looks like this:and in particular the process has gone down from 0.4 seconds to 0.05 seconds, and the second part of the story in the original trace, beginning
has completely vanished.
Before the change, typeclass inference is taking 0.35 seconds to prove
Units.instCommGroupUnitsToMonoid.1 =?= Group.mk _
, and this calculation is occurring around 20 times during elaboration of the term, which explains why it was taking 7 seconds to elaborate.The text was updated successfully, but these errors were encountered: