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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

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.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Le mardi 23 novembre 2021 à 10:09 +0100, Stéphane Glondu a écrit :

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).

Indeed, that's what's the policy says.

I made the mistake with coq (I pushed a fixing commit), but since I
based my elpi & ocaml-ansi-terminal on studying other packages, those
are ok.

I won't upload coq again that soon though (unless I get a fix for
bytecode-only architectures!), as I'd like to rework the packaging
quite extensively.

Cheers,

J.Puydt

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Le 24/11/2021 à 14:57, Julien Puydt a écrit :

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).

Indeed, that's what's the policy says.

I made the mistake with coq (I pushed a fixing commit), but since I
based my elpi & ocaml-ansi-terminal on studying other packages, those
are ok.

I won't upload coq again that soon though (unless I get a fix for bytecode-only architectures!), as I'd like to rework the packaging
quite extensively.

Do you intend to let the current state to migrate to testing?

If so, the binaries (of coq and its reverse dependencies, including why3
and frama-c) on bytecode architectures should be removed from unstable.

If not, many packages (everything related to ocaml-zarith) will be
blocked in their migration to testing. I think this should be avoided.


Cheers,

--
Stéphane

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)