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.

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

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

Last updated: Jul 23 2024 at 21:01 UTC