Stream: Coq users

Topic: Install Coq master on Debian testing


view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Sep 28 2020 at 14:26):

Today I had to do opam upgrade lablgtk3-sourceview3

view this post on Zulip Enrico Tassi (Sep 28 2020 at 14:26):

The ocaml bindings are too old, not the C library

view this post on Zulip Robbert Krebbers (Sep 28 2020 at 14:30):

Note that I'm not using opam, just the Debian package manager.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)?

view this post on Zulip 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 <

view this post on Zulip Enrico Tassi (Sep 28 2020 at 14:50):

Would yo mind opening an issue? (I'm busy right now)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 28 2020 at 15:45):

For convenience and to workaround pitfalls in the version detection code.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 28 2020 at 16:38):

Yup, you gotta send the bot a mail IIANM.

view this post on Zulip 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.

view this post on Zulip Oliver (Sep 30 2020 at 02:00):

You could try installing with aptitude it's smarter than apt.

view this post on Zulip Oliver (Sep 30 2020 at 02:01):

It can be helpful to have around anyway for --full-resolver

view this post on Zulip Robbert Krebbers (Oct 01 2020 at 06:49):

Thanks @Emilio Jesús Gallego Arias for reporting at Debian!

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 01 2020 at 14:01):

NP @Robbert Krebbers

view this post on Zulip 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: Jan 28 2023 at 07:30 UTC