Stream: MetaCoq

Topic: erasurefunction taking lots of memory?


view this post on Zulip Gaëtan Gilbert (May 26 2023 at 11:09):

in Coq CI some jobs have been failing in erasurefunction from out of memory
eg https://gitlab.com/coq/coq/-/jobs/4351425321
is this expected?

view this post on Zulip Matthieu Sozeau (May 27 2023 at 05:07):

It needs a medium or large worker I think

view this post on Zulip Pierre-Marie Pédrot (May 27 2023 at 12:05):

I've perfed a bit, and there are weird things going on w.r.t. memory allocation. https://github.com/coq/coq/pull/17652 should hopefully help

view this post on Zulip Pierre-Marie Pédrot (May 27 2023 at 12:22):

(This PR makes EraruseFunction about 30% faster on my machine and reduces the memory footprint by several hundreds of megabytes)

view this post on Zulip Gaëtan Gilbert (May 27 2023 at 16:08):

        coq-metacoq-erasure  310.34  334.81  -7.31  1395011076201  1501383760938  -7.08  2219034906611  2438460232701  -9.00  2060224  2606256  -20.95 

nice


Last updated: Jul 23 2024 at 20:01 UTC