eg https://gitlab.com/coq/coq/-/jobs/3629404898 but not just that PR
Command terminated by signal 9
examples/hulk.vo (real: 37.44, user: 24.52, sys: 6.17, mem: 3240892 ko)
Makefile.test-suite.coq:815: recipe for target 'examples/hulk.vo' failed
https://github.com/math-comp/hierarchy-builder/blob/coq-master/examples/hulk.v
it seems like memory use increased by about 50% in https://github.com/coq/coq/pull/17098:
master before it https://gitlab.com/coq/coq/-/jobs/3616417701
0m26.90s | 2267476 ko | examples/hulk.vo
master after it https://gitlab.com/coq/coq/-/jobs/3620106489
0m29.72s | 3313532 ko | examples/hulk.vo
the other files don't show noticeable memory use change
@Enrico Tassi does this file stress something in particular?
I don't think the increase in memory usage is related to that PR. Are you sure it is the only change?
In particular, the file has many things in it, but should not stress the parser of Coq at all.
FWIW all memory allocated in hulk.v seems to be due to conversion in CClosure.
and all callers are ground unification, so it seems we're just allocating big terms from there.
any PR touching conversion/unification?
there are many potential culprits in the same area
I've touched stuff around SProp that might have subtly destroyed fast-paths
the jobs I linked are consecutive merges
how could some other PR be involved?
maybe parsing subtly broke something unification-related?
Last updated: Dec 07 2023 at 09:01 UTC