Stream: Coq users

Topic: How to explore Coq API


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

view this post on Zulip Gaëtan Gilbert (Aug 03 2022 at 19:14):

I think dune utop is supposed to work
cc @Emilio Jesús Gallego Arias

view this post on Zulip walker (Aug 03 2022 at 19:44):

I am absolutely clueless here.....

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

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

view this post on Zulip walker (Aug 04 2022 at 10:36):

@Emilio Jesús Gallego Arias is there a place where I can learn how to do that ?

view this post on Zulip Emilio Jesús Gallego Arias (Aug 04 2022 at 11:21):

What Coq version are you ?

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

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

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

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

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

view this post on Zulip Alexander Gryzlov (Aug 04 2022 at 14:17):

It's lambdaProlog, so probably not as bad :)

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

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

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

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

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

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

)

view this post on Zulip walker (Aug 04 2022 at 14:35):

When I remove the coq-core.plugins.extraction I get compile time error about those lines:

open Extraction_plugin.Table

view this post on Zulip walker (Aug 04 2022 at 14:36):

So that means that Extraction_plugin.Table is viewable at compile time.

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

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

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

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

view this post on Zulip walker (Aug 04 2022 at 14:39):

Coq fails to import it at runtime when I import my plugin.

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

view this post on Zulip Gaëtan Gilbert (Aug 04 2022 at 14:46):

what coq version?

view this post on Zulip walker (Aug 04 2022 at 14:48):

The Coq Proof Assistant, version 8.15.2
compiled with OCaml 4.13.1

view this post on Zulip Emilio Jesús Gallego Arias (Aug 04 2022 at 14:48):

You need to do Declare ML Module "extraction_plugin" before your own

view this post on Zulip Emilio Jesús Gallego Arias (Aug 04 2022 at 14:48):

This is fixed in 8.16

view this post on Zulip Emilio Jesús Gallego Arias (Aug 04 2022 at 14:48):

Declare ML Module is not aware of dependencies among plugins

view this post on Zulip walker (Aug 04 2022 at 14:49):

omg! that works

view this post on Zulip walker (Aug 04 2022 at 14:49):

how do you debug issues like that ?

view this post on Zulip walker (Aug 04 2022 at 14:50):

also really thanks a lot!

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

view this post on Zulip Emilio Jesús Gallego Arias (Aug 04 2022 at 15:13):

like in the dune template

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

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

view this post on Zulip walker (Aug 05 2022 at 13:55):

actually coq's team is more helpful than I imagined.

view this post on Zulip Enrico Tassi (Aug 05 2022 at 17:41):

@Emilio Jesús Gallego Arias isn't the work around you suggested unnecessary on 8.16?

view this post on Zulip Paolo Giarrusso (Aug 05 2022 at 18:12):

https://github.com/ocaml/dune/issues/5998#issuecomment-1195423937 describes some remaining problems

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

view this post on Zulip 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: Jan 28 2023 at 08:02 UTC