Re: Building clean packages for coq theories

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

Hi,

Le lundi 22 novembre 2021 à 09:01 +0100, Ralf Treinen a écrit :
> 
> 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.


If nobody already has its hands in the cogs (pun intended) already, I
can give it a try. I think I would start by packaging it as it is now
so coq+ssreflect can migrate to testing.

And only then I'll break coq and ssreflect in different packages. In
fact, for ssreflect I'm wondering if changing the source package name
wouldn't be sensible, if that's possible...

But first, I'd like to know where I'm heading to. I have to admit the
OCaml Packaging Policy isn't clear for me -- especially since it's
mostly about OCaml-but-not-coq!

Say a foobar package provides an executable, an ocaml lib and/or a coq
theories lib, with documentation. Of course the source package will be
foobar, but for the binaries:

- libfoobar-ocaml (ocaml runtime library, *.cma, *.cmxs)

- libfoobar-ocaml-dev (ocaml devel library, *.a, *.cmi, *.cmo, *.cmt,
*.cmx, *.cmxa, *.ml, *.mli, *.o, META, dune-package, opam)

- libfoobar-ocaml-doc (doc for the library, *html)

- foobar (executable, /usr/bin/foobar and associated manual)

- libfoobar-coq (coq theory, *.v, *.vo, *.vos, *.glob)

- libfoobar-coq-doc (coq theory doc, *html)

does that look right?

Cheers,

J.Puydt