Stream: Coq devs & plugin devs

Topic: ✔ Serapi overlay & coq-lsp

view this post on Zulip Maxime Dénès (Mar 29 2023 at 06:02):

Hi there,

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?

view this post on Zulip Guillaume Melquiond (Mar 29 2023 at 06:17):

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.

view this post on Zulip Enrico Tassi (Mar 29 2023 at 06:26):

Add to the ci script rm -rf vendor/serapi

view this post on Zulip Maxime Dénès (Mar 29 2023 at 06:42):

Oh! I think I see, it does not pick up the vendored one, it just ignores the overlay.

view this post on Zulip Maxime Dénès (Mar 29 2023 at 06:42):

i.e. if you run make ci-coq_lsp without running make ci-serapi, the overlay doesn't seem to have any effect

view this post on Zulip Maxime Dénès (Mar 29 2023 at 06:46):

Thanks for the tips!

view this post on Zulip Notification Bot (Mar 29 2023 at 06:47):

Maxime Dénès has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC