The Coq mailing list

[e AT x80.org (Emilio Jesús Gallego Arias)]

Dear Coq plugin writers,

following the 8.7 beta announcement, we think it is a good time to
encourage you all to port your plugins to Coq 8.7 and to consider
whether they would be a candidate for inclusion in the Coq's CI
infrastructure [1,2].

Porting to Coq 8.7:
===================

Unfortunately, Coq 8.7 includes quite a few API changes, see [3] for
a summary and for some hints about porting. In particular, "EConstr"
[4] turns out to be a pretty invasive change in some scenarios.

If you have any question, we encourage you to contact the developers
at Coq's Gitter [5] or mailing list [6].

Porting to Coq 8.8!
===================

A novelty of the 8.7 release cycle is the use of an experimental
Continuous Integration infrastructure, which has allowed developers to
assess the impact of changes on developments. A good compatibility
story is important given that Coq is switching to a 6-month release
schedule.

As of today, the situation wrt plugin compatibility seems far from
optimal, with few plugins being available for 8.7. However, we think
that the CI infrastructure could help alleviate this problem in the
8.8 cycle.

We thus invite you to consider if your plugin could benefit from Coq's
CI infrastructure. The main advantages of adding your development to
the CI are:

- any change in Coq will be tested against you plugin, and Coq
  developers will get a good picture of the impact of their proposals;

- you may get some amount of maintenance "for free". Coq API changes
  are usually required to be accompanied of patches updating
  developments in the CI;

  However, if the plugin is deemed as "misusing the API",
  collaboration with the authors to update the code could be
  requested.

On the other side, when a plugin author requests inclusion in Coq's
CI, they commit to:

- maintain a buildable branch for each Coq stable and development
  branch; this implies that no compilation-breaking changes should be
  made to the branches used by Coq's CI;

- timely integrate API patches sent by Coq developers;

- optionally, you think it would make sense for your plugin to be
  distributed alongside Coq in the medium term, as it provides key
  functionality not yet available in Coq.

It should be remarked again that the above Coq's CI policies and
infrastructure are yet under development and should be considered
experimental; please don't hesitate to comment on this proposal, or
to ask any kind of question: feedback is much appreciated!

Best regards,
The Coq CI team

[1] https://travis-ci.org/coq/coq/
[2] https://github.com/coq/coq/blob/master/README.ci.md
[3] https://github.com/coq/coq/blob/master/dev/doc/changes.txt
[4] https://github.com/coq/coq/blob/master/dev/doc/econstr.md
[5] https://gitter.im/coq/coq
[6] https://sympa.inria.fr/sympa/info/coqdev