Re: Packaging elpi, hierarchy-builder and recent a mathcomp -- starting to work on it
Hi,
Le jeudi 28 octobre 2021 à 09:24 +0200, Stéphane Glondu a écrit :
>
> Le 27/10/2021 à 18:40, Julien Puydt a écrit :
> > as I wrote to this list in august, I'm interested in coq theories,
> > and
> > specifically mathcomp, which will soon require hierarchy-builder,
> > wich
> > requires coq-elpi, which requires elpi.
> >
> > I am a Debian developer and I am already part of a few teams (games,
> > javascript, python and science), so I should have the general
> > practice
> > of managing packages right, but I really lack experience about OCaml
> > packaging, so I will need some help before I'm efficient.
> >
> > I have tried to package elpi already, and made the result available
> > here: https://mentors.debian.net/package/elpi/
> >
> > Notice:
> > (1) no ITP yet ;
> > (2) already pointing to the team's salsa ;
>
> Feel free to push your git repository there.
>
I just made an access request.
> > (3) packaging inspired by those of ppxlib and ssreflect ;
> > (4) lintian finds so many things to complain about!
>
> There are many that are present in many OCaml packages... but, why did
> you mark libelpi-ocaml-dev as arch:all? This is an obvious error which,
> when fixed, would remove many Lintian errors.
>
Oh, dear... a stupid typo.
> > Comments and corrections are very welcome,
>
> This is more a comment on upstream, but I cannot not say it: using
> camlp5 and ppxlib at the same time seems very strange to me.
>
I improved my package, making it two binaries (with the exec in a
package with its manpage).
There are still three last lintian complaints:
W: libelpi-ocaml-dev: shared-library-lacks-prerequisites
usr/lib/ocaml/elpi/elpi.cmxs
W: libelpi-ocaml-dev: shared-library-lacks-prerequisites
usr/lib/ocaml/elpi/trace/ppx/trace_ppx.cmxs
W: libelpi-ocaml-dev: shared-library-lacks-prerequisites
usr/lib/ocaml/elpi/trace/runtime/trace_ppx_runtime.cmxs
but with --pedantic, it's still awfully verbose.
Cheers,
J.Puydt
Reply to: