## Stream: general

### Topic: multilinear timeouts

#### Rob Lewis (Mar 11 2021 at 11:37):

I just opened #6639, which speeds up a proof that's causing timeouts in CI. But I'm not sure if the slowness here is related to recent changes or if it's always been there. Any ideas?

#### Gabriel Ebner (Mar 11 2021 at 11:39):

I think the definition is just on the edge of the timeout, and any change is liable to push it over.

#### Rob Lewis (Mar 11 2021 at 11:41):

Looking at @Jannis Limperg 's benchmark tool output, this commit added 20 seconds (25%) to normed_space/multilinear.lean

#### Rob Lewis (Mar 11 2021 at 11:42):

Which isn't proportional to the lines added, but the file was still slow before

#### Sebastien Gouezel (Mar 11 2021 at 12:07):

Looks like https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/223001979 is also having an effect, so I disabled some subsingleton instances in this file for further speedup.

Last updated: May 13 2021 at 06:15 UTC