Zulip Chat Archive

Stream: general

Topic: type class slowdown: mv_polynomial algebras


view this post on Zulip Rob Lewis (Jul 20 2020 at 13:49):

import data.mv_polynomial

universes u v w

section
variables {σ : Type u} (R : Type v) [comm_ring R]
  (A : Type w) [comm_ring A] [algebra R A]

set_option trace.class_instances true
#check (infer_instance : algebra R (mv_polynomial σ R))

end

The type class search here takes ~2 seconds on my laptop. It's definitely the algebra search that's slow, elaborating the type is fine. What's strange is the search succeeds in two steps. It fails to unify the target with algebra R A, and then finds the corect instance mv_polynomial.algebra. These respectively fail and succeed instantly when I try them outside of the type class search.

view this post on Zulip Rob Lewis (Jul 20 2020 at 13:49):

This seems to be fallout from https://github.com/leanprover-community/mathlib/commit/ce48b6ba77a02430c098f26f3fcc3c11e516179b . The search is instant before that.

view this post on Zulip Rob Lewis (Jul 20 2020 at 13:49):

But I can't tell why it's slow now. Any ideas?

view this post on Zulip Johan Commelin (Jul 20 2020 at 14:16):

This one is instant:

import data.mv_polynomial

universes u v w

section
variables {σ : Type u} (R : Type v) [comm_semiring R]
  (A : Type w) [comm_ring A] [algebra R A]

set_option trace.class_instances true
#check (infer_instance : algebra R (mv_polynomial σ R))

end

view this post on Zulip Johan Commelin (Jul 20 2020 at 14:17):

The diff: comm_semiring R instead of comm_ring R

view this post on Zulip Sebastien Gouezel (Jul 20 2020 at 14:19):

It's really strange, because the instance search output is pretty short in any case, and for the same question apply_instance works instantaneously.

I have no clue about what's going on.

view this post on Zulip Rob Lewis (Jul 20 2020 at 14:25):

It's not the comm_semiring -> semiring search that's at fault. This def is instant and doesn't affect the bad search.

@[instance, priority 1000000] def csr : comm_semiring R := infer_instance

view this post on Zulip Rob Lewis (Jul 20 2020 at 14:25):

Which makes me suspect that some instance is taking a long time to unify or fail to unify.

view this post on Zulip Rob Lewis (Jul 20 2020 at 14:25):

But I'm not sure how to debug this.

view this post on Zulip Sebastien Gouezel (Jul 20 2020 at 14:33):

How do you explain that

import data.mv_polynomial

universes u v w

section
variables {σ : Type u} (R : Type v) [comm_ring R]

set_option trace.class_instances true

noncomputable lemma foo : algebra R (mv_polynomial σ R) :=
let a := (infer_instance : algebra R (mv_polynomial σ R)) in
infer_instance

end

is also instant?

view this post on Zulip Rob Lewis (Jul 20 2020 at 14:36):

My guess is a caching thing. The type class cache should be frozen after the :=.

view this post on Zulip Sebastien Gouezel (Jul 20 2020 at 14:41):

Yes, it's a cache thing:

import data.mv_polynomial

universes u v w

section

set_option trace.class_instances true

noncomputable example {σ : Type u} (R : Type v) [comm_ring R] : true :=
begin
  unfreezingI {let a := (infer_instance : algebra R (mv_polynomial σ R)) },
  trivial
end

end

is also slow.

view this post on Zulip Johan Commelin (Jul 20 2020 at 14:44):

Now I have a headache...

view this post on Zulip Sebastien Gouezel (Jul 20 2020 at 14:46):

And the profiler is totally unhelpful:

set_option profiler true

lemma foo {σ : Type u} (R : Type v) [comm_ring R] : true :=
begin
  unfreezingI { let a := (infer_instance : algebra R (mv_polynomial σ R)) },
  trivial
end

gives the output

elaboration: tactic execution took 4.25s
num. allocated objects:  35
num. allocated closures: 117
 4249ms   100.0%   tactic.to_expr
 4249ms   100.0%   tactic.interactive.let._lambda_1
 4249ms   100.0%   _interaction._lambda_3
 4249ms   100.0%   tactic.focus1
 4249ms   100.0%   tactic.step
 4249ms   100.0%   tactic.unfreezing._lambda_2
 4249ms   100.0%   tactic.istep._lambda_1
 4249ms   100.0%   tactic.istep
 4249ms   100.0%   _interaction._lambda_2
 4249ms   100.0%   scope_trace
 4249ms   100.0%   _interaction

view this post on Zulip Rob Lewis (Jul 20 2020 at 15:05):

So this is as minimal as I have it.

import data.mv_polynomial

universes u v w

section
variables {σ : Type u} (R : Type v) [cr : comm_ring R]
include cr
noncomputable def p : semiring (mv_polynomial σ R) := infer_instance

#check (infer_instance :
@algebra R (@ mv_polynomial σ R (@comm_ring.to_comm_semiring _ cr))
           (@comm_ring.to_comm_semiring _ cr) (@p σ R cr))

There's exactly one type class search in the #check. It tries to apply exactly one instance.

view this post on Zulip Rob Lewis (Jul 20 2020 at 15:07):

Uhm. And using by apply_instance instead of infer_instance makes it instant.Maybe because this freezes the instance cache?

view this post on Zulip Sebastien Gouezel (Jul 20 2020 at 15:13):

Yes, getting into tactic mode should freeze the cache.

Should we invoke @Gabriel Ebner ?

view this post on Zulip Rob Lewis (Jul 20 2020 at 15:16):

Poor Gabriel is too popular for his own health, hah.

view this post on Zulip Jannis Limperg (Jul 20 2020 at 15:26):

I should walk over and remind him that all this research business is interfering with his Lean maintenance duties. :upside_down:

view this post on Zulip Sebastien Gouezel (Jul 20 2020 at 15:28):

Isn't he on holidays? We should definitely not interfere with the holidays!

view this post on Zulip Gabriel Ebner (Jul 20 2020 at 16:04):

Is this lean#397? If not, please file an issue. I'm back from holidays but occupied by another project for the next two days.

view this post on Zulip Rob Lewis (Jul 20 2020 at 16:10):

It's not directly the same but could be related. I'll file it separately for when you have time. Thanks as always!

view this post on Zulip Floris van Doorn (Jul 20 2020 at 17:15):

Rob Lewis said:

Uhm. And using by apply_instance instead of infer_instance makes it instant.Maybe because this freezes the instance cache?

I've noticed infer_instance being worse than by apply_instance in multiple cases. I think in those cases usually infer_instance fails and by apply_instance succeeds. My personal workaround is just to never use infer_instance anymore.

view this post on Zulip Johan Commelin (Jul 20 2020 at 17:15):

But this is a MWE extracted from a situation where we use neither, I think

view this post on Zulip Johan Commelin (Jul 22 2020 at 12:23):

This is biting me again :sad:

view this post on Zulip Johan Commelin (Jul 22 2020 at 16:37):

@Gabriel Ebner do you think that lean#403 also fixes this issue?

view this post on Zulip Gabriel Ebner (Jul 23 2020 at 09:30):

I think so.

view this post on Zulip Johan Commelin (Jul 23 2020 at 09:32):

@Gabriel Ebner Cool! Any idea about when you want to release a new Lean? (-;


Last updated: May 10 2021 at 00:31 UTC