Re: Building clean packages for coq theories
Hello,
On Fri, Nov 19, 2021 at 08:04:44AM +0100, Julien Puydt wrote:
> 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).
sslreflect should probably be repacked. For starters, the name
"sslreflect" is due to the fact that when the package was created it
also contained the sslreflect plugin, which is now part of the coq
upstream distribution. The name should be something containing
the words "coq" and "mathcomp".
Then, there should be several binary packages. I suggest following
the organisation of the opam packages since this is what users will
find in the mathcomp documentation, I guess. Splitting of architecture
independent packages would be plus.
-Ralf.
Reply to: