The Coq mailing list

[Lasse Blaauwbroek <lasse AT blaauwbroek.eu>]

With dune, Coq's libraries are split into sub-libraries, such as 'coq.plugins.ltac'. When you need to use a particular API file, you check which library it is in (by opening the dune file in the directory of that file), and add that library as a dep. The repo I linked does this with 'coq.plugins.ltac'.

On 08/09/2021 02:50, Talia Ringer wrote:

Thanks, with Dune though I can't even get my Coq plugin without SerAPI to load Constr, Environ, and other necessary modules. I have no idea what I'm supposed to depend on to get those.

On Tue, Sep 7, 2021 at 7:47 PM Lasse Blaauwbroek <lasse AT blaauwbroek.eu> wrote:

I have an example plugin that does exactly this here: https://github.com/LasseBlaauwbroek/serapi-example

I think I built this again 8.11 at the time, but I'm not sure (I didn't try to recompile the plugin before this email). Word of warning: Using SerAPI in a Coq plugin can be rather difficult due to its dependencies.

Lasse

On 08/09/2021 02:30, Talia Ringer wrote:

Hi all,

Have any of you gotten plugins that call out to SerAPI working, especially on Coq 8.9 (I am bound to 8.9 because of a dependency)? If so, I'd really love to see some example plugins. This is a major blocker for me and a student on a project.

I'm open to any build system at this point, but I haven't managed to get Dune working even without SerAPI---it gives me a bunch of errors failing to find Constr, Environ, and so on. The Dune tutorial didn't seem to address those errors. I don't know where to find the list of Coq libraries I can try to depend on from within a Dune project.

Without using Dune, using the normal _CoqProject and so on, I can get it to build if I build from source, which is already hacky. But then it fails to load:

File "./theories/Plib.v", line 1, characters 0-25:
Error:
while loading /home/talia/coq-plugin-lib/src/plib.cmxs:
error loading shared library: /home/talia/coq-plugin-lib/src/plib.cmxs: undefined symbol: camlPlib__Serapi_goals__anon_fn$5bcoq$2dserapi$2fserapi$2fserapi_goals$2eml$3a66$2c31$2d$2d47$5d_175_closure

Help with either of these paths would be strongly appreciated. 

Talia