# Zulip Chat Archive

## Stream: general

### Topic: slow elaboration

#### Kenny Lau (May 25 2020 at 09:05):

```
import algebra.group_ring_action linear_algebra.basis field_theory.subfield
universes u v
variables (G : Type u) [group G] (F : Type v) [field F] [mul_semiring_action G F] (g : G)
def fixed : set F :=
{ x | ∀ g : G, g • x = x }
instance : is_subfield (fixed G F) :=
sorry
/-- Embedding induced by action. -/
def mul_action.to_fun : F ↪ (G → F) :=
⟨λ x m, m • x, λ x y H, one_smul G x ▸ one_smul G y ▸ by convert congr_fun H 1⟩
theorem linear_independent_smul_of_linear_independent {s : finset F}
(hs : linear_independent (fixed G F) (λ i : (↑s : set F), (i : F))) :
linear_independent F (λ i : (↑(s.map $ mul_action.to_fun G F) : set (G → F)), (i : G → F)) :=
sorry
```

#### Kenny Lau (May 25 2020 at 09:05):

the statement of the theorem is slow to elaborate

#### Kenny Lau (May 25 2020 at 09:06):

but `profiler`

doesn't show any abnormality

#### Kenny Lau (May 25 2020 at 09:06):

if I use `trace.class_instances`

there is this mysterious search for:

```
has_coe_to_fun ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s)
```

#### Kenny Lau (May 25 2020 at 09:07):

which I cannot find in the `pp.all`

`#print`

#### Kenny Lau (May 25 2020 at 09:07):

is there anyway to somehow track the elaboration?

#### Kevin Buzzard (May 25 2020 at 09:15):

Does

```
set_option trace.type_context.is_def_eq true
set_option trace.type_context.is_def_eq_detail true
```

help?

#### Kevin Buzzard (May 25 2020 at 09:16):

Wait, what version of Lean are you on? Everything is instant for me on 3.13.2

#### Kenny Lau (May 25 2020 at 09:17):

`(3, (14, 0))`

#### Kevin Buzzard (May 25 2020 at 09:18):

I do have some crazy search for the coercion though:

```
[class_instances] (2) ?x_104 : has_coe ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s) ?x_101 := @list.bin_tree_to_list ?x_205
failed is_def_eq
[class_instances] (2) ?x_104 : has_coe ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s) ?x_101 := smt_tactic.has_coe ?x_206
failed is_def_eq
[class_instances] (2) ?x_104 : has_coe ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s) ?x_101 := @lean.parser.has_coe ?x_207
failed is_def_eq
[class_instances] (2) ?x_104 : has_coe ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s) ?x_101 := @tactic.ex_to_tac ?x_208
failed is_def_eq
[class_instances] (2) ?x_104 : has_coe ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s) ?x_101 := @tactic.opt_to_tac ?x_209
failed is_def_eq
[class_instances] (2) ?x_104 : has_coe ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s) ?x_101 := @expr.has_coe ?x_210 ?x_211
failed is_def_eq
[class_instances] (2) ?x_104 : has_coe ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s) ?x_101 := string_to_format
failed is_def_eq
[class_instances] (2) ?x_104 : has_coe ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s) ?x_101 := nat_to_format
failed is_def_eq
[class_instances] (2) ?x_104 : has_coe ↥↑(@finset.map F (G → F) (@mul_action.to_fun G _inst_1 F _inst_2 _inst_3) s) ?x_101 := string_to_name
failed is_def_eq
```

etc

#### Kenny Lau (May 25 2020 at 09:19):

I've never used those so I don't know what to look for

#### Kevin Buzzard (May 25 2020 at 09:19):

```
elaboration of linear_independent_smul_of_linear_independent took 0.0389ms
```

#### Kenny Lau (May 25 2020 at 09:20):

yeah `profiler`

shows nothing

#### Kenny Lau (May 25 2020 at 09:20):

but I can see the orange bar

#### Kenny Lau (May 25 2020 at 09:20):

takes about 4 seconds for the orange bar to disappear

#### Kenny Lau (May 25 2020 at 09:20):

so maybe 1 second for you

#### Kevin Buzzard (May 25 2020 at 09:21):

It takes well under a second for mine to disappear. I'll upgrade to 3.14.

#### Kevin Buzzard (May 25 2020 at 09:23):

The trace output was huge though

#### Kevin Buzzard (May 25 2020 at 09:25):

Still fast for me

#### Kenny Lau (May 25 2020 at 09:34):

I upgraded mathlib and now it only takes 2 seconds for the orange bar to disappear

#### Kenny Lau (May 25 2020 at 09:35):

so this should be 0.5 seconds for you

#### Kenny Lau (May 25 2020 at 09:35):

which I guess would still be visible

#### Kevin Buzzard (May 25 2020 at 10:00):

Oh I see it, I can believe it's about a third of a second

#### Kenny Lau (May 29 2020 at 13:54):

```
import algebra.group_ring_action field_theory.subfield ring_theory.polynomial
import field_theory.minimal_polynomial field_theory.splitting_field
local attribute [instance] classical.dec
universes u v
variables (G : Type u) [group G] (F : Type v) [field F] [mul_semiring_action G F] (g : G)
def fixed : set F :=
{ x | ∀ g : G, g • x = x }
instance fixed.is_subfield : is_subfield (fixed G F) :=
sorry
#check (1 : polynomial (fixed G F))
```

#### Kenny Lau (May 29 2020 at 13:55):

the `check`

takes 3 to 4 seconds

#### Kenny Lau (May 29 2020 at 13:55):

I can't do anything if I can't even talk about `1`

#### Yury G. Kudryashov (Jun 02 2020 at 18:29):

Elaboration of the `inhabited`

instance in #2897 takes ~10s with `lean -j1`

on my laptop. It's more than the rest of the file.

#### Johan Commelin (Jun 02 2020 at 18:48):

What happened to our :racecar: fast lean?

#### Gabriel Ebner (Jun 02 2020 at 18:49):

I took a quick look. The following reduces the runtime from 8.5s to 2s on my laptop:

```
local attribute [instance, priority 1001] classical.prop_decidable
```

#### Gabriel Ebner (Jun 02 2020 at 18:50):

The reason is that `split_if`

uses `by_cases`

, which uses `decidable`

even if the goal is a prop.

#### Johan Commelin (Jun 02 2020 at 18:51):

Aah, so would `open_locale classical`

have avoided this problem?

#### Gabriel Ebner (Jun 02 2020 at 18:52):

There is already an `open_locale classical`

.

#### Yury G. Kudryashov (Jun 02 2020 at 18:52):

I have `open_locale classical`

but it adds `classical.prop_decidable`

as a low prio instance.

#### Yury G. Kudryashov (Jun 02 2020 at 18:52):

Gabriel explains that I need to make it a high priority instance.

#### Johan Commelin (Jun 02 2020 at 18:52):

priorities are hard

#### Gabriel Ebner (Jun 02 2020 at 18:52):

And/or fix `by_cases`

.

#### Johan Commelin (Jun 02 2020 at 18:53):

Ooh... I was still looking at Kenny's code

#### Johan Commelin (Jun 02 2020 at 18:53):

Is it the same problem?

#### Johan Commelin (Jun 02 2020 at 18:53):

I somehow assumed that Yury's post was a semireply to Kenny

#### Sebastien Gouezel (Jun 02 2020 at 19:35):

I have a good one. The beginning of the file `analysis/specific_functions/pow.lean`

(after imports) is

```
open_locale classical real topological_space
namespace complex
/-- The complex power function `x^y`, given by `x^y = exp(y log x)` (where `log` is the principal
determination of the logarithm), unless `x = 0` where one sets `0^0 = 1` and `0^y = 0` for
`y ≠ 0`. -/
noncomputable def cpow (x y : ℂ) : ℂ :=
if x = 0
then if y = 0
then 1
else 0
else exp (log x * y)
noncomputable instance : has_pow ℂ ℂ := ⟨cpow⟩
@[simp] lemma cpow_eq_pow (x y : ℂ) : cpow x y = x ^ y := rfl
lemma cpow_def (x y : ℂ) : x ^ y =
if x = 0
then if y = 0
then 1
else 0
else exp (log x * y) := rfl
```

With `profiler`

on, I get 17.3s to elaborate `cpow`

(and my computer is pretty fast, so I guess Kenny couldn't even open this file). Then, for `cpow_def`

, the profiler tells me that it is less than one second, but the bar stays orange also for roughly 20s, so something is hidden here.

#### Johan Commelin (Jun 02 2020 at 19:44):

What on earth is so hard about `cpow`

?

#### Yury G. Kudryashov (Jun 02 2020 at 19:45):

Probably it tries many `decidable`

instances before using `classical`

fallback.

#### Yury G. Kudryashov (Jun 02 2020 at 19:46):

@Sebastien Gouezel Did you try to make `classical`

a high priority instance?

#### Sebastien Gouezel (Jun 02 2020 at 19:46):

Exactly. If you set `local attribute [instance, priority 1001] classical.prop_decidable`

, everything becomes instant.

#### Gabriel Ebner (Jun 02 2020 at 19:48):

This also makes it instant:

```
instance : decidable_eq ℂ := λ _ _, classical.prop_decidable _
```

#### Johan Commelin (Jun 02 2020 at 19:48):

That's crazy...

#### Johan Commelin (Jun 02 2020 at 19:48):

@Kenny Lau Does this also fix your problems in this thread?

#### Yury G. Kudryashov (Jun 02 2020 at 19:49):

Should we add these instance for real and complex numbers?

#### Gabriel Ebner (Jun 02 2020 at 19:50):

Wow, this is also instant:

```
instance : decidable_eq ℂ := by apply_instance
```

#### Sebastien Gouezel (Jun 02 2020 at 19:52):

Don't look at the instance trace, it is definitely not for kids. with things like

```
[class_instances] (4) ?x_33 : nonneg_ring ℂ := @linear_nonneg_ring.to_nonneg_ring ?x_34 ?x_35
```

What's a `nonneg_ring`

?!

#### Gabriel Ebner (Jun 02 2020 at 19:52):

The cause for this decidable tarpit is the `eq.decidable`

instance, which derives `decidable_eq α`

from `decidable_linear_order α`

. And this searches through half of the tc hierarchy.

#### Kenny Lau (Jun 02 2020 at 19:56):

Gabriel Ebner said:

The cause for this decidable tarpit is the

`eq.decidable`

instance, which derives`decidable_eq α`

from`decidable_linear_order α`

. And this searches through half of the tc hierarchy.

oh!

#### Sebastien Gouezel (Jun 02 2020 at 19:59):

Should we downgrade its priority to 90 and put `classical`

at 95?

#### Johan Commelin (Jun 02 2020 at 19:59):

What would happen if we completely unbundle all `decidable`

stuff? So you only have `decidable_{eq,prop}`

and `linear_order`

, but not `decidable_linear_order`

.

#### Sebastien Gouezel (Jun 02 2020 at 20:00):

For a long time, I have wanted to kill `decidable_linear_order`

, but this in core, alas. Oh, wait :)

#### Johan Commelin (Jun 02 2020 at 20:01):

Oh, wait :)

Is that a promise?

#### Mario Carneiro (Jun 02 2020 at 20:37):

`nonneg_ring`

should not be a class, that was a mistake

#### Mario Carneiro (Jun 02 2020 at 20:38):

and `eq.decidable`

should be a local instance

#### Bryan Gin-ge Chen (Jun 02 2020 at 22:54):

I'm just catching up on this now. Is there a PR for this (in progress)? If not, can someone summarize what needs to be done?

#### Johan Commelin (Jun 03 2020 at 05:03):

Johan Commelin said:

What would happen if we completely unbundle all

`decidable`

stuff? So you only have`decidable_{eq,prop}`

and`linear_order`

, but not`decidable_linear_order`

.

I really have no idea if this is feasable. But @Gabriel Ebner gave a :thumbs_up:, so I think we can/should try this.

#### Kenny Lau (Jun 09 2020 at 13:39):

```
import data.monoid_algebra
import ring_theory.algebra
import algebra.invertible
import algebra.char_p
import linear_algebra.basis
universes u
noncomputable theory
open module
open monoid_algebra
variables {k : Type u} [comm_ring k] {G : Type u} [group G]
variables {V : Type u} [add_comm_group V] [module (monoid_algebra k G) V]
variables {W : Type u} [add_comm_group W] [module (monoid_algebra k G) W]
#check (by apply_instance : semimodule k (restrict_scalars k (monoid_algebra k G) W))
#check @linear_map.{u u u} k (restrict_scalars k (monoid_algebra k G) W) (restrict_scalars k (monoid_algebra k G) V) _ _ _
/- restrict_scalars k (monoid_algebra k G) W →ₗ[k] restrict_scalars k (monoid_algebra k G) V :
Π [_inst_4 : semimodule k (restrict_scalars k (monoid_algebra k G) W)]
[_inst_5 : semimodule k (restrict_scalars k (monoid_algebra k G) V)], Type u
```

#### Kenny Lau (Jun 09 2020 at 13:39):

Hi everyone, it's Kenny "Slow Elaboration" Lau again

#### Kenny Lau (Jun 09 2020 at 13:39):

the elaboration speed is ok here

#### Kenny Lau (Jun 09 2020 at 13:40):

until one puts two more underscores at the end to tell Lean to find the remaining instances

#### Kenny Lau (Jun 09 2020 at 13:40):

note how the first check tells you that Lean can find the instance in "normal" speed

#### Kenny Lau (Jun 09 2020 at 13:40):

but for some reason Lean is slow if I put the underscore at the end

#### Kenny Lau (Jun 09 2020 at 13:41):

so I cannot seem to isolate the problem

#### Mario Carneiro (Jun 09 2020 at 14:19):

both `#check`

s are near instant for me

#### Mario Carneiro (Jun 09 2020 at 14:20):

that's on a slightly older version of mathlib though, maybe something changed recently

#### Kenny Lau (Jun 09 2020 at 14:25):

@Mario Carneiro even when you add two underscores at the end?

#### Mario Carneiro (Jun 09 2020 at 14:26):

oh I misunderstood

#### Mario Carneiro (Jun 09 2020 at 14:29):

Okay I can replicate.

```
-- fast
#check @linear_map.{u u u} k
(restrict_scalars k (monoid_algebra k G) W)
(restrict_scalars k (monoid_algebra k G) V) _ _ _
(by apply_instance) (by apply_instance)
-- slow
#check @linear_map.{u u u} k
(restrict_scalars k (monoid_algebra k G) W)
(restrict_scalars k (monoid_algebra k G) V) _ _ _
_ _
```

#### Kenny Lau (Jun 09 2020 at 14:30):

that's just fascinating

#### Kenny Lau (Jun 09 2020 at 14:30):

what's happening?

#### Mario Carneiro (Jun 09 2020 at 14:32):

This looks like it will require a C++ deep dive. I don't know what could make this happen besides elaboration order shenanigans as a result of using `by`

#### Kenny Lau (Jun 09 2020 at 14:33):

```
-- fast
#check @linear_map.{u u u} k
(restrict_scalars k (monoid_algebra k G) W)
(restrict_scalars k (monoid_algebra k G) V) _ _ _
(by apply_instance)
-- slow
#check @linear_map.{u u u} k
(restrict_scalars k (monoid_algebra k G) W)
(restrict_scalars k (monoid_algebra k G) V) _ _ _
infer_instance
```

#### Mario Carneiro (Jun 09 2020 at 14:36):

```
-- fast
example := @linear_map.{u u u} k
(restrict_scalars k (monoid_algebra k G) W)
(restrict_scalars k (monoid_algebra k G) V) _ _ _ _ _
-- slow
#check @linear_map.{u u u} k
(restrict_scalars k (monoid_algebra k G) W)
(restrict_scalars k (monoid_algebra k G) V) _ _ _ _ _
```

#### Kenny Lau (Jun 09 2020 at 14:37):

what :o

#### Kenny Lau (Jun 09 2020 at 14:38):

interesting

#### Reid Barton (Jun 09 2020 at 14:42):

what if you make the `example`

a `def`

, and `#check`

it?

#### Kevin Buzzard (Jun 09 2020 at 16:05):

changing the example to a def makes it slow, in Mario's example. Kenny's last example freaks me out a bit more

#### Mario Carneiro (Jun 09 2020 at 17:55):

kenny's version makes sense to me only in the sense that it's testing the same thing as my example before that. There is something about switching to tactic mode here using `by`

that makes it work out

#### Kenny Lau (Jun 25 2020 at 07:14):

```
import algebra.char_p data.polynomial
universe u
namespace polynomial
theorem C_nat_cast {R : Type u} [comm_semiring R] (n : ℕ) : C (n : R) = n :=
ring_hom.map_nat_cast C.to_ring_hom n
instance {R : Type u} [comm_semiring R] (p : ℕ) [h : char_p R p] : char_p (polynomial R) p :=
let ⟨h⟩ := h in ⟨λ n, by rw [← C_nat_cast, ← C_0, C_inj, h]⟩
-- fast
theorem frobenius_eq {R : Type u} [comm_ring R] (p : ℕ) [fact p.prime] [char_p R p] (f : polynomial R) :
@frobenius (polynomial R) _ p _ (polynomial.char_p p) f = f.eval₂ C (X ^ p) :=
sorry
-- slow
theorem frobenius_eq {R : Type u} [comm_ring R] (p : ℕ) [fact p.prime] [char_p R p] (f : polynomial R) :
@frobenius (polynomial R) _ p _ _ f = f.eval₂ C (X ^ p) :=
sorry
-- fast
theorem frobenius_eq'' {R : Type u} [comm_ring R] (p : ℕ) [fact p.prime] [char_p R p] (f : polynomial R) :
by exact @frobenius (polynomial R) _ p _ _ f = f.eval₂ C (X ^ p) :=
sorry
end polynomial
```

#### Kenny Lau (Jun 25 2020 at 07:14):

is this the same bug?

#### Kenny Lau (Jun 25 2020 at 07:14):

(btw the theorem is false)

#### Kenny Lau (Jun 25 2020 at 07:16):

(edit: I guess I found the workaround)

#### Johan Commelin (Jun 25 2020 at 07:17):

What's going on with `C_nat_cast`

? Shouldn't there be `alg_hom.nat_cast`

instead?

#### Kenny Lau (Jun 25 2020 at 07:19):

right

Last updated: May 08 2021 at 09:11 UTC