The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

> Ideas and comments are very welcome.

Idea one: if some of your tags are not free-form but follow some machine-checkable conventions (well or at least are requested of any package, so their presence is checkable), you should have a tool similar to `opam lint` that knows about them. It should not be that hard to develop given that opam exports its internal libraries to manipulate packge metadata, etc., and maybe `opam lint` itself is customizable in some way -- we started a discussion on that in https://github.com/ocaml/opam/issues/2448 with Louis Gesbert (in cc:).

The OCaml opam-repository relies a lot on continuous integration to facilitate the repository maintainers' work, and those ideas should be reused for the Coq repository.

Idea two: Fabrice Le Fessant (in cc:) develop a tool called opam-builder that checks buildability of all the packages in the OCaml opam repository (it does some clever incrementalization by taking snapshots of the built binaries and skipping the re-builds if none of the dependencies changed, so that it can react a few minutes, at most an hour, to repository changes). See the current output at

  http://opam.ocamlpro.com/builder/html/report-full.html

Having a version of this tool running on the Coq repository could be very helpful for gracious evolution of packages. I'm thinking, for example, that people may place version bounds on their dependencies that are initially too wide (for example coq-coqeal-refinements 0.9.1 currently depends on coq-coqeal >= "0.9.0", but it may be broken by a future backward-incompatible release and need an upper bound to be added at that time), and that continuously monitoring buildability is the robust way to notice these issues and fix them.

The internals of opam-builder seem somewhat obscure right now, and I'm not sure how much work it is to repurpose it for the Coq repository (does some of the incrementality logic need to be changed? if not, then it could be very easy), but I think it could be very interesting for the Coq community.

On Tue, Sep 6, 2016 at 7:39 AM, Enrico Tassi <enrico.tassi AT inria.fr> wrote:

On Tue, Sep 06, 2016 at 01:08:16PM +0200, Maxime Dénès wrote:
> The Coq Development Team is pleased to officially announce the Coq
> Package Index, an online catalog of Coq developments available as OPAM
> packages:
>
>   https://coq.inria.fr/opam/www
>
> Users not familiar with OPAM can find some help on how to install Coq
> and related packages via OPAM at the following page:
>
>   https://coq.inria.fr/opam/www/using.html
>
> Users willing to add their work to the Coq Package Index can find a
> short tutorial at the following page:
>
>   https://coq.inria.fr/opam/www/packaging.html

I'd like to invite people already contributing packages to have a look at

  https://github.com/coq/ceps/blob/master/text/003-opam-metadata.md

The tags field of the opam file can be used to hold interesting, Coq
specific, metadata like keywords, categorization, or the Coq logical
path inhabited by the package.  Such metadata is displayed in the index.

Ideas and comments are very welcome.

Best,
--
Enrico Tassi