import causes deterministic timeout

Stream: general

[Antoine Labelle]

Hi! The following code works fine until I import linear_algebra.dual, but then it gives me a deterministic timeout. Does anyone see a possible explanation for this weird behavior?

import representation_theory.basic

variables (k G V W : Type*) [comm_semiring k] [group G] [add_comm_monoid V] [add_comm_monoid W]
variables [module k V] [distrib_mul_action G V] [smul_comm_class G k V]
variables [module k W] [distrib_mul_action G W] [smul_comm_class G k W]

open representation

instance  linear_hom_distrib_mul_action : distrib_mul_action G (V →ₗ[k] W) :=
{ smul := λ g f, ↑(as_group_hom k G W g) ∘ₗ f ∘ₗ ↑(as_group_hom k G V g)⁻¹,
  one_smul := λ f, by {ext, simp},
  mul_smul := λ g h f, by {ext, simp},
  smul_add := λ g f₁ f₂, by simp [linear_map.add_comp, linear_map.comp_add],
  smul_zero := λ g, by simp}

[Eric Wieser]

Does the timeout persist if you instead import the things imported by file#linear_algebra/dual?

[Eric Wieser]

That is

import linear_algebra.finite_dimensional
import linear_algebra.projection
import linear_algebra.sesquilinear_form

[Antoine Labelle]

Yes, and it persists if I import only linear_algebra.sesquilinear_form

[Eric Wieser]

Can you keep tracing back the imports until it doesn't break any more?

[Antoine Labelle]

Eric Wieser said:

Can you keep tracing back the imports until it doesn't break any more?

The problematic file seems to be linear_algebra.matrix.reindex

[Eric Wieser]

file#linear_algebra/matrix/reindex

[Eric Wieser]

Looks innocuous...

[Antoine Labelle]

Indeed, that's weird

[Antoine Labelle]

Update : I reproduced the definition in a separate project to see if the problem was related to other things I had in my file, and now it still breaks if I import file#linear_algebra/dual, but it doesn't if I import only the files imported by file#linear_algebra/dual (in particular it doesn't break for file#linear_algebra/matrix/reindex).

[Eric Wieser]

Your problem is likely just that simp is slower for each simp lemma that's imported

[Eric Wieser]

And that you have four simps all at once

[Antoine Labelle]

Indeed, if I just replace the simp in smul_zero by simp only [linear_map.zero_comp, linear_map.comp_zero] it now works. Seems pretty arbitrary but at least now it's fixed!