Stream: Coq users

Topic: external module in Coq plugin

view this post on Zulip Emily First (Aug 03 2021 at 18:43):

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.

view this post on Zulip Enrico Tassi (Aug 03 2021 at 21:11):

Which build system are you using?

view this post on Zulip Emily First (Aug 04 2021 at 14:25):

I'm using coq_makefile

view this post on Zulip Enrico Tassi (Aug 06 2021 at 13:12):

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