Hi,

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 ;
(3) packaging inspired by those of ppxlib and ssreflect ;
(4) lintian finds so many things to complain about!

Comments and corrections are very welcome,

J.Puydt

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

Hi,

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.

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

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.


Cheers,

--
Stéphane

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

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

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

Le jeudi 28 octobre 2021 à 09:24 +0200, Stéphane Glondu a écrit :

Feel free to push your git repository there.

Access request still pending.

I improved my elpi package, see
https://mentors.debian.net/packages/elpi/

I'm wondering why "ocamlfind list" shows its version as n/a.

The next package I would want to work on is coq-elpi, but it requires a
more recent coq (at least 8.14).

Cheers,

J.Puydt


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