hoqide on OS X

Yiming Xu

unread,

Mar 27, 2019, 11:28:53 PM3/27/19

to HoTT Cafe

Has anyone successfully used hoqide on OS X? We've been trying for a while to set it up. The instructions at https://github.com/HoTT/HoTT/blob/master/INSTALL.md seem to be missing many steps.

We seem to be stuck at our inability to install lablgtk. Does anyone have an idea what to do with the following error message?

$ opam install lablgtk

The following actions will be performed:

∗ install lablgtk 2.18.7

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫

[lablgtk.2.18.7] found in cache

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫

[ERROR] The compilation of lablgtk failed at

"/Users/yimingxu/.opam/opam-init/hooks/sandbox.sh build ./configure

--prefix /Users/yimingxu/.opam/default

LABLGLDIR=/Users/yimingxu/.opam/default/lib/lablgl".

#=== ERROR while compiling lablgtk.2.18.7 =====================================#

# context 2.0.3 | macos/x86_64 | ocaml-base-compiler.4.07.1 | https://opam.ocaml.org#fe723de2

# path ~/.opam/default/.opam-switch/build/lablgtk.2.18.7

# command ~/.opam/opam-init/hooks/sandbox.sh build ./configure --prefix /Users/yimingxu/.opam/default LABLGLDIR=/Users/yimingxu/.opam/default/lib/lablgl

# exit-code 1

# env-file ~/.opam/log/lablgtk-35119-d8a4ae.env

# output-file ~/.opam/log/lablgtk-35119-d8a4ae.out

### output ###

# [...]

# checking for suffix of object files... o

# checking whether we are using the GNU C compiler... yes

# checking whether cc accepts -g... yes

# checking for cc option to accept ISO C89... none needed

# checking whether C compiler accepts -fno-unwind-tables... yes

# checking platform... Unix

# checking native dynlink... checking for pkg-config... /usr/local/bin/pkg-config

# checking for GTK+ - version >= 2.0.0... no

# *** Could not run GTK+ test program, checking why...

# *** The test program failed to compile or link. See the file config.log for the

# *** exact error that occured. This usually means GTK+ is incorrectly installed.

# configure: error: GTK+ is required

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫

┌─ The following actions failed

│ λ build lablgtk 2.18.7

└─

╶─ No changes have been performed

<><> lablgtk.2.18.7 troubleshooting <><><><><><><><><><><><><><><><><><><><> 🐫

=> This package requires gtk+ 2.0 development packages installed on your system

=> To solve pkg-config issues, you may need to do

'export PKG_CONFIG_PATH=/opt/X11/lib/pkgconfig' and retry

The packages you requested declare the following system dependencies. Please

make sure they are installed before retrying:

expat gtk

Hendrik Boom

unread,

Mar 28, 2019, 6:20:35 PM3/28/19

to HoTT Cafe

On Wed, Mar 27, 2019 at 08:28:53PM -0700, Yiming Xu wrote:
>
> <><> *Error report*
> <><><><><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
>
> ┌─ The following actions failed
>
> │ λ build *lablgtk* 2.18.7

>
> └─
>
> ╶─ No changes have been performed
>

>

> <><> *lablgtk.2.18.7 troubleshooting*
> <><><><><><><><><><><><><><><><><><><><> 🐫

>
> => This package requires gtk+ 2.0 development packages installed on your
> system
>

Are there gtk+ 2.0 development packages installed on your system?
lablgtk is a binding to a native version of gtk.
And installation wants the development packages instead of merely the
use-libraries. On Debian those would be packages whose names end in -dev.
I don't know what the analogu is on ios.

-- hendrik

Scott Morrison

unread,

Mar 28, 2019, 11:44:28 PM3/28/19

to HoTT Cafe

I've been trying this as well (... the HoTT installation instructions could do with some work ...) and am failing at the same point, with the error message Yiming reported above.

We've been installing dependencies using 'homebrew'. Here's what I get when I ask what's installed from gtk:

$ brew search gtk

==> Formulae

clutter-gtk gtk-doc gtk-murrine-engine gtkglext gtksourceview3 gtkspell3 pygtksourceview

gtk+ ✔ gtk-engines gtk-vnc gtkmm gtksourceview4 lablgtk ✔ qalculate-gtk

gtk+3 ✔ gtk-gnutella gtkdatabox gtkmm3 gtksourceviewmm pygtk ✔

gtk-chtheme gtk-mac-integration ✔ gtkextra ✔ gtksourceview ✔ gtksourceviewmm3 pygtkglext

==> Casks

gtkwave

I don't see anything that's specifically a dev version. Is there some way to work out which gtk library opam is trying to using? Perhaps it is using the built-in macOS gtk library, rather than the homebrew one?

best regards,

Scott

Andrej Bauer

unread,

Mar 30, 2019, 2:56:38 PM3/30/19

to HoTT Cafe

I tried to install hoqide on OSX several times (after all I created the whole hoq thing) and I always failed to install lablgtk. I may give it another try, but if there's someone else who is adept at convincing OSX that it is Linux, I would appreciate some hints.

With kind regards,

Andrej

Daniel R. Grayson

unread,

Mar 30, 2019, 3:23:20 PM3/30/19

to HoTT Cafe

I had no problem a few months ago:

gallium$ type lablgtk2

lablgtk2 is /usr/local/bin/lablgtk2

gallium$ ls -l /usr/local/bin/lablgtk2

lrwxrwxr-x 1 brew admin 39 Jan 10 15:31 /usr/local/bin/lablgtk2 -> ../Cellar/lablgtk/2.18.6_3/bin/lablgtk2

Try "brew install lablgtk".

Scott Morrison

unread,

Mar 31, 2019, 1:19:43 AM3/31/19

to HoTT Cafe

Ok, I've now tried again on another mac, and after adding a few missing steps (opam init and opam install ocamlfind num) to the build instructions https://github.com/HoTT/HoTT/pull/1019, it does seem that etc/install_coq.sh can find lablgtk:

$ git submodule sync
Synchronizing submodule url for 'coq-HoTT'
Synchronizing submodule url for 'etc/coq-dpdgraph'
Synchronizing submodule url for 'etc/coq-scripts'
$ git submodule update --init --recursive
~/scratch/HoTT/coq-HoTT ~/scratch/HoTT ~/scratch/HoTT/etc ~/scratch/HoTT
$ ./configure -local
You have OCaml 4.07.1. Good!
You have OCamlfind 1.8.0. Good!
You have native-code compilation. Good!
You have the Num library installed. Good!
Warning: Could not check the version of lablgtk2.
Make sure your version is at least 2.18.3.
LablGtk2 found (in OCaml library, an unknown version), with native threads:
=> native CoqIde will be built.

I'm really not sure what Yiming and I were doing differently before. Certainly we had both successfully installed lablgtk via brew (see my message above), but etc/install_coq.sh was still claiming it couldn't find it, so we had next tried installing lablgtk via opam, which had failed (see Yiming's first message).

However a bit later in the installation, things still fail, with

...
OCAMLOPT -o bin/coqide
ocamlfind: Package `lablgtk2.sourceview2' not found
make[1]: *** [bin/coqide] Error 2
make: *** [submake] Error 2

I've tried "brew install gtksourceview", but this doesn't help. The available gtk related casks on brew are

$ brew search gtk
==> Formulae

clutter-gtk gtk-gnutella gtkglext gtksourceviewmm pygtksourceview
gtk+ ✔ gtk-mac-integration ✔ gtkmm gtksourceviewmm3 qalculate-gtk
gtk+3 ✔ gtk-murrine-engine gtkmm3 gtkspell3
gtk-chtheme gtk-vnc gtksourceview ✔ lablgtk ✔
gtk-doc gtkdatabox gtksourceview3 pygtk ✔
gtk-engines gtkextra gtksourceview4 pygtkglext

==> Casks
gtkwave

Since it is ocamlfind complaining here, I decided to try install some things via opam, rather than via brew. However opam install conf-gtksourceview fails with

The packages you requested declare the following system dependencies. Please make sure they are installed before retrying:

pkg-config

but after "brew install pkgconfig" it fails with two apparently independent error messages:

#=== ERROR while compiling conf-gtksourceview.2 ===============================#
# context 2.0.3 | macos/x86_64 | ocaml-system.4.07.1 | https://opam.ocaml.org#1a9d5b0d
# path ~/.opam/default/.opam-switch/build/conf-gtksourceview.2
# command ~/.opam/opam-init/hooks/sandbox.sh build pkg-config --short-errors --print-errors gtksourceview-2.0
# exit-code 1
# env-file ~/.opam/log/conf-gtksourceview-52952-dd682e.env
# output-file ~/.opam/log/conf-gtksourceview-52952-dd682e.out
### output ###
# Package 'libffi', required by 'gobject-2.0', not found

and

The packages you requested declare the following system dependencies. Please make sure they are installed before retrying:

gtksourceview libxml2

At this point brew reports that all of libffi, libxml2, and gtksourceview are installed. What's going on? Uninstalling and reinstalling those, we get a helpful message from brew:

libffi is keg-only, which means it was not symlinked into /usr/local,
because some formulae require a newer version of libffi.

For compilers to find libffi you may need to set:
export LDFLAGS="-L/usr/local/opt/libffi/lib"

For pkg-config to find libffi you may need to set:

export PKG_CONFIG_PATH="/usr/local/opt/libffi/lib/pkgconfig"

(and a similar message about libxml2). So we now try

export PKG_CONFIG_PATH="/usr/local/opt/libffi/lib/pkgconfig:/usr/local/opt/libxml2/lib/pkgconfig:/usr/local/opt/gtksourceview/lib/pkgconfig"
opam install conf-gtksourceview lablgtk

and it succeeds! Re-running etc/install_coq.sh we get a little further... on to our next error:

...

OCAMLOPT ide/preferences.ml
File "ide/preferences.ml", line 1:
Error: The files /Users/scott/.opam/default/lib/lablgtk2/gSourceView2.cmi
and ide/tags.cmi make inconsistent assumptions over interface GText
make[1]: *** [ide/preferences.cmx] Error 2
make: *** [submake] Error 2

Any suggestions for this?

best regards,

Scott

Scott Morrison

unread,

Mar 31, 2019, 2:42:40 AM3/31/19

to HoTT Cafe

Deleting the HoTT directory and starting again seems to ... require "brew install autoconf automake", and then work!

I will try this with Yiming sometime, and hopefully make a PR to install.md, adding these many missing steps.

best,
Scott

Yiming Xu

unread,

Mar 31, 2019, 5:39:20 PM3/31/19

to HoTT Cafe

Hi, everyone.

I have checked that Scott's instruction works! The instruction is now on : https://github.com/HoTT/HoTT/blob/e965427f7f8b6b66c6273bb64e8c0da3ac9bdc70/INSTALL.md

Reply all

Reply to author

Forward