Zulip Chat Archive

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've run into the same issue in a different PR: https://github.com/leanprover-community/mathlib/pull/6045/files#diff-030c8b121453cb0be59dad5f7db3fe154f7bd17ad5ec67167535b9cb68400559

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: Aug 03 2023 at 10:10 UTC