Zulip Chat Archive

Stream: general

Topic: linting time

view this post on Zulip Bryan Gin-ge Chen (Feb 18 2021 at 10:34):

The time it takes to lint mathlib has been creeping upwards again lately. It now takes almost 90 minutes, whereas it was closer to 65 minutes at the beginning of December and 48 minutes near the end of September. See the CI times for master, which are mostly spent linting, due to cached oleans.

Is this scaling as expected?

view this post on Zulip Gabriel Ebner (Feb 18 2021 at 10:37):

Linting spends most of time in the simp lemmas. I would expect the simp linters to have quadratic runtime. (Every simp lemma is linted using the simplifier, whose slowness is presumably linear in the number of simp lemmas.)

view this post on Zulip Bryan Gin-ge Chen (Feb 19 2021 at 00:19):

Thanks to #6293 by Gabriel, the linting time is back down to 45 minutes!

view this post on Zulip Kevin Buzzard (Feb 19 2021 at 00:20):

See you again in July!

view this post on Zulip Scott Morrison (Feb 19 2021 at 00:49):

If only number of cores available also grew quadratically. :-)

view this post on Zulip Eric Wieser (Feb 19 2021 at 04:44):

We could presumably go further and lint declarations with even- and odd- length names in separate jobs

Last updated: May 16 2021 at 05:21 UTC