lean is slow

Stream: condensed mathematics

[Johan Commelin]

system_of_complexes.lean:56:4
parsing took 0.882ms
system_of_complexes.lean:56:4
elaboration of complex took 1.59s
system_of_complexes.lean:56:4
type checking of complex took 2.45ms
system_of_complexes.lean:56:4
decl post-processing of complex took 12.5s

[Johan Commelin]

/-- The complex of normed groups `V-hat(M_{≤c})^{T⁻¹} ⟶ V-hat(M_{≤c_1c}^2)^{T⁻¹} ⟶ …` -/
@[simps]
def complex (r : ℝ≥0) (V : NormedGroup) [normed_with_aut r V] [fact (0 < r)]
  (r' : ℝ≥0) [fact (0 < r')] [fact (r' ≤ 1)] (M : ProFiltPseuNormGrpWithTinv r') (c : ℝ≥0) :
  cochain_complex ℕ NormedGroup :=
cochain_complex.mk'
  (BD.complex_X c' r V M c)
  (BD.complex_d c' r V M c)
  (BD.complex_d_comp_d c' r V M c)

[Johan Commelin]

https://github.com/leanprover-community/lean-liquid/blob/master/src/pseudo_normed_group/system_of_complexes.lean#L52-L60

[Johan Commelin]

Does anybody know why this innocent looking def should take > 12s?

[Patrick Massot]

Did you try removing @[simps] as a first investigation step?

[Patrick Massot]

On my machine it certainly looks like simps is the piece taking up a lot of time.

[Patrick Massot]

Did you have a look at the generated simp lemmas?

[Johan Commelin]

I agree that @[simps] seems to account for the 12s post-processing

[Patrick Massot]

You can also try to #check all three arguments to cochain_complex.mk' (all the required variables are already defined) and see they are elaborated instantly.