I just hit a failure in ci-serapi.

```
File "sertop/dune", line 6, characters 79-90:
6 | (libraries findlib.dynload cmdliner serapi coq-lsp.serlib coq-lsp.serlib.ltac coq-lsp.coq serlib_extra))
^^^^^^^^^^^
Error: Library "coq-lsp.coq" not found.
File "serlib_extra/dune", line 6, characters 33-47:
6 | (libraries coq-core.stm sexplib coq-lsp.serlib))
^^^^^^^^^^^^^^
Error: Library "coq-lsp.serlib" not found.
make: *** [Makefile.ci:193: ci-serapi] Error 2
```

Is it broken?

Yes, we did change some setup, actually the fix should have been ready to merge this morning, however I did remove the overlay branch in mistake so we need to run the CI again, but once https://github.com/coq/coq/pull/19134 completes we can merge and fix.

When checking `make ci-coq_lsp`

or `make ci-serapi`

on current master, I still have the error above. Am I doing something wrong?

did you try deleting _build_ci?

Yes

IDK then, I get the error from univ inconsistency in serlib

CI seems OK, how can I reproduce?

My bad, the pull had not worked.

Last updated: Oct 13 2024 at 01:02 UTC