The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

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