Re: Lintian warnings with the coq package
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.
Reply to: