walker (Aug 03 2022 at 16:59): walker (Aug 03 2022 at 16:59):I am trying to write extraction plugin for coq, basically being separate plugin, and I am having hard time working my head around Coq, API, is there a way to load coq libraries in utop to explore things interactively ?
Gaëtan Gilbert (Aug 03 2022 at 19:14):I think dune utop is supposed to work
cc @Emilio Jesús Gallego Arias
walker (Aug 03 2022 at 19:44):I am absolutely clueless here.....
walker (Aug 03 2022 at 19:52):I am building my plugin with coq make files as in the tutorial
so dune is not working.
Emilio Jesús Gallego Arias (Aug 04 2022 at 10:04):Yup, dune utop works, but you'll have a to setup a dune file for your plugin
walker (Aug 04 2022 at 10:36):@Emilio Jesús Gallego Arias is there a place where I can learn how to do that ?
Emilio Jesús Gallego Arias (Aug 04 2022 at 11:21):What Coq version are you ?
Enrico Tassi (Aug 04 2022 at 11:58):walker said:
I am trying to write extraction plugin for coq, basically being separate plugin, and I am having hard time working my head around Coq, API, is there a way to load coq libraries in utop to explore things interactively ?
IMO, to start a new project, you should consider not using OCaml, but rather Coq-Elpi or Metacoq. Both give you the syntax of Coq terms (complete in metacoq, no mutual fix in Elpi) and a way to get any existing term in that syntax, to manipulate it and to save the result (or print it).
Enrico Tassi (Aug 04 2022 at 12:00):When you have the prototype running, then you may consider rewriting it in OCaml, if you need more speed for example. But only then.
walker (Aug 04 2022 at 12:35):I am really struggling with ocaml (compilation errors and linking erros) so would you susggest matacoq or elpi ?
walker (Aug 04 2022 at 12:36):I am trying to write plugin to extract coq code to rust, and none of the solutions seams to work well (lack documentation or outdated).
walker (Aug 04 2022 at 13:21):oh elpi is prolog , I didn't like prolog when I once tried it ... I am sticking to metacoq (until I find reason not to do so)
Alexander Gryzlov (Aug 04 2022 at 14:17):It's lambdaProlog, so probably not as bad :)
walker (Aug 04 2022 at 14:22):Ok, I need to be careful here, because I invested time learning ocaml so I don't want to waste lots of time in the wrong direction
walker (Aug 04 2022 at 14:23):current goal is to extract some coq code to Rust, while making heavy use of rust standard API.
walker (Aug 04 2022 at 14:26):option 1) existing tools (all of them look outdated)
option 2) write plugin in Ocaml (currently I am getting link error at runtime)
option 3) write plugin in elpi
option 4) write plugin in metacoq
Here are my concerns about elpi and metacoq, are they full programming languages, can I just write stuff to files and interact with the outside world?
Another concern, is there (at least informal ) support for out of tree ocaml coq plugins ? For instance, (as of right now) linking errors and things like that, would devs be interested in figuring out the issue and resolving it if it is on coq's side ?
Gaëtan Gilbert (Aug 04 2022 at 14:28):nobody will try to figure out an issue when the only description is "there exists some error"
walker (Aug 04 2022 at 14:34):nobody will try to figure out an issue when the only description is "there exists some error"
I will take that as a yes. then, I can be more specific, but I wanted to dig things out myself first. but here we go so I am trying to build pluign using both _Coqproject and dune, in both cases, I am getting
Runtime error from Ocam's Dynlinker:
error Dynlink.Cannot_open_dll "Failure(\"/path/to/src/RustExtractionPlugin.cmxs: undefined symbol: camlExtraction_plugin__Table\")")
So I checked in _CoqProject build system that -linkall is being used, and in dune building I checked that the right library exists as follows:
walker (Aug 04 2022 at 14:34):(library
(name RustExtractionPlugin)
(public_name coq_rust.plugin)
(libraries
coq-core.plugins.ltac
coq-core.plugins.extraction
)
(flags :standard -rectypes -w -27)
)
When I remove the coq-core.plugins.extraction I get compile time error about those lines:
open Extraction_plugin.Table
So that means that Extraction_plugin.Table is viewable at compile time.
walker (Aug 04 2022 at 14:36):but for some reason when I do
Declare ML Module "RustExtractionPlugin".
in coq, it does not detect that RustExtractionPlugin depends on ExtractionPlugin.
walker (Aug 04 2022 at 14:38):The only thing that worried me that maybe Coq's extraction plugin does not export the correct symbol.
walker (Aug 04 2022 at 14:39):so I checked ~/.opam/default/lib/coq-core/plugins/extraction/extraction_plugin.cmxs manually and I found that camlExtraction_plugin__Table is global symbol.
walker (Aug 04 2022 at 14:39):so the problem is Coq extration plugin experts Table to be used, dune can see that my project depends on it at compile time.
walker (Aug 04 2022 at 14:39):Coq fails to import it at runtime when I import my plugin.
walker (Aug 04 2022 at 14:41):I am not 100% comitted to this approach if it is not supproted by coq, but I need to have rust extraction from Coq, so I am open to available approaches.
Gaëtan Gilbert (Aug 04 2022 at 14:46):what coq version?
walker (Aug 04 2022 at 14:48):The Coq Proof Assistant, version 8.15.2
compiled with OCaml 4.13.1
Emilio Jesús Gallego Arias (Aug 04 2022 at 14:48):You need to do Declare ML Module "extraction_plugin" before your own
Emilio Jesús Gallego Arias (Aug 04 2022 at 14:48):This is fixed in 8.16
Emilio Jesús Gallego Arias (Aug 04 2022 at 14:48):Declare ML Module is not aware of dependencies among plugins
walker (Aug 04 2022 at 14:49):omg! that works
walker (Aug 04 2022 at 14:49):how do you debug issues like that ?
walker (Aug 04 2022 at 14:50):also really thanks a lot!
Emilio Jesús Gallego Arias (Aug 04 2022 at 15:13):You debug asking around here, that's pretty low-level stuff, tho it is documented in some of my build projects
Emilio Jesús Gallego Arias (Aug 04 2022 at 15:13):like in the dune template
Enrico Tassi (Aug 05 2022 at 12:36):What is going to be the hard part? Do you want to massage coq terms a lot? Do you want to reuse some parts of ocaml extraction?
I mean, there are plenty of ways to go, you couls even extract to json and do the heavy work in rust itself...
walker (Aug 05 2022 at 13:55):JSON and the heavy part in rust looks now very tempting but it is too late, I kinda learned ocaml and I am putting it to good use.
walker (Aug 05 2022 at 13:55):actually coq's team is more helpful than I imagined.
Enrico Tassi (Aug 05 2022 at 17:41):@Emilio Jesús Gallego Arias isn't the work around you suggested unnecessary on 8.16?
Paolo Giarrusso (Aug 05 2022 at 18:12):https://github.com/ocaml/dune/issues/5998#issuecomment-1195423937 describes some remaining problems
Paolo Giarrusso (Aug 05 2022 at 18:13):but yeah, many problems are already solved in 8.16 (as shown in https://github.com/ejgallego/coq-plugin-template), this discussion is still about 8.15
Emilio Jesús Gallego Arias (Aug 07 2022 at 22:33):Enrico Tassi said:
Emilio Jesús Gallego Arias isn't the work around you suggested unnecessary on 8.16?
As I wrote: "This is fixed in 8.16"
Last updated: Oct 03 2023 at 04:02 UTC