Zulip Chat Archive

Stream: general

Topic: multilinear timeouts


view this post on Zulip 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?

view this post on Zulip Gabriel Ebner (Mar 11 2021 at 11:39):

I've run into the same issue in a different PR: https://github.com/leanprover-community/mathlib/pull/6045/files#diff-030c8b121453cb0be59dad5f7db3fe154f7bd17ad5ec67167535b9cb68400559

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Rob Lewis (Mar 11 2021 at 11:42):

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

view this post on Zulip 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