On the coq ecosystem in Debian
Hi,
I'm trying to get more of the coq ecosystem into Debian. There are
several things I would like to package -- but first I think I need to
consolidate what's already there.
Here is a list of issues I have, on which I would need feedback ; I put
explicit "Question: ..." to make it clearer what is asked.
(1) Currently, each time coq is rebuilt (either because OCaml was
updated or it was updated itself), the whole stack should be too, or
things just break! (There are some bugs about it: #741535, #977258
[cloned as #979756]).
I expect the new uploads should trigger automatic transitions, much
like soname changes do for C/C++ libs. That makes things much easier.
I know "ben" (https://ben.debian.net/) helps following transitions
(here: https://release.debian.org/transitions/), I know
https://wiki.debian.org/Teams/ReleaseTeam/Transitions explains how
manual transitions work and mentions an auto-transitioner, but didn't
find where that thing is.
Question: how are such things done? (pointers to code and/or
documentation are welcome)
(2) I'm not sure the current source packages all give good binary
packages (here: content).
The src:coq package provides libcoq-stdlib which contains the coq
standard library and its doc. The binary libcoq-core-ocaml and libcoq-
core-ocaml-dev look honest OCaml packages, providing the correct files
in /usr/lib/ocaml/coq-core. Probably ok.
For src:coq-elpi, things don't look so good:
- libcoq-elpi-ocaml is mostly .v, .vo and .glob coq files in
/usr/lib/ocaml/coq/user-contrib/elpi, with only a pair of .cma/.cmxs in
/usr/lib/ocaml/coq/user-contrib/elpi, so it doesn't look sane.
- libcoq-elpi-ocaml-dev has .a, .cmi, .cmo, .cmx, .cmxa files so I
think it's good.
Question: shouldn't I split the current libcoq-elpi in a libcoq-elpi
for the purely coq part and a libcoq-elpi-ocaml packages for the
.cma/.cmxs pair?
The binary libcoq-mathcomp-* packages (coming from src:ssreflect,
src:mathcomp-bigenouh and src:mathcomp-finmap) have .v, .vo and .glob
files, so there is some coherence.
The src:aac-tactics package builds libaac-tactics-coq with .v, .vo and
.glob files and the documentation, libaac-tactics-ocaml with a
.cmo/.cmxs pair in /usr/lib/ocaml/coq and libaac-tactics-ocaml-dev
provides .cmi and .mli files in /usr/lib/ocaml/coq and documentation (I
think it's code documentation, so puting it in -dev makes sense).
libaac-tactics-coq and libaac-tactics-ocaml-dev depend on libaac-
tactic-ocaml, and libaac-tactics-coq recommends libaac-tactics-ocaml.
(3) I'm not sure the current source packages all give good binary
packages (here: names).
You'll have noticed above that the packages I made (either because I
started packaging them or I came along and split an existing one) have
a name starting with libcoq-foo. The various upstreams provide opam
packages, and the names are coq-foo, so I just followed upstream pretty
blindly here, and added a lib prefix because... well, that looked like
libs in some sense.
What I hadn't noticed was src:aac-tactics, where the coq part follows
the libfoo-coq convention. And well, if I look in my /usr/share/doc,
there's libcommons-logging-java, libsereal-decoder-perl, libsexplib-
ocaml... so it's pretty common to use libfoo-<lang> for package names.
But some quick "apt-cache search librust", "apt-cache search libghc",
"apt-cache search libjulia" shows other languages follow a prefix
convention. And with golang and erlang, they use <lang>-foo without any
lib prefix!
So basically, if upstream is named foo, the possible conventions could
be:
(1) libfoo-coq, libfoo-ocaml and libfoo-ocaml-dev
(2) libcoq-foo, libcoq-foo-ocaml and libcoq-foo-ocaml-dev
(3) coq-foo, libcoq-foo-ocaml and libcoq-foo-ocaml-dev
(4) coq-foo, libfoo-coq-ocaml and libfoo-coq-ocaml-dev
(5) coq-foo, libfoo-ocaml and libfoo-ocaml-dev
Notice that src:elpi and src:coq-elpi both exist ; the first is a
normal OCaml library and the second, mentioned above, is coq-based, so
the fifth proposition is probably out.
If you want to see more package names in the ecosystem, I have a
comparison page (output of a script I wrote) with the "Coq Platform"
which should help:
https://people.debian.org/~jpuydt/coq_platform.html
Question: Which convention should I follow?
Cheers,
J.Puydt
Reply to: