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 _


That's crazy...

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 #checks 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) _ _ _ _ _


what :o

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: Dec 20 2023 at 11:08 UTC