Stream: MetaCoq

Topic: Unbearably slow compilation of some Coq files


view this post on Zulip Rodolphe Lepigre (Jun 05 2024 at 13:46):

I am preparing a MetaCoq Coq CI overlay for https://github.com/coq/coq/pull/18973, and I'm noticing that some files take ages to build. Is that a known issue? I'm thinking of erasure/theories/Typed/OptimizeCorrectness.v, whose build I cancelled after 30 minutes. Stepping through the file shows tons of places where lia basically diverges, and similarly for uses of now .... For lia, clearing hypotheses helps a lot in many cases, and replacing now ... by ...; auto is typically instant when it works.

view this post on Zulip Gaëtan Gilbert (Jun 05 2024 at 13:51):

it doesn't anywhere that bad in recent bench https://coq.gitlabpages.inria.fr/-/coq/-/jobs/4404665/artifacts/_bench/html/coq-metacoq-erasure/erasure/theories/Typed/OptimizeCorrectness.v.html
and the perfile log https://coq.gitlabpages.inria.fr/-/coq/-/jobs/4404665/artifacts/_bench/logs/coq-metacoq-erasure.BOTH.perfile_timings.1.log said it took about 40s (peak mem about 1.3GB)

2min in https://gitlab.inria.fr/coq/coq/-/jobs/4402785#L4007

view this post on Zulip Rodolphe Lepigre (Jun 05 2024 at 13:52):

Then there is probably something wrong in my branch...


Last updated: Jul 23 2024 at 21:01 UTC