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!
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
for the record, the pyml core developer is one of the authors of PyCoq
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
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)
That would be great if its the case. @Emilio Jesús Gallego Arias please let me know when you get the chance
@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
Emilio is away from the internet at the current time. But maybe @Thierry Martinez can chim in.
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)
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
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.
Oh, thanks! That's good to know, we definitely have more than a week's worth of other things we could do haha
What part are you having trouble with? pyml should work the same as any other OCaml library dep in a plugin.
Here is an example of a plugin project in Dune if this helps: https://dune.readthedocs.io/en/stable/coq.html#coq-plugin-project
Thanks! I've tried with that template and run into this issue: https://github.com/ocaml/dune/issues/5998
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.
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 )
What is the error exactly?
Also which version of Coq?
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
Coq 8.16.0
How did you install pyml? via opam?
Also where did you add the pyml dep? Did you add it to the (plugins)
field of the theory stanza as well?
This findlib error is from Coq, so I suspect the correct -I flag wasn't passed.
For that to happen you should include pyml
in the (plugins)
field.
Pyml was installed via opam, yes
so pyml
should be included in the (libraries)
field of the (library )
stanza and the (plugins )
field of the (coq.theory )
stanza.
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 -I
ing the plugins.
Let me know if that works for you.
Error changed to:
File "./theories/MyPlugin.v", line 1, characters 0-51:
Error: Can't find file my_plugin.cmxs on loadpath.
Ok some progress. Can you paste your (library)
stanza?
Right so in Coq 8.16 you no longer use the name my_plugin.
(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))
You need to use the public_name which is pyml.plugin.
So Declare ML Module "pyml.plugin".
Is this Dune file from Emilio's tutorial from a while back?
Yes
Coq's plugin loading has changed a bit since then. Let me know if using the public_name works for you.
Ali Caglayan said:
So
Declare ML Module "pyml.plugin".
Isnt the naming convention different for coq 8.16?
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 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"
Try Declare ML Module "my_plugin:pyml.plugin".
.
And also what does your (coq.theory) stanza look like
(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.
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.
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\")")
Right you have to play the same game as before.
I mentioned that Coq cannot handle (discover) transitive deps (for plugins) so you will have to add them in yourself.
The stanza of pyml has: (libraries unix bigarray stdcompat))
so you will need to add these to the plugins field too.
I believe that should be the last of them however.
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.
Thanks a lot for all your help! I will try this out
Just to report back on this: That didnt resolve the error
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
@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.
@Arpan Agrawal Could you put ``` above and below your code comments so we can read them?
What is the error message this time round?
Also what was wrong with your previous Dune file?
Ali Caglayan said:
What is the error message this time round?
Dynlink error for camlPy
Ali Caglayan said:
Also what was wrong with your previous Dune file?
Dynlink error for camlStdcompat
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))
Your (plugins) field needs to have all the (libraries) from your library stanza. There are still some missing.
@Ali Caglayan that doesnt change the error, still running into a dynlink error for camlPy
Could you put it in a repo so I can take a look later?
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
Is there no way to get it working currently? (Even if its not easily reproducible)
@Emilio Jesús Gallego Arias wanted to follow up on this, is there no way to use pyml in a dune based plugin currently?
Hi @Arpan Agrawal , yes, there is a way; to summarize:
-linkall
in your plugin linking code, best way is to use (executable ...)
with (mode plugin)
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