Building clean packages for coq theories

[Julien Puydt <julien.puydt@gmail.com>]

Hi,

I updated src:coq, I uploaded src:elpi (to NEW).

I'm trying to create a nice package for coq-elpi, but I'm not sure
exactly how to do that.

The examples I have are coq's standard library and ssreflect. And
neither looks clean.

By this I mean that for coq, there's coq-theories, and it ships .v .vo
files and the html doc. Those represent 56% of the package according to
lintian, and it's asking why a arch-dep package is so largely arch-
indep.

And for ssreflect, it ships a single libssreflect-coq package ; it's
shipping .v, .vo and .glob files and the html doc. It's arch-indep.
[aside: it needs updating to latest upstream.]

In both cases, the package name doesn't seem to follow a convention,
and the package name bears little link to upstream's packaging names
(stdlib for coq, mathcomp for ssreflect).

For coq-elpi, there's a main coq plugin (.v, .vo ok, but also .cma,
.cmi, .cmo, .cmx, .cmxa, .cmxs in /usr/lib/coq/user-contrib/) and there
are child plugins (.v and .vo).

If no convention exists, I would like to see if we could work on one.

Cheers,

J.Puydt