## Stream: condensed mathematics

### Topic: lean is slow

#### Johan Commelin (Mar 13 2021 at 19:21):

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 (Mar 13 2021 at 19:21):

/-- 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 (Mar 13 2021 at 19:22):

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

#### Johan Commelin (Mar 13 2021 at 19:22):

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

#### Patrick Massot (Mar 13 2021 at 19:32):

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

#### Patrick Massot (Mar 13 2021 at 19:41):

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

#### Patrick Massot (Mar 13 2021 at 19:42):

Did you have a look at the generated simp lemmas?

#### Johan Commelin (Mar 13 2021 at 19:42):

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

#### Patrick Massot (Mar 13 2021 at 19:44):

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.

Last updated: May 09 2021 at 22:13 UTC