Zulip Chat Archive

Stream: general

Topic: slow elaboration


view this post on Zulip 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

view this post on Zulip Kenny Lau (May 25 2020 at 09:05):

the statement of the theorem is slow to elaborate

view this post on Zulip Kenny Lau (May 25 2020 at 09:06):

but profiler doesn't show any abnormality

view this post on Zulip 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)

view this post on Zulip Kenny Lau (May 25 2020 at 09:07):

which I cannot find in the pp.all #print

view this post on Zulip Kenny Lau (May 25 2020 at 09:07):

is there anyway to somehow track the elaboration?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 25 2020 at 09:17):

(3, (14, 0))

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 25 2020 at 09:19):

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

view this post on Zulip Kevin Buzzard (May 25 2020 at 09:19):

elaboration of linear_independent_smul_of_linear_independent took 0.0389ms

view this post on Zulip Kenny Lau (May 25 2020 at 09:20):

yeah profiler shows nothing

view this post on Zulip Kenny Lau (May 25 2020 at 09:20):

but I can see the orange bar

view this post on Zulip Kenny Lau (May 25 2020 at 09:20):

takes about 4 seconds for the orange bar to disappear

view this post on Zulip Kenny Lau (May 25 2020 at 09:20):

so maybe 1 second for you

view this post on Zulip Kevin Buzzard (May 25 2020 at 09:21):

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

view this post on Zulip Kevin Buzzard (May 25 2020 at 09:23):

The trace output was huge though

view this post on Zulip Kevin Buzzard (May 25 2020 at 09:25):

Still fast for me

view this post on Zulip Kenny Lau (May 25 2020 at 09:34):

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

view this post on Zulip Kenny Lau (May 25 2020 at 09:35):

so this should be 0.5 seconds for you

view this post on Zulip Kenny Lau (May 25 2020 at 09:35):

which I guess would still be visible

view this post on Zulip Kevin Buzzard (May 25 2020 at 10:00):

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

view this post on Zulip 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))

view this post on Zulip Kenny Lau (May 29 2020 at 13:55):

the check takes 3 to 4 seconds

view this post on Zulip Kenny Lau (May 29 2020 at 13:55):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 02 2020 at 18:48):

What happened to our :racecar: fast lean?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 02 2020 at 18:51):

Aah, so would open_locale classical have avoided this problem?

view this post on Zulip Gabriel Ebner (Jun 02 2020 at 18:52):

There is already an open_locale classical.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jun 02 2020 at 18:52):

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

view this post on Zulip Johan Commelin (Jun 02 2020 at 18:52):

priorities are hard

view this post on Zulip Gabriel Ebner (Jun 02 2020 at 18:52):

And/or fix by_cases.

view this post on Zulip Johan Commelin (Jun 02 2020 at 18:53):

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

view this post on Zulip Johan Commelin (Jun 02 2020 at 18:53):

Is it the same problem?

view this post on Zulip Johan Commelin (Jun 02 2020 at 18:53):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 02 2020 at 19:44):

What on earth is so hard about cpow?

view this post on Zulip Yury G. Kudryashov (Jun 02 2020 at 19:45):

Probably it tries many decidable instances before using classical fallback.

view this post on Zulip Yury G. Kudryashov (Jun 02 2020 at 19:46):

@Sebastien Gouezel Did you try to make classical a high priority instance?

view this post on Zulip Sebastien Gouezel (Jun 02 2020 at 19:46):

Exactly. If you set local attribute [instance, priority 1001] classical.prop_decidable, everything becomes instant.

view this post on Zulip Gabriel Ebner (Jun 02 2020 at 19:48):

This also makes it instant:

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

view this post on Zulip Johan Commelin (Jun 02 2020 at 19:48):

That's crazy...

view this post on Zulip Johan Commelin (Jun 02 2020 at 19:48):

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

view this post on Zulip Yury G. Kudryashov (Jun 02 2020 at 19:49):

Should we add these instance for real and complex numbers?

view this post on Zulip Gabriel Ebner (Jun 02 2020 at 19:50):

Wow, this is also instant:

instance : decidable_eq  := by apply_instance

view this post on Zulip 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?!

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Sebastien Gouezel (Jun 02 2020 at 19:59):

Should we downgrade its priority to 90 and put classical at 95?

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip Johan Commelin (Jun 02 2020 at 20:01):

Oh, wait :)

Is that a promise?

view this post on Zulip Mario Carneiro (Jun 02 2020 at 20:37):

nonneg_ring should not be a class, that was a mistake

view this post on Zulip Mario Carneiro (Jun 02 2020 at 20:38):

and eq.decidable should be a local instance

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 09 2020 at 13:39):

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

view this post on Zulip Kenny Lau (Jun 09 2020 at 13:39):

the elaboration speed is ok here

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 09 2020 at 13:40):

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

view this post on Zulip Kenny Lau (Jun 09 2020 at 13:40):

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

view this post on Zulip Kenny Lau (Jun 09 2020 at 13:41):

so I cannot seem to isolate the problem

view this post on Zulip Mario Carneiro (Jun 09 2020 at 14:19):

both #checks are near instant for me

view this post on Zulip Mario Carneiro (Jun 09 2020 at 14:20):

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

view this post on Zulip Kenny Lau (Jun 09 2020 at 14:25):

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

view this post on Zulip Mario Carneiro (Jun 09 2020 at 14:26):

oh I misunderstood

view this post on Zulip 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) _ _ _
  _ _

view this post on Zulip Kenny Lau (Jun 09 2020 at 14:30):

that's just fascinating

view this post on Zulip Kenny Lau (Jun 09 2020 at 14:30):

what's happening?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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) _ _ _ _ _

view this post on Zulip Kenny Lau (Jun 09 2020 at 14:37):

what :o

view this post on Zulip Kenny Lau (Jun 09 2020 at 14:38):

interesting

view this post on Zulip Reid Barton (Jun 09 2020 at 14:42):

what if you make the example a def, and #check it?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 25 2020 at 07:14):

is this the same bug?

view this post on Zulip Kenny Lau (Jun 25 2020 at 07:14):

(btw the theorem is false)

view this post on Zulip Kenny Lau (Jun 25 2020 at 07:16):

(edit: I guess I found the workaround)

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jun 25 2020 at 07:19):

right


Last updated: May 08 2021 at 09:11 UTC