Zulip Chat Archive

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