The Coq mailing list

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

We got Dune and SerAPI working, and also Lymp so we can call out to machine learning models in Python. (Pyml and Py didn't work, and gave us mysterious errors.)

It's in a branch of coq-plugin-lib, in case anyone finds this in the future and needs to do something similar: https://github.com/uwplse/coq-plugin-lib/tree/sound

Talia

On Wed, Sep 8, 2021 at 4:15 PM Talia Ringer <tringer AT cs.washington.edu> wrote:

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