• Lintian warnings with the coq package

    From Julien Puydt@21:1/5 to All on Wed Nov 10 11:50:01 2021
    Hi,

    I'm still not satisfied with the coq package I prepared : lintian finds
    too much to complain about.



    PROBLEM I: shared-library-lacks-prerequisites lintian warnings
    (many of them)

    For example:
    W: libcoq-ocaml: shared-library-lacks-prerequisites usr/lib/coq- core/clib/clib.cmxs

    My libcoq-ocaml has /usr/lib/coq-core/clib/clib.cma and /usr/lib/coq- core/clib/clib.cmxs ; my libcoq-ocaml-dev has /usr/lib/coq-
    core/clib/clib.a and /usr/lib/coq-core/clib/clib.cmxa.

    I did things like this because the Debian Ocaml Packaging Policy says
    "If the library provides native plugins (*.cmxs) or is meant to be
    dynamically loaded using the Dynlink library, those plugins, relevant
    *.cmo or *.cma files, and the META file referencing them should also be provided by this runtime package.", so since there's no cmo file (which
    the previous package had), I moved the cma files in.


    Do I miss something? The fact that the error message is not OCaml-
    specific makes me wonder if lintian might just makes bogus claims.




    PROBLEM II: ocaml-dangling-cmi lintian warnings
    (many of them)

    For example:
    I: libcoq-ocaml-dev: ocaml-dangling-cmi usr/lib/coq- core/gramlib/gramlib__Gramext.cmi

    In fact, all of the cases giving me issues have the form foo__bar.cmi,
    so I suspect there's something special about them: for all other .cmi,
    I have corresponding files and no warning.

    Is there something specific with foo__bar.cmi files which lintian
    doesn't know about?



    PROBLEM III: unstripped-static-library lintian warnings
    (many of them)

    For example:
    I: libcoq-ocaml-dev: unstripped-static-library usr/lib/coq- core/gramlib/gramlib.a

    There I'm wondering if it's not detecting .a files, treating them like C-language .a files and hence complaining for nothing.





    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



    Of course, there are other issues, but the above ones bother me.

    Cheers,

    J.Puydt

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Ralf Treinen@21:1/5 to Julien Puydt on Thu Nov 11 19:50:01 2021
    Hello,

    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.

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

    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.

    PROBLEM II: ocaml-dangling-cmi lintian warnings
    (many of them)

    No idea, and sicne the build fails for me I cannot reproduce.

    PROBLEM III: unstripped-static-library lintian warnings

    No idea, either (sorry that I am not very helpful)

    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?

    Bon courage -Ralf.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Julien Puydt@21:1/5 to Julien Puydt on Thu Nov 11 22:00:01 2021
    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 &lt;<a href="mailto:treinen@fdn.fr">treinen@fdn.fr</a>&gt; 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&#39;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 &amp;&amp; /bin/bash -e -u -o pipefail -c dev/tools/make_git_revision.sh) &gt; _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&#39;t investigate yet ; indeed I&#39;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>

    &gt; 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&#39;ll do it - I&#39;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">
    &gt; PROBLEM II: ocaml-dangling-cmi lintian warnings<br>
    &gt; (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&#39;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">
    &gt; 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&#39;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">
    &gt; PROBLEM IV: coq&#39;s lib is not in /usr/lib/ocaml<br>
    &gt; <br>
    &gt; That was the case with the previous packaging (/usr/lib/coq)), it&#39;s<br>
    &gt; still the case (/usr/lib/coq-core), and it&#39;s incoherent with the<br> &gt; policy:<br>
    &gt; libcoq-ocaml-dev: ocaml-dev-file-not-in-usr-lib-ocaml 998 files in<br> &gt; usr/lib<br>

    Isn&#39;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&#39;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&#39;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)