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?
I've never seen that
does "here and there" include some CI log you could link?
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
What is even more weird is that the errors I saw were different, but always about universes
I only see the hulk failure in them
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
please link job logs not PRs
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.
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: Jun 08 2023 at 04:01 UTC