Stream: Coq devs & plugin devs

Topic: HB failures in CI


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Jan 20 2023 at 20:00):

any PR touching conversion/unification?

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2023 at 20:01):

there are many potential culprits in the same area

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2023 at 20:02):

I've touched stuff around SProp that might have subtly destroyed fast-paths

view this post on Zulip Gaëtan Gilbert (Jan 20 2023 at 20:06):

the jobs I linked are consecutive merges
how could some other PR be involved?

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2023 at 20:13):

maybe parsing subtly broke something unification-related?


Last updated: Mar 29 2024 at 04:02 UTC