I made a serapi overlay for a PR. However it is not picked up by
coq-lsp which vendors serapi. What am I supposed to do? Should I make the
serapi submodule of coq-lsp point to my serapi repo and branch?
In Coq's CI, coq-lsp is built using
dune built --only-packages=coq-lsp. Short of a bug in dune, it should cause it to completely ignore the vendored serapi.
Add to the ci script rm -rf vendor/serapi
Oh! I think I see, it does not pick up the vendored one, it just ignores the overlay.
i.e. if you run
make ci-coq_lsp without running
make ci-serapi, the overlay doesn't seem to have any effect
Thanks for the tips!
Maxime Dénès has marked this topic as resolved.
Last updated: Nov 29 2023 at 21:01 UTC