The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Thanks Enrico, I'll take a look at what you did in mathcomp.

On Thu, Jan 12, 2017 at 5:34 PM, Enrico Tassi <enrico.tassi AT inria.fr> wrote:

On Thu, Jan 12, 2017 at 05:20:57PM -0300, Beta Ziliani wrote:
> Hi list,
>
> I want to create packages for different versions of Coq. How do I do that?
> For what I understand from
>
> http://coq-blog.clarus.me/make-a-coq-package.html
>
> packages are listed according to version number, like
>
> coq-unicoq-1.0.0
>
> Now I want to have two more versions of the new 1.1.0 release, one for Coq
> 8.5 and one for 8.6 (since they have different API, the code is slightly
> different). Morally, they are both v1.1.0 of UniCoq. How do I do this?

I see two ways.

If the .v code is mostly the same, while the ml is not, you can put
in the same tarball both "versions" of the ml code and let the Makefile
choose.  We do that in mathcomp.  Then you declare that the OPAM package
works with Coq 8.5 || 8.6.

If the differences are pervasive, then you can make 2 packages using
different sources, with a version number that reflects the Coq version, as
  1.1.0+v8.5 depending on Coq >= 8.5 && < 8.6~
  1.1.0+v8.6 depending on Coq >= 8.6 && < 8.7~
A third party package can then depend on coq-unicoq >= 1.1.0 (both
package above would do, but only one would be installable).  If Coq
itself is pinned to one version, as the instruction on the Coq website
recommend, the fact that the latter version is "syntactically"
greater than the former should not result in an undesired upgrade of
Coq (from 8.5 to 8.6).

Best,
--
Enrico Tassi