Hi! I’m interested in including an external module in a Coq plugin. I’m wondering what I have to include such that it compiles correctly without having to copy over the entire module into my plugin code.

For example, I’ve installed coq-serapi using opam and want to be able to use it as a library, but I get “Unbound module” errors.

Which build system are you using?

I'm using coq_makefile

In that case you can use a findlib directive in Makefile.coq.local, example: https://github.com/LPCIC/coq-elpi/blob/dc24b73bb3111c866272939dcbd93c3e8de6d014/Makefile.coq.local#L1

Last updated: Oct 05 2023 at 02:01 UTC