Stream: Coq devs & plugin devs

Topic: Pyml with dune for plugin


view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Nov 28 2022 at 18:20):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 )

view this post on Zulip Ali Caglayan (Dec 01 2022 at 22:25):

What is the error exactly?

view this post on Zulip Ali Caglayan (Dec 01 2022 at 22:25):

Also which version of Coq?

view this post on Zulip 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

view this post on Zulip Arpan Agrawal (Dec 01 2022 at 22:26):

Coq 8.16.0

view this post on Zulip Ali Caglayan (Dec 01 2022 at 22:27):

How did you install pyml? via opam?

view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Dec 01 2022 at 22:28):

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

view this post on Zulip Ali Caglayan (Dec 01 2022 at 22:29):

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

view this post on Zulip Arpan Agrawal (Dec 01 2022 at 22:29):

Pyml was installed via opam, yes

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Dec 01 2022 at 22:33):

Let me know if that works for you.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Dec 01 2022 at 22:37):

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

view this post on Zulip Ali Caglayan (Dec 01 2022 at 22:39):

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

view this post on Zulip 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))

view this post on Zulip Ali Caglayan (Dec 01 2022 at 22:39):

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

view this post on Zulip Ali Caglayan (Dec 01 2022 at 22:39):

So Declare ML Module "pyml.plugin".

view this post on Zulip Ali Caglayan (Dec 01 2022 at 22:40):

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

view this post on Zulip Arpan Agrawal (Dec 01 2022 at 22:40):

Yes

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Ali Caglayan (Dec 01 2022 at 22:44):

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

view this post on Zulip Ali Caglayan (Dec 01 2022 at 22:45):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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\")")

view this post on Zulip Ali Caglayan (Dec 01 2022 at 23:08):

Right you have to play the same game as before.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Dec 01 2022 at 23:09):

I believe that should be the last of them however.

view this post on Zulip 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.

view this post on Zulip Arpan Agrawal (Dec 01 2022 at 23:23):

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

view this post on Zulip Arpan Agrawal (Dec 02 2022 at 18:03):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Dec 02 2022 at 18:34):

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

view this post on Zulip Ali Caglayan (Dec 02 2022 at 18:37):

What is the error message this time round?

view this post on Zulip Ali Caglayan (Dec 02 2022 at 18:37):

Also what was wrong with your previous Dune file?

view this post on Zulip Arpan Agrawal (Dec 02 2022 at 18:39):

Ali Caglayan said:

What is the error message this time round?

Dynlink error for camlPy

view this post on Zulip Arpan Agrawal (Dec 02 2022 at 18:39):

Ali Caglayan said:

Also what was wrong with your previous Dune file?

Dynlink error for camlStdcompat

view this post on Zulip 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))

view this post on Zulip 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.

view this post on Zulip Arpan Agrawal (Dec 05 2022 at 16:28):

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

view this post on Zulip Ali Caglayan (Dec 05 2022 at 17:35):

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

view this post on Zulip 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

view this post on Zulip Arpan Agrawal (Dec 06 2022 at 17:59):

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

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 16 2022 at 15:36):

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

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: Mar 28 2024 at 16:02 UTC