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

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
```

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: Oct 13 2024 at 01:02 UTC