Robbert Krebbers (Sep 28 2020 at 14:23): Robbert Krebbers (Sep 28 2020 at 14:23):I'mm trying to install Coq + CoqIDE master on Debian testing, but it complains that I have not installed the correct version of LablGtk3 and LablGtkSourceView3. However, according to my package manager (apt), I have.
robbert@robbert:~/coq/coq$ apt search lablgtk sourceview3
Sorting... Done
Full Text Search... Done
liblablgtksourceview3-ocaml/testing,unstable,now 3.1.1-1+b1 amd64 [installed]
OCaml bindings for libgtksourceview3 (runtime)
liblablgtksourceview3-ocaml-dev/testing,unstable,now 3.1.1-1+b1 amd64 [installed]
OCaml bindings for libgtksourceview3 (development files)
robbert@robbert:~/coq/coq$ apt search lablgtk3
Sorting... Done
Full Text Search... Done
liblablgtk3-ocaml/testing,unstable,now 3.1.1-1+b1 amd64 [installed]
OCaml bindings to Gtk+ version 3 (runtime)
liblablgtk3-ocaml-dev/testing,unstable,now 3.1.1-1+b1 amd64 [installed]
OCaml bindings to Gtk+ version 3 (development files)
liblablgtk3-ocaml-doc/testing,unstable,now 3.1.1-1 all [installed,automatic]
OCaml bindings to Gtk+ version 3 (documentation)
robbert@robbert:~/coq/coq$ ./configure -local
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]):
=> no CoqIde will be built.
Architecture : Linux
Sys.os_type : Unix
Coq VM bytecode link flags : -dllib -lcoqrun -dllpath "/home/robbert/coq/coq/kernel/byterun"
Other bytecode link flags :
OCaml version : 4.08.1
OCaml binaries in : /usr/bin/
OCaml library in : /usr/lib/ocaml
OCaml flambda flags :
Native dynamic link support : true
CoqIde : no
Documentation : None
Web browser : firefox -remote "OpenURL(%s,new-tab)" || firefox %s &
Coq web site : http://coq.inria.fr/
Bytecode VM enabled : true
Native Compiler enabled : true
Local build, no installation...
If anything is wrong above, please restart './configure'.
*Warning* To compile the system for a new architecture
don't forget to do a 'make clean' before './configure'.
Anyone an idea what's going on here? I am happy to provide more information if that's needed.
Enrico Tassi (Sep 28 2020 at 14:26):Today I had to do opam upgrade lablgtk3-sourceview3
Enrico Tassi (Sep 28 2020 at 14:26):The ocaml bindings are too old, not the C library
Robbert Krebbers (Sep 28 2020 at 14:30):Note that I'm not using opam, just the Debian package manager.
Karl Palmskog (Sep 28 2020 at 14:40):maybe the Debian OCaml bindings for Lablgtk3 are out of date with what Coq assumes? I'd try with the opam approach and see if it suddenly works.
Robbert Krebbers (Sep 28 2020 at 14:43):But this seems like a bug in the ./configure script, no? Debian reports 3.1.1 is installed, and that's >= 3.1.0.
Karl Palmskog (Sep 28 2020 at 14:44):it may be that Debian has a bug in not installing the OCaml bindings in a way expected by OCaml (ocamlfind, etc.)?
Enrico Tassi (Sep 28 2020 at 14:49):Right, the bug is here: https://github.com/coq/coq/pull/13049
The changelog says >= 3.1.0 but the code I comment here https://github.com/coq/coq/pull/13049/files#r495997541 is using <
Enrico Tassi (Sep 28 2020 at 14:50):Would yo mind opening an issue? (I'm busy right now)
Enrico Tassi (Sep 28 2020 at 14:53):Nah, I guess I was wrong but the bug may still be in that piece of code, which fails to "parse" the version of the debian package
Robbert Krebbers (Sep 28 2020 at 15:01):Thanks @Enrico Tassi . The problem appears to be with the output of ocamlfind, which gives:
robbert@robbert:~/coq/coq$ ocamlfind query -format %v lablgtk3
[unspecified]
For other packages, e.g., zarith, it gives a sensible output. Any idea where I should report this bug? Is it a Debian bug or an Ocamlfind bug?
Robbert Krebbers (Sep 28 2020 at 15:08):I currently just hacked around this problem by commenting out the check in configure.ml. Both Coq and CoqIDE appear to compile fine.
Enrico Tassi (Sep 28 2020 at 15:17):ocamlfind query lablgtk3 should print a path. In there you should find a META file, it's text, check what version= is in there
Enrico Tassi (Sep 28 2020 at 15:36):I've downloaded the package (from sid) and the META file does not contain the version = "..." line, so there is it
Emilio Jesús Gallego Arias (Sep 28 2020 at 15:44):Sorry @Robbert Krebbers , this is a known issue with Debian packages which are indeed buggy; there is no easy way for Coq's configure script to check versions other than relying on findlib, we will add a --no-version-check parameter to configure for convenience.
Emilio Jesús Gallego Arias (Sep 28 2020 at 15:45):For convenience and to workaround pitfalls in the version detection code.
Enrico Tassi (Sep 28 2020 at 15:46):hacking the META file by adding a version = "3.1.1" line may be the quickest fix for you.
Robbert Krebbers (Sep 28 2020 at 16:30):Thanks for the suggestions.
Arghh @Debian, they still expect one to report bugs via email or their reportbug utility... https://www.debian.org/Bugs/Reporting
Emilio Jesús Gallego Arias (Sep 28 2020 at 16:38):Yup, you gotta send the bot a mail IIANM.
Théo Zimmermann (Sep 29 2020 at 09:27):FTR there is already an issue opened on the Coq bug tracker discussing the same issue. It might be worth checking since the author might have already reported the problem to Debian.
Oliver (Sep 30 2020 at 02:00):You could try installing with aptitude it's smarter than apt.
Oliver (Sep 30 2020 at 02:01):It can be helpful to have around anyway for --full-resolver
Robbert Krebbers (Oct 01 2020 at 06:49):Thanks @Emilio Jesús Gallego Arias for reporting at Debian!
Robbert Krebbers (Oct 01 2020 at 06:50):You could try installing with aptitude it's smarter than apt.
I don't think that's relevant here. The problem is not that apt fails to install something, but that there's a bug in a package.
Emilio Jesús Gallego Arias (Oct 01 2020 at 14:01):NP @Robbert Krebbers
Oliver (Oct 02 2020 at 16:57):Robbert Krebbers said:
You could try installing with aptitude it's smarter than apt.
I don't think that's relevant here. The problem is not that apt fails to install something, but that there's a bug in a package.
Which is a surprise to me since I just installed the other day on testing without issue.
Last updated: Apr 19 2024 at 13:02 UTC