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.
