Hi,
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