Stream: Coq devs & plugin devs

Topic: CI failure with unimath

view this post on Zulip Pierre-Marie Pédrot (Jun 20 2021 at 15:17):

It seems that unimath currently fails with memory overflow with a high probability in our CI. What should be done?

view this post on Zulip Jason Gross (Jun 20 2021 at 18:04):

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?

view this post on Zulip Gaëtan Gilbert (Jun 20 2021 at 18:12):

past benches:
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

view this post on Zulip Gaëtan Gilbert (Jun 22 2021 at 11:37):

so what do we do?

view this post on Zulip Pierre-Marie Pédrot (Jun 22 2021 at 12:04):

can't we raise the memory limits of our runners?

view this post on Zulip Théo Zimmermann (Jun 22 2021 at 12:19):

The shared runners or our private runners?

view this post on Zulip Pierre-Marie Pédrot (Jun 22 2021 at 12:28):

any of these, as long as we can force unimath to run on those with more memory

view this post on Zulip Théo Zimmermann (Jun 22 2021 at 13:00):

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