The Coq mailing list

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

Just for the record for the future I guess, I couldn't get Dune working with the original plugin (even without SerAPI) because the plugin has many subdirectories, and I can't figure out a way to get the .v theory that loads the plugin to begin with to link to all of them. I can sort of hack it by adding a lot of "declare ML module" lines in the top-level theory for every subdirectory, but if I do that, coqdep gives me a number of warnings like "declared ML module contexts has not been found!" and then the build does not progress any further. I tried messing with the paths in a few different ways but couldn't figure anything out that got rid of the warning.

My work-in-progress is here: https://github.com/uwplse/coq-plugin-lib/tree/dune . I hope I figure it out at some point since this is a serious blocker for integrating a machine learning model into an existing plugin. Probably I will try to corner Emilio and talk him into a synchronous call :). But if anyone has encountered this before, I'd love to hear how you resolved it.

Talia

On Wed, Sep 8, 2021 at 12:43 AM Talia Ringer <tringer AT cs.washington.edu> wrote:

Thanks, this path looks really promising and I'll try it as soon as I get the chance.

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

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