Hi,
Le jeu. 11 nov. 2021 à 19:41, Ralf Treinen <
treinen@fdn.fr> a écrit :
thanks for the work on the coq package. First of all a general
comment: in the ocaml team we usually use different branches for packaging work that is intended to go to experimental (branches experimental/master
and experimental/upstream), but I don't think it is a drama when you
commit to master.
Oh.
Is there a reason why you are not using the dune build system? I am
myself not a big fan of the monolithic dune system but that is the
primary build system that the upstream developers have decided for.
This might also solve the build failures on bytecode-only architectures. (export COQ_USE_DUNE=1 in debian/rules)
I thought upstream was still considering the Makefile system as the
default.
I tried to build (from commit a322bfa8547a1f88a3cadc8e543be0b495c00e8b)
but it fails with:
(cd _build/default && /bin/bash -e -u -o pipefail -c dev/tools/make_git_revision.sh) > _build/default/revision
/bin/bash: dev/tools/make_git_revision.sh: /usr/bin/bash: bad interpreter:
No such file or directory
I have on my system /bin/bash, not /usr/bin/bash. Anyway, either bash
should be replaced by /bin/sh, or we need a build-dependency on bash.
I saw the build was broken on a few architectures but didn't investigate
yet ; indeed I'll try get rid of that use of bash.
On Wed, Nov 10, 2021 at 11:40:37AM +0100, Julien Puydt wrote:
PROBLEM I: shared-library-lacks-prerequisites lintian warnings
I have also many of these on my packages, no idea what can be done
about these.
I know what can be done about these: report to lintian devs and discuss
with them how to do better. I'll do it - I've already had problems with
lintian and they were very receptive.
PROBLEM II: ocaml-dangling-cmi lintian warnings
(many of them)
No idea, and sicne the build fails for me I cannot reproduce.
I'll fix that problem. I think I have the same with elpi, which is much
faster to compile.
PROBLEM III: unstripped-static-library lintian warnings
No idea, either (sorry that I am not very helpful)
Same as above, I would say: lintian devs might want to know about it, and
I'll get in touch.
PROBLEM IV: coq's lib is not in /usr/lib/ocaml
That was the case with the previous packaging (/usr/lib/coq)), it's
still the case (/usr/lib/coq-core), and it's incoherent with the
policy:
libcoq-ocaml-dev: ocaml-dev-file-not-in-usr-lib-ocaml 998 files in
usr/lib
Isn't there a configuration option to chose the location of the the coq library? Or maybe it is the COQLIB environment variable that has to
be set accordingly?
Well, it turns out that my work on a coq-elpi (after an initial false
start) proves that it's not a problem after all, so that one is solved.
Summary:
- problems I and III are probably for lintian devs to solve with some help ;
- problem II is still a question ;
- problem IV is solved.
I'll fix the use of bash and start trying to build packages depending on
coq to see if uploading will break anything, then proceed to an upload to unstable - probably monday.
Cheers,
J. Puydt
<div dir="auto"><div>Hi, <br><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Le jeu. 11 nov. 2021 à 19:41, Ralf Treinen <<a href="mailto:
treinen@fdn.fr">
treinen@fdn.fr</a>> a écrit :</div><blockquote class="gmail_quote" style="
margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
thanks for the work on the coq package. First of all a general<br>
comment: in the ocaml team we usually use different branches for packaging<br> work that is intended to go to experimental (branches experimental/master<br> and experimental/upstream), but I don't think it is a drama when you<br> commit to master.<br></blockquote></div></div><div dir="auto"><br></div><div dir="auto">Oh.</div><div dir="auto"><br></div><div dir="auto"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;
padding-left:1ex">
Is there a reason why you are not using the dune build system? I am<br>
myself not a big fan of the monolithic dune system but that is the<br>
primary build system that the upstream developers have decided for.<br>
This might also solve the build failures on bytecode-only architectures.<br> (export COQ_USE_DUNE=1 in debian/rules)<br></blockquote></div></div><div dir="auto"><br></div><div dir="auto">I thought upstream was still considering the Makefile system as the default. </div><div dir="auto"><br></div><div dir="auto"><div class="gmail_
quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
I tried to build (from commit a322bfa8547a1f88a3cadc8e543be0b495c00e8b)<br>
but it fails with:<br>
(cd _build/default && /bin/bash -e -u -o pipefail -c dev/tools/make_git_revision.sh) > _build/default/revision<br>
/bin/bash: dev/tools/make_git_revision.sh: /usr/bin/bash: bad interpreter: No such file or directory<br>
I have on my system /bin/bash, not /usr/bin/bash. Anyway, either bash<br> should be replaced by /bin/sh, or we need a build-dependency on bash.<br></blockquote></div></div><div dir="auto"><br></div><div dir="auto">I saw the build was broken on a few architectures but didn't investigate yet ; indeed I'll try get rid of
that use of bash.<br></div><div dir="auto"><br></div><div dir="auto"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
On Wed, Nov 10, 2021 at 11:40:37AM +0100, Julien Puydt wrote:<br>
> PROBLEM I: shared-library-lacks-prerequisites lintian warnings<br>
I have also many of these on my packages, no idea what can be done<br>
about these.<br></blockquote></div></div><div dir="auto"><br></div><div dir="auto">I know what can be done about these: report to lintian devs and discuss with them how to do better. I'll do it - I've already had problems with lintian and they
were very receptive. </div><div dir="auto"><br></div><div dir="auto"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
> PROBLEM II: ocaml-dangling-cmi lintian warnings<br>
> (many of them)<br>
No idea, and sicne the build fails for me I cannot reproduce.<br></blockquote></div></div><div dir="auto"><br></div><div dir="auto">I'll fix that problem. I think I have the same with elpi, which is much faster to compile. </div><div dir="auto"><br><
/div><div dir="auto"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
> PROBLEM III: unstripped-static-library lintian warnings<br>
No idea, either (sorry that I am not very helpful)<br></blockquote></div></div><div dir="auto"><br></div><div dir="auto">Same as above, I would say: lintian devs might want to know about it, and I'll get in touch. </div><div dir="auto"><br></div><
div dir="auto"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
> PROBLEM IV: coq's lib is not in /usr/lib/ocaml<br>
> <br>
> That was the case with the previous packaging (/usr/lib/coq)), it's<br>
> still the case (/usr/lib/coq-core), and it's incoherent with the<br> > policy:<br>
> libcoq-ocaml-dev: ocaml-dev-file-not-in-usr-lib-ocaml 998 files in<br> > usr/lib<br>
Isn't there a configuration option to chose the location of the the coq<br> library? Or maybe it is the COQLIB environment variable that has to<br>
be set accordingly?<br></blockquote></div></div><div dir="auto"><br></div><div dir="auto">Well, it turns out that my work on a coq-elpi (after an initial false start) proves that it's not a problem after all, so that one is solved.</div><div dir="
auto"><br></div><div dir="auto">Summary:</div><div dir="auto">- problems I and III are probably for lintian devs to solve with some help ;</div><div dir="auto">- problem II is still a question ;</div><div dir="auto">- problem IV is solved.</div><div dir="
auto"><br></div><div dir="auto">I'll fix the use of bash and start trying to build packages depending on coq to see if uploading will break anything, then proceed to an upload to unstable - probably monday.</div><div dir="auto"><br></div><div dir="
auto">Cheers,</div><div dir="auto"><br></div><div dir="auto">J. Puydt</div><div dir="auto"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
</blockquote></div></div></div>
--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)