Stream: Coq devs & plugin devs

Topic: ✔ Plugins and coq versions

Julin S (Jul 06 2022 at 06:32):

I was trying out the hello world plugin at https://github.com/coq/coq/tree/master/doc/plugin_tutorial/tuto0

Should the plugin source code be changed inorder to work with each newer coq version?

Because had to change branch when using with different coq version inorder for it compile.

Julin S (Jul 06 2022 at 06:33):

And what does Pp mean in open Pp?

Julin S (Jul 06 2022 at 06:33):

Pretty printing?

Julin S (Jul 06 2022 at 06:36):

The documentation seems a bit too concise: https://ocaml.org/p/coq/8.12.0/doc/Pp/index.html#val-strbrk (I'm new to ocaml)

Guillaume Melquiond (Jul 06 2022 at 06:42):

Julin S said:

Should the plugin source code be changed inorder to work with each newer coq version?

Yes. Coq does not provide any compatibility guarantee for plugins. So, unless it is a trivial do-nothing plugin, its source code has to be specific to each Coq version.

Julin S (Jul 06 2022 at 06:44):

What part of coq is responsible for the incompatibility?

I mean, is it an api or something?

Guillaume Melquiond (Jul 06 2022 at 06:45):

Julin S said:

And what does Pp mean in open Pp?

Pp is the name of an OCaml module provided by Coq. It is indeed responsible for pretty-printing (nothing fancy, mostly indentation), hence its name.

Guillaume Melquiond (Jul 06 2022 at 06:46):

Julin S said:

I mean, is it an api or something?

Yes, Coq's API is not stable, it is constantly changing.

Julin S (Jul 06 2022 at 06:55):

Thanks!

Notification Bot (Jul 06 2022 at 06:55):

Julin S has marked this topic as resolved.

Julin S (Jul 06 2022 at 06:56):

Are stuff like metacoq made as plugins? Quite a large code base to fix if it is to support every new coq version.

Kenji Maillard (Jul 06 2022 at 07:55):

Metacoq contains a small plugin to do reification/reflection (transform some piece of Coq code into an ast representation that can be manipulated directly in Gallina) and access the proofstate. However most of Metacoq, and indeed all of its proofs, consists just of regular Gallina code and does not rely on the plugin.

Enrico Tassi (Jul 06 2022 at 08:38):

Julin S said:

Are stuff like metacoq made as plugins? Quite a large code base to fix if it is to support every new coq version.

Coq-Elpi is a plugin and uses a lot of APIs which are indeed changing, but it is in Coq's CI so when changes happen the devs typically submit a patch. If you develop your own plugin you should really consider doing the same.

Julin S (Jul 07 2022 at 09:07):

And is there more documentation to the coq api than just the types of functions?

I had been looking at https://ocaml.org/p/coq/8.12.0/doc/Proofview/index.html

but couldn't really figure out what each of the functions would do.

How is it usually done? Do people look into the source code itself or is there some documentation that I'm missing?

Gaëtan Gilbert (Jul 07 2022 at 09:19):

why are you looking at 8.12? It looks like it got generated wrong.
https://ocaml.org/p/coq/8.15.0/doc/Proofview/index.html has some more info
In general I do look at the source rather than html generated stuff

Enrico Tassi (Jul 07 2022 at 09:20):

In the coq sources you have some doc in dev/
I find the .mli not very well documented, and that is what you see online.

What are you really trying to implement? The hope is that today you would not need to understand the ocaml API, but hopefully use one of the various extension languages (Elpi, Ltac2, MetaCoq-Template...). They have smaller and more curated APIs. What is your use case?

Julin S (Jul 07 2022 at 09:24):

I wasn't yet doing anything serious. Just wanted to understand how extraction works in coq. Been using old coq version because... uh.. been too lazy to update.

Julin S (Jul 07 2022 at 09:24):

Hadn't known about elpi.

Julin S (Jul 07 2022 at 09:25):

metacoq-template is same as template-coq, right? Or is it different?

Julin S (Jul 07 2022 at 09:27):

Never tried ltac2 but the mention of 'missing usability features' at https://coq.inria.fr/refman/proof-engine/ltac2.html sort of made me scared.

Kenji Maillard (Jul 07 2022 at 09:29):

Template-coq is the name of the "old"/original name of metacoq. At the time I think the project was mostly concerned with reification/reflection

Kenji Maillard (Jul 07 2022 at 09:32):

If you are interested in extraction, there is an ongoing work in metacoq to formalize Coq's extraction mechanism (certicoq is also relevant on the topic of extraction). The main written reference on extraction is probably remains Letouzey's PhD Thesis.

Ali Caglayan (Jul 07 2022 at 09:45):

Julin S said:

I wasn't yet doing anything serious. Just wanted to understand how extraction works in coq. Been using old coq version because... uh.. been too lazy to update.

Extraction isn't the easiest code to understand, but you can find all of it in plugins/extraction.

Julin S (Jul 08 2022 at 04:12):

Thanks folks.

I was just playing around and thought it would be cool to see how it worked. Maybe I should begin smaller.

Julin S (Jul 08 2022 at 07:41):

Just found in the metacoq website:

At the center of this project is the Template-Coq quoting library for Coq

So I guess Template-Coq is something that's part of metacoq?

Théo Winterhalter (Jul 08 2022 at 07:51):

Yeah Template-Coq and metacoq-template are the same thing.

Last updated: Oct 12 2024 at 13:01 UTC