Pyml with dune for plugin · Coq devs & plugin devs

Stream: Coq devs & plugin devs

Topic: Pyml with dune for plugin

Arpan Agrawal (Nov 28 2022 at 18:17):

Hi everyone,

I'm trying to build a new plugin that requires Python-Ocaml interfacing, and wanted to use dune as the build system for the plugin. I'm using the pyml library for this, but cannot find any resource mentioning how to use this library in a plugin. Can someone help me with this?
Thanks!

Karl Palmskog (Nov 28 2022 at 18:19):

sorry if I'm not answering the question, but have you looked at PyCoq? It's highly recommended to use it for all Python-Coq tooling/interaction: https://github.com/ejgallego/pycoq

Karl Palmskog (Nov 28 2022 at 18:20):

for the record, the pyml core developer is one of the authors of PyCoq

Arpan Agrawal (Nov 28 2022 at 18:22):

I've seen PyCoq before, but this provides Coq access from Python, right? My use case requires calling Python from within OCaml, as part of a plugin

Karl Palmskog (Nov 28 2022 at 18:23):

maybe @Emilio Jesús Gallego Arias can confirm, but my understanding is that the interaction Python-Coq is two-sided with PyCoq (access Python from Coq/OCaml, or access Coq/OCaml from Python)

Arpan Agrawal (Nov 28 2022 at 18:47):

That would be great if its the case. @Emilio Jesús Gallego Arias please let me know when you get the chance

Arpan Agrawal (Dec 01 2022 at 19:29):

@Emilio Jesús Gallego Arias sorry to bother you again, would be very helpful if you could take a look at this! @Talia Ringer mentioned you would know about this

Théo Zimmermann (Dec 01 2022 at 19:48):

Emilio is away from the internet at the current time. But maybe @Thierry Martinez can chim in.

Talia Ringer (Dec 01 2022 at 19:50):

Ah, do you know when he'll be back? Knowing could help us with project planning/which parts of the plugin to focus on. (Happy to hear from Thierry, though, if he can help)

Talia Ringer (Dec 01 2022 at 19:52):

Also @Arpan Agrawal I hadn't read this conversation until now, but from this it sounds like it might be worth looking at PyCoq and playing with it in case it turns out it is two-sided communication, even if you don't hear from Emilio

Théo Zimmermann (Dec 01 2022 at 19:53):

Talia Ringer said:

Ah, do you know when he'll be back? Knowing could help us with project planning/which parts of the plugin to focus on. (Happy to hear from Thierry, though, if he can help)

Next week, I think.

Talia Ringer (Dec 01 2022 at 19:53):

Oh, thanks! That's good to know, we definitely have more than a week's worth of other things we could do haha

Ali Caglayan (Dec 01 2022 at 20:37):

What part are you having trouble with? pyml should work the same as any other OCaml library dep in a plugin.

Ali Caglayan (Dec 01 2022 at 20:38):

Here is an example of a plugin project in Dune if this helps: https://dune.readthedocs.io/en/stable/coq.html#coq-plugin-project

Arpan Agrawal (Dec 01 2022 at 21:26):

Thanks! I've tried with that template and run into this issue: https://github.com/ocaml/dune/issues/5998

Thierry Martinez (Dec 01 2022 at 22:20):

Arpan Agrawal said:

Thanks! I've tried with that template and run into this issue: https://github.com/ocaml/dune/issues/5998

Could you share a code reproducing this issue? The discussion on issue 5998 mentions several possible errors.

Arpan Agrawal (Dec 01 2022 at 22:24):

Its the plugin template with pyml added as a dependency in the dune file and this function added in the .ml file:

let init ?interpreter ?version () =
if not (Py.is_initialized ()) then (
Printf.eprintf "pyml-pyplot: initializing python... " ;
Py.initialize ?interpreter ?version () ;
Printf.eprintf "pyml-pyplot: done.\n%!" ) ;
if not (Py.is_initialized ()) then (
Printf.printf "pyml-pyplot: can't initialize Python, exiting" ;
exit 1 )

Ali Caglayan (Dec 01 2022 at 22:25):

What is the error exactly?

Ali Caglayan (Dec 01 2022 at 22:25):

Also which version of Coq?

Arpan Agrawal (Dec 01 2022 at 22:25):

Then running dune build results in:

File "./theories/MyPlugin.v", line 1, characters 0-51:
Error:
Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/home/arpan/Downloads/coq-plugin-template/_build/default/src/my_plugin.cmxs: undefined symbol: camlPy\")")
Findlib paths:

Followed by a bunch of paths

Arpan Agrawal (Dec 01 2022 at 22:26):

Coq 8.16.0

Ali Caglayan (Dec 01 2022 at 22:27):

How did you install pyml? via opam?

Ali Caglayan (Dec 01 2022 at 22:28):

Also where did you add the pyml dep? Did you add it to the (plugins) field of the theory stanza as well?

Ali Caglayan (Dec 01 2022 at 22:28):

This findlib error is from Coq, so I suspect the correct -I flag wasn't passed.

Ali Caglayan (Dec 01 2022 at 22:29):

For that to happen you should include pyml in the (plugins) field.

Arpan Agrawal (Dec 01 2022 at 22:29):

Pyml was installed via opam, yes

Ali Caglayan (Dec 01 2022 at 22:32):

so pyml should be included in the (libraries) field of the (library ) stanza and the (plugins ) field of the (coq.theory ) stanza.

Ali Caglayan (Dec 01 2022 at 22:33):

Coq sucks at loading plugins transitively, but perhaps Dune could be smarter here and pass the transitive closure of the plugins field rather than just -Iing the plugins.

Ali Caglayan (Dec 01 2022 at 22:33):

Let me know if that works for you.

Arpan Agrawal (Dec 01 2022 at 22:34):

Error changed to:
File "./theories/MyPlugin.v", line 1, characters 0-51:
Error: Can't find file my_plugin.cmxs on loadpath.

Ali Caglayan (Dec 01 2022 at 22:37):

Ok some progress. Can you paste your (library) stanza?

Ali Caglayan (Dec 01 2022 at 22:39):

Right so in Coq 8.16 you no longer use the name my_plugin.

Arpan Agrawal (Dec 01 2022 at 22:39):

(library
(name my_plugin) ; This is the name you will use in
; Coq's Declare ML Module, and
; the name of the main OCaml
; module of your plugin.

(public_name pyml.plugin) ; This makes the plugin
; installable; recommended, must
; match opam package name.

(synopsis "My Coq plugin") ; Synopsis, used in META generation.

(flags :standard -rectypes -w -27) ; Coq requires the -rectypes
; flag; CoqPP generated code
; requires to disable warning 27
; often.

(foreign_stubs ; we link our plugin with a C
(language c) ; library! Optional, of course.
(names ce_get))

(libraries ; OCaml Libraries we want to link
; with, your choice here.

coq-core.vernac ; Needed for vernac extend.
coq-core.plugins.ltac ; Needed for tactic extend.
pyml ; For Python-OCaml interaction.
)
)

; This will let Dune know about Coq's .mlg grammar files.
(coq.pp (modules ce_syntax))

Ali Caglayan (Dec 01 2022 at 22:39):

You need to use the public_name which is pyml.plugin.

Ali Caglayan (Dec 01 2022 at 22:39):

So Declare ML Module "pyml.plugin".

Ali Caglayan (Dec 01 2022 at 22:40):

Is this Dune file from Emilio's tutorial from a while back?

Arpan Agrawal (Dec 01 2022 at 22:40):

Yes

Ali Caglayan (Dec 01 2022 at 22:40):

Coq's plugin loading has changed a bit since then. Let me know if using the public_name works for you.

Arpan Agrawal (Dec 01 2022 at 22:43):

Ali Caglayan said:

So Declare ML Module "pyml.plugin".

Isnt the naming convention different for coq 8.16?

Arpan Agrawal (Dec 01 2022 at 22:43):

File "./theories/MyPlugin.v", line 1, characters 0-32:
Error:
Findlib error: pyml.plugin not found in:

Followed by the paths from earlier

Arpan Agrawal (Dec 01 2022 at 22:44):

Arpan Agrawal said:

File "./theories/MyPlugin.v", line 1, characters 0-32:
Error:
Findlib error: pyml.plugin not found in:

Followed by the paths from earlier

This is after doing Declare ML Module "pyml.plugin"

Ali Caglayan (Dec 01 2022 at 22:44):

Try Declare ML Module "my_plugin:pyml.plugin"..

Ali Caglayan (Dec 01 2022 at 22:45):

And also what does your (coq.theory) stanza look like

Arpan Agrawal (Dec 01 2022 at 22:46):

(coq.theory
(name MyPlugin) ; This will determine the top-level Coq
; module of your theory, modules will
; be MyPlugin.A, etc., when seen from the
; outside.

(package pyml) ; Adding this line will make your
; library installable in the opam package

                               ; for your Coq files.

(plugins pyml))
; Other important fields are modules and flags, see Dune
; documentation for more details.

Arpan Agrawal (Dec 01 2022 at 22:50):

Ali Caglayan said:

Try Declare ML Module "my_plugin:pyml.plugin"..

Results in this:

File "./theories/MyPlugin.v", line 1, characters 0-42:
Error: Can't find file my_plugin.cmxs on loadpath.

Arpan Agrawal (Dec 01 2022 at 22:52):

Ali Caglayan said:

Try Declare ML Module "my_plugin:pyml.plugin"..

I changed it to "pyml:pyml.plugin" and now the Dynlink Error says:

File "./theories/MyPlugin.v", line 1, characters 0-37:
Error:
Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/home/arpan/.opam/duneplugin/lib/pyml/pyml.cmxs: undefined symbol: camlStdcompat\")")

Ali Caglayan (Dec 01 2022 at 23:08):

Right you have to play the same game as before.

Ali Caglayan (Dec 01 2022 at 23:09):

I mentioned that Coq cannot handle (discover) transitive deps (for plugins) so you will have to add them in yourself.

Ali Caglayan (Dec 01 2022 at 23:09):

The stanza of pyml has: (libraries unix bigarray stdcompat)) so you will need to add these to the plugins field too.

Ali Caglayan (Dec 01 2022 at 23:09):

I believe that should be the last of them however.

Ali Caglayan (Dec 01 2022 at 23:10):

I've submitted a Dune bug about doing this transitive closure in Dune btw, and if I have time I might be able to implement it soon. But that will obviously land in a much later Dune version.

Arpan Agrawal (Dec 01 2022 at 23:23):

Thanks a lot for all your help! I will try this out

Arpan Agrawal (Dec 02 2022 at 18:03):

Just to report back on this: That didnt resolve the error

Arpan Agrawal (Dec 02 2022 at 18:04):

Still getting the same error. I tried to get a fresh start with the plugin template, without changing the name, but now it cant even link pyml

Arpan Agrawal (Dec 02 2022 at 18:33):

@Ali Caglayan
Do you know why this could be happening?

Here's the (library) stanza:

(library
(name my_plugin) ; This is the name you will use in
; Coq's Declare ML Module, and
; the name of the main OCaml
; module of your plugin.

(public_name coq-my-plugin.plugin) ; This makes the plugin
; installable; recommended, must
; match opam package name.

(synopsis "My Coq plugin") ; Synopsis, used in META generation.

(flags :standard -rectypes -w -27) ; Coq requires the -rectypes
; flag; CoqPP generated code
; requires to disable warning 27
; often.

(foreign_stubs ; we link our plugin with a C
(language c) ; library! Optional, of course.
(names ce_get))

(libraries ; OCaml Libraries we want to link
pyml ; with, your choice here.
unix
bigarray
stdcompat
coq-core.vernac ; Needed for vernac extend.
coq-core.plugins.ltac ; Needed for tactic extend.
)
)

; This will let Dune know about Coq's .mlg grammar files.
(coq.pp (modules ce_syntax))

And here's the (coq.theory):

(coq.theory
(name MyPlugin) ; This will determine the top-level Coq
; module of your theory, modules will
; be MyPlugin.A, etc., when seen from the
; outside.

(package coq-my-plugin) ; Adding this line will make your
; library installable in the opam package

                               ; OCaml plugin dependencies
                               ; for your Coq files.

(plugins pyml coq-my-plugin.plugin stdcompat unix bigarray))
; Other important fields are modules and flags, see Dune
; documentation for more details.

Ali Caglayan (Dec 02 2022 at 18:34):

@Arpan Agrawal Could you put ``` above and below your code comments so we can read them?

Ali Caglayan (Dec 02 2022 at 18:37):

What is the error message this time round?

Ali Caglayan (Dec 02 2022 at 18:37):

Also what was wrong with your previous Dune file?

Arpan Agrawal (Dec 02 2022 at 18:39):

Ali Caglayan said:

What is the error message this time round?

Dynlink error for camlPy

Arpan Agrawal (Dec 02 2022 at 18:39):

Ali Caglayan said:

Also what was wrong with your previous Dune file?

Dynlink error for camlStdcompat

Arpan Agrawal (Dec 02 2022 at 18:40):

Here's the stanzas without comments:

(library
(name my_plugin)
(public_name coq-my-plugin.plugin)
(synopsis "My Coq plugin")
(flags :standard -rectypes -w -27)
(foreign_stubs
(language c)
(names ce_get))
(libraries
link
pyml
unix
bigarray
stdcompat
coq-core.vernac
coq-core.plugins.ltac
)
)
(coq.pp (modules ce_syntax))

and

(coq.theory
(name MyPlugin)
(package coq-my-plugin)
(plugins pyml coq-my-plugin.plugin stdcompat unix bigarray))

Ali Caglayan (Dec 03 2022 at 17:29):

Your (plugins) field needs to have all the (libraries) from your library stanza. There are still some missing.

Arpan Agrawal (Dec 05 2022 at 16:28):

@Ali Caglayan that doesnt change the error, still running into a dynlink error for camlPy

Ali Caglayan (Dec 05 2022 at 17:35):

Could you put it in a repo so I can take a look later?

Emilio Jesús Gallego Arias (Dec 06 2022 at 14:05):

IIUC, the error is the classical one, Coq won't autoload deps in legacy mode, and Dune will fail in findlib mode due to https://github.com/coq/coq/issues/16571

I think most efficiently would be to fix the above bug, if my analysis is correct. Then everything should work out of the box

Arpan Agrawal (Dec 06 2022 at 17:59):

Is there no way to get it working currently? (Even if its not easily reproducible)

Arpan Agrawal (Dec 16 2022 at 15:21):

@Emilio Jesús Gallego Arias wanted to follow up on this, is there no way to use pyml in a dune based plugin currently?

Emilio Jesús Gallego Arias (Dec 16 2022 at 15:36):

Hi @Arpan Agrawal , yes, there is a way; to summarize:

streamlined support is blocked by https://github.com/coq/coq/issues/16571
you can either then use -linkall in your plugin linking code, best way is to use (executable ...) with (mode plugin)
query ocamlfind to see what your plugin depends on, and simulate loading all the deps with Declare Ml Module

Anyways, I'm sorry I can't provide better support these days about these low-level OCaml issues, I'm just don't have the time to provide general support for Coq and OCaml development, you may have better luck asking in OCaml-help specific forums.

Last updated: Jun 08 2023 at 04:01 UTC