Re: Building clean packages for coq theories

[Stéphane Glondu <glondu@debian.org>]

Le 22/11/2021 à 09:39, Julien Puydt a écrit :
> 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?

META is usually put in libfoobar-ocaml, as it contains the information
to locate the *.cma and *.cmxs files (this information is used by
anything using findlib as a lib, for example ocsigenserver).

The rest looks right.

Feel free to update the OCaml packaging policy as you see fit.

Thank you for taking care of the question!


Cheers,

-- 
Stéphane