Stream: Coq devs & plugin devs

Topic: CI failure in coq-elpi


view this post on Zulip Enrico Tassi (Feb 09 2023 at 08:47):

I've seen here and there a failure in coq-elpi somewhat related to universes. Locally here it works fine. Is it a know issue? Does it ring any bell? Are you merging PRs ignoring the failure?

view this post on Zulip Gaëtan Gilbert (Feb 09 2023 at 08:49):

I've never seen that

view this post on Zulip Gaëtan Gilbert (Feb 09 2023 at 08:50):

does "here and there" include some CI log you could link?

view this post on Zulip Enrico Tassi (Feb 09 2023 at 09:22):

Well, I saw it https://github.com/coq/coq/pull/13448 (gone at the third retry) but also in https://github.com/coq/coq/pull/17237

view this post on Zulip Enrico Tassi (Feb 09 2023 at 09:25):

What is even more weird is that the errors I saw were different, but always about universes

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

I only see the hulk failure in them
eg https://gitlab.com/coq/coq/-/jobs/3736006977

Command terminated by signal 9
examples/hulk.vo (real: 22.23, user: 20.53, sys: 1.40, mem: 3223768 ko)
Makefile.test-suite.coq:815: recipe for target 'examples/hulk.vo' failed

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

please link job logs not PRs

view this post on Zulip Enrico Tassi (Feb 09 2023 at 12:22):

That one seems a memory problem due to -j2.
I'll try to keep the links, maybe I was mislead by the fact that the last line in the log (again because of -j2) was an expected universe related error.

view this post on Zulip Gaëtan Gilbert (Feb 10 2023 at 09:18):

maybe it was something like https://gitlab.com/coq/coq/-/jobs/3745222059

File "src/coq_elpi_HOAS.ml", line 70, characters 36-52:
70 |   let show x = Pp.string_of_ppcmds (Univ.Universe.pr UnivNames.pr_with_global_universes x)
                                         ^^^^^^^^^^^^^^^^
Error: This function has type Univ.Universe.t -> Pp.t
       It is applied to too many arguments; maybe you forgot a `;'.
Command exited with non-zero status 2
src/coq_elpi_HOAS.cmo (real: 0.11, user: 0.09, sys: 0.01, mem: 26240 ko)
Makefile.coq:737: recipe for target 'src/coq_elpi_HOAS.cmo' failed

where the tested coq commit didn't include https://github.com/coq/coq/pull/17177 even though the overlay for 17177 was already merged?


Last updated: Mar 03 2024 at 15:01 UTC