Topic: linting time
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?
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.)
Bryan Gin-ge Chen (Feb 19 2021 at 00:19):
Thanks to #6293 by Gabriel, the linting time is back down to 45 minutes!
Kevin Buzzard (Feb 19 2021 at 00:20):
See you again in July!
Scott Morrison (Feb 19 2021 at 00:49):
If only number of cores available also grew quadratically. :-)
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