Stream: Dune devs & users

Topic: Template Coq plugin repo


view this post on Zulip Karl Palmskog (Jun 20 2023 at 22:32):

We now transferred the repo successfully to coq-community: https://github.com/coq-community/coq-plugin-template

However, is the goal now to always have the default branch be for the latest released version of Coq (e.g., v8.17)? Should there be a branch for Coq master that is also in Coq's CI?

view this post on Zulip Karl Palmskog (Jun 20 2023 at 22:33):

Potentially, this repo could be linked in various official documentation places, such as Dune's and Coq's, so would be good to figure out what the goal is.

view this post on Zulip Karl Palmskog (Jun 20 2023 at 22:35):

my view is something like: the goal of the repo is to be forkable and inspire writing plugins with Dune for latest released version of Coq, so v8.17 as default makes sense. But having some branch that's in Coq's CI and tracks Coq master might ease maintenance (we just branch off this when 8.XY.0 is out)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 20 2023 at 22:38):

I'm unsure how to organize the branches, the support matrix for Dune and Coq looks like:

So indeed I would expect that we drop support for Coq < 8.13 , and maybe mark that Coq + findlib Ml plugin requires 8.17.1

view this post on Zulip Emilio Jesús Gallego Arias (Jun 20 2023 at 22:38):

We tried to be very careful in Dune as not to couple with Coq

view this post on Zulip Karl Palmskog (Jun 20 2023 at 22:39):

but the example uses .mlg code that might break as Coq evolves

view this post on Zulip Emilio Jesús Gallego Arias (Jun 20 2023 at 22:40):

view this post on Zulip Emilio Jesús Gallego Arias (Jun 20 2023 at 22:40):

Karl Palmskog said:

but the example uses .mlg code that might break as Coq evolves

Yup, but that'd be a lot of duplication. We could try to have a single template and use %{coq:version} to handle this

view this post on Zulip Emilio Jesús Gallego Arias (Jun 20 2023 at 22:40):

So we'd have a file coq_api_8.17.ml coq_api_dev.ml etc....

view this post on Zulip Emilio Jesús Gallego Arias (Jun 20 2023 at 22:41):

and a rule:

(rule
  (action (copy coq_api_%{coq:version}.ml coq_api.ml)))

view this post on Zulip Karl Palmskog (Jun 20 2023 at 22:41):

wouldn't that be a bit confusing for those who clone or fork?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 20 2023 at 22:41):

Maybe, I don't kno

view this post on Zulip Emilio Jesús Gallego Arias (Jun 20 2023 at 22:41):

I don't know

view this post on Zulip Emilio Jesús Gallego Arias (Jun 20 2023 at 22:42):

A very simple Coq plugin can be also made work in a lot of Coq versions

view this post on Zulip Emilio Jesús Gallego Arias (Jun 20 2023 at 22:42):

I was thinking that having a few of 8.17 8.18 branches which are in terms of dune identical, would be maybe confusing

view this post on Zulip Emilio Jesús Gallego Arias (Jun 20 2023 at 22:42):

If the goal of the template is to be a plugin tutorial indeed that makes sense

view this post on Zulip Emilio Jesús Gallego Arias (Jun 20 2023 at 22:42):

if the goal is to be a dune tutorial, Coq version has very little impact (thankfully)

view this post on Zulip Karl Palmskog (Jun 20 2023 at 22:43):

well, I see it as a combination of writing OCaml code that does something with Coq's ML API, and letting Dune do as much as possible of the lifting, and including opam packaging

view this post on Zulip Karl Palmskog (Jun 20 2023 at 22:44):

if you think we can have a regular main/master branch that is compatible with a range of Coq versions under that premise, that may be easiest

view this post on Zulip Théo Zimmermann (Jun 21 2023 at 09:18):

I think it would be appropriate to check the "Template repository" checkbox under the general repository settings. Docs are here: https://docs.github.com/en/repositories/creating-and-managing-repositories/creating-a-repository-from-a-template

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2023 at 11:50):

Karl Palmskog said:

if you think we can have a regular main/master branch that is compatible with a range of Coq versions under that premise, that may be easiest

I think that indeed showcasing a plugin that supports several Coq versions could be useful, as this seems to be a common case for at least a few people.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2023 at 11:50):

But indeed I'm unsure what the people would like to see there.

view this post on Zulip Karl Palmskog (Jun 21 2023 at 12:36):

don't we want something like the following:

You can use this plugin as a template for developing your own plugin using Dune for these Coq versions: 8.16, 8.17 and Coq master. However, as soon as you select a Coq version and use Coq's ML API for that version in a nontrivial way, you will likely be bound to this version due to ML API changes between Coq versions.

view this post on Zulip Karl Palmskog (Jun 21 2023 at 12:37):

(not sure about exact version range, so view as an example)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2023 at 13:41):

That depends if we include version-specific files in the build setup or not

view this post on Zulip Karl Palmskog (Jun 21 2023 at 13:41):

but how far can we get without including anything version-specific in the setup?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2023 at 13:45):

Not very far, but a plugin is workable. You can diff the plugin_tutoriall in Coq sources to see what the changes among versions are (not many)

On the other hand it seems to me that a template should actually illustrate how to support several Coq versions using the build system, that's a bit of an special case. Supporting only a single Coq version is easy (nothing to do other than the regular ML setup)

view this post on Zulip Karl Palmskog (Jun 21 2023 at 15:57):

OK, my view would be to as a first step, create some default branch not tied to a Coq version, then:

  1. quickly get this branch to work with as many Coq versions as possible, including at least 8.17, without using %{coq:version} or similar
  2. work on the "illustrate how to support several Coq versions" in the longer term

view this post on Zulip Karl Palmskog (Jun 21 2023 at 16:00):

if we do step 1, then we can at least start to recommend/link it for forking and use in documentation, right now

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2023 at 16:01):

1 is already done

view this post on Zulip Emilio Jesús Gallego Arias (Jun 21 2023 at 16:03):

I'm unsure what "to work with as many Coq versions" means tho, a trivial plugin will work with all supported Coq versions, but will not be very useful.

view this post on Zulip Karl Palmskog (Jun 26 2023 at 11:03):

@Emilio Jesús Gallego Arias any chance for a quick eye/approval of my changes here? It would be nice to set up v8.17 as the default branch so we can mark this repo as a (working) template repo

view this post on Zulip Karl Palmskog (Jun 26 2023 at 11:06):

open to changes after that, even to branch structure, but a working v8.17 is enough to market this to people


Last updated: May 25 2024 at 21:01 UTC