Gaëtan Gilbert (Jan 20 2023 at 13:20): Gaëtan Gilbert (Jan 20 2023 at 13:20):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?
Enrico Tassi (Jan 20 2023 at 18:58):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.
Pierre-Marie Pédrot (Jan 20 2023 at 19:57):FWIW all memory allocated in hulk.v seems to be due to conversion in CClosure.
Pierre-Marie Pédrot (Jan 20 2023 at 19:58):and all callers are ground unification, so it seems we're just allocating big terms from there.
Enrico Tassi (Jan 20 2023 at 20:00):any PR touching conversion/unification?
Pierre-Marie Pédrot (Jan 20 2023 at 20:01):there are many potential culprits in the same area
Pierre-Marie Pédrot (Jan 20 2023 at 20:02):I've touched stuff around SProp that might have subtly destroyed fast-paths
Gaëtan Gilbert (Jan 20 2023 at 20:06):the jobs I linked are consecutive merges
how could some other PR be involved?
Pierre-Marie Pédrot (Jan 20 2023 at 20:13):maybe parsing subtly broke something unification-related?
Last updated: Dec 07 2023 at 09:01 UTC