It seems that unimath currently fails with memory overflow with a high probability in our CI. What should be done?
Is this a result of a recent change in Coq, or a recent change in Unimath? Can we track down the change resulting in the high memory usage?
https://gitlab.com/coq/coq/-/jobs/1335869478 unimath was around 1GB memory (unimath runs start around 16:00 and 17:00 CEST June 11th)
https://gitlab.com/coq/coq/-/jobs/1339135031 around 3GB (unimath runs start around 11:00 and 12:15 CEST June 12th)
seems like something happened around June 12th (give or take a day)
example failing job https://gitlab.com/coq/coq/-/jobs/1360985187
build/CoqMakefile.make:762: recipe for target 'UniMath/Bicategories/DisplayedBicats/Examples/DisplayedInserter.vo' failed
this is a file from https://github.com/UniMath/UniMath/pull/1363 merged June 11th 17:20 GMT+2
I'm not good at timezones but I think CEST = GMT+2 so the first bench just barely missed the updated unimath for the OLD run
PS in the second bench https://coq.gitlab.io/-/coq/-/jobs/1339135031/artifacts/_bench/html/coq-unimath/UniMath/Bicategories/DisplayedBicats/Examples/DisplayedInserter.v.html we see that https://github.com/UniMath/UniMath/blob/d0e7d748fb5cee00472c08abe1835022910ec7ff/UniMath/Bicategories/DisplayedBicats/Examples/DisplayedInserter.v#L858 is by far the line which takes the longest to execute in that file
so what do we do?
can't we raise the memory limits of our runners?
The shared runners or our private runners?
any of these, as long as we can force unimath to run on those with more memory
We can't change the memory limits on shared runners AFAICT. For our private runners (pendulum, because pyrolyse is broken since it was upgraded to a more recent Ubuntu version), we should check if the memory problem actually occurred first.
Last updated: Dec 07 2023 at 09:01 UTC