./configure incorrectly detects LablGtk3 and LablGtkSourceView3 version 3.1.1 as "[unspecified]" and refuses to build CoqIDE

[JasonGross]

Description of the problem

https://launchpadlibrarian.net/498745150/buildlog_ubuntu-groovy-amd64.coq_8.master~git~202009232210+21727-0~daily337-d7b2da080b~ubuntu20.10.1_BUILDING.txt.gz

Get:321 http://ftpmaster.internal/ubuntu groovy/universe amd64 libgtksourceview-3.0-dev amd64 3.24.11-2 [330 kB]
Get:322 http://ftpmaster.internal/ubuntu groovy/universe amd64 liblablgtk3-ocaml amd64 3.1.1-1build2 [2443 kB]
Get:323 http://ftpmaster.internal/ubuntu groovy/universe amd64 liblablgtk3-ocaml-dev amd64 3.1.1-1build2 [5840 kB]
Get:324 http://ftpmaster.internal/ubuntu groovy/universe amd64 liblablgtksourceview3-ocaml amd64 3.1.1-1build2 [233 kB]
Get:325 http://ftpmaster.internal/ubuntu groovy/universe amd64 liblablgtksourceview3-ocaml-dev amd64 3.1.1-1build2 [489 kB]
[...]
Selecting previously unselected package liblablgtk3-ocaml.
Preparing to unpack .../310-liblablgtk3-ocaml_3.1.1-1build2_amd64.deb ...
Unpacking liblablgtk3-ocaml (3.1.1-1build2) ...
Selecting previously unselected package liblablgtk3-ocaml-dev.
Preparing to unpack .../311-liblablgtk3-ocaml-dev_3.1.1-1build2_amd64.deb ...
Unpacking liblablgtk3-ocaml-dev (3.1.1-1build2) ...
Selecting previously unselected package liblablgtksourceview3-ocaml.
Preparing to unpack .../312-liblablgtksourceview3-ocaml_3.1.1-1build2_amd64.deb ...
Unpacking liblablgtksourceview3-ocaml (3.1.1-1build2) ...
Selecting previously unselected package liblablgtksourceview3-ocaml-dev.
Preparing to unpack .../313-liblablgtksourceview3-ocaml-dev_3.1.1-1build2_amd64.deb ...
Unpacking liblablgtksourceview3-ocaml-dev (3.1.1-1build2) ...
[...]
Setting up humanity-icon-theme (0.6.15) ...
Setting up liblablgtk3-ocaml (3.1.1-1build2) ...
Setting up gir1.2-gtksource-3.0:amd64 (3.24.11-2) ...
Setting up libgtk-3-dev:amd64 (3.24.23-1ubuntu1) ...
Setting up liblablgtksourceview3-ocaml (3.1.1-1build2) ...
Setting up liblablgtk3-ocaml-dev (3.1.1-1build2) ...
Setting up libgtksourceview-3.0-dev:amd64 (3.24.11-2) ...
Setting up ubuntu-mono (20.10-0ubuntu1) ...
Setting up liblablgtksourceview3-ocaml-dev (3.1.1-1build2) ...
[...]
./configure -arch Linux -prefix /usr -mandir /usr/share/man -configdir /etc/xdg/coq -browser "/usr/bin/x-www-browser %s &" -with-doc no -vmbyteflags "-dllib,-lcoqrun"
You have OCaml 4.08.1. Good!
You have OCamlfind 1.8.1. Good!
You have native-code compilation. Good!
You have the Zarith library 1.10 installed. Good!
LablGtk3 and LablGtkSourceView3 found ([unspecified]), but too old (required >= 3.1.0, found [unspecified]):

Coq Version

master (d7b2da0)

[Zimmi48]

That's likely to be a bug in your packaging of lablgtk3 3.1.1. OCaml packages released with dune-release provide a .tbz archive (https://github.com/garrigue/lablgtk/releases/download/3.1.1/lablgtk3-3.1.1.tbz) that should be used as source. In nixpkgs, it is a common issue that people used the auto-generated GitHub source archive instead and the consequence is usually that the version is unknown.

[JasonGross]

I guess someone should report this as a bug in the package (I'm using the official Ubuntu package, not packaging this myself)

[ejgallego]

What does ocamlfind query -format "%v" lablgtk3 return? Indeed Coq uses this value, so if it returned unspecified looks like a bug in the packaging.

There is a planned configure revamp that will include an "ignore deps" flags so people can avoid these problems, meanwhile we are out of luck barring a similar patch.

[JasonGross]

Reported at https://bugs.launchpad.net/ubuntu/+source/lablgtk3/+bug/1897171

[silene]

Honestly, Debian maintainers could rightly complain that a distributed file (dune-project, I guess) has been tampered with, since it is different from the versioned file at the corresponding tag. If file dune-project is meant to be generated on the fly by dune-release, then having it in the lablgtk3 repository is bound to cause some misunderstanding.

[Zimmi48]

The dune-project file is also meant to be in the repository because you need it to build the development version of the project. Why should Debian maintainers have to care about the version controlled file? It's an oversight not to use the proper archive distributed by the maintainers.

[silene]

Why should Debian maintainers have to care about the version controlled file?

They do not need to. But as I said, you cannot expect them to guess that the file that is shipped in the tarball is different from the one in the repository.

Here is a bit more context. For various reasons (security, accountability, auditing, and so on), Debian maintains a git mirror of all the packages. Except for the debian/ subdirectory in the packages, this is a pristine copy of the upstream repository. They have no problem working with projects that have no upstream repository; they just create one from scratch then. But, when there exists one, they have a priori no reason not to use it, unless they are told that it is not authoritative.

Anyway, once they try to ship Coq 8.13, they will notice the issue. And at that point they will either patch Lablgtk or Coq to fix it.

[Zimmi48]

I would hope that they fix their packaging of lablgtk given how general this issue is in the OCaml ecosystem nowadays (as I've said before, I faced it more than once with OCaml packages in nixpkgs).

[ejgallego]

Again this is a bug on Debian packaging, if you are building from git you gotta call dune subst , then use -p, see for example most opam files that do this step correctly, for example in lablgtk3 current git head:

$ dune subst && dune build -p lablgtk3 && dune exec -- ocamlfind query -format "%v" lablgtk3
3.1.1-1-g034d4fbb

That being said current configure version parsing should be better as to detect this kind of versions.

[ejgallego]

Moved to https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=971439