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.