CoqIDE segmentation fault in 8.13.1

[elefthei]

Description of the problem

CoqIDE is crashing with a segfault for Mac users

Coq Version

coq 8.13.1

[Alizter]

What are the steps to reproduce?

[elefthei]

Here's the instructions for Mac, one of the students in our Coq workshop run into this

install homebrew via https://brew.sh/ (open a terminal and copy install line into the terminal)
brew install will give you two lines to run in the terminal that will set up your paths for later
open the terminal application and brew install opam
Initialize opam with these commands
opam init
eval $(opam env)

Webpage to use opam to install coq: https://coq.inria.fr/opam-using.html
opam install opam-depext
opam-depext coq
opam pin add coq 8.13.1
opam-depext coqide
opam install coqide
Should be able to start coqide at this point by typing coqide in the command line (terminal) with
coqide -debug.

[Zimmi48]

That's not likely to be enough to reproduce. Otherwise, we would have received reports of this crash before. I guess we would need at least the exact macOS version.

BTW, you might be interested in the Coq platform (https://github.com/coq/platform) when presenting how to install Coq to students. It comes either as a binary, or as a script which automates most of the opam operations.

[elefthei]

I also can't reproduce on a Mac 11.2.3. Perhaps I can get a stacktrace from the student if that's helpful. Coq platform looks like a much better option thanks!

[Zimmi48]

There are good chances that this would be related to gtk, so getting an exact list of versions of installed libraries with brew (not sure what the command is to get this) and with opam (opam list) from your student would probably be the most important information to reproduce (besides the exact macOS version).

[elefthei]

Here's the specs
MacOS Big Sur, Version 11.2.3

# brew list --installed

adwaita-icon-theme 40.1.1
atk 2.36.0
cairo 1.16.0_5
coq 8.13.2
expat 2.3.0
fontconfig 2.13.1
freetype 2.10.4
fribidi 1.0.10
gdbm 1.19
gdk-pixbuf 2.42.6
gettext 0.21
glib 2.68.2
gmp 6.2.1
gobject-introspection 1.68.0
gpatch 2.7.6
graphite2 1.3.14
gsettings-desktop-schemas 40.0
gtk+3 3.24.29
gtksourceview3 3.24.11_3
harfbuzz 2.8.1
hicolor-icon-theme 0.17
icu4c 69.1
jpeg 9d
libepoxy 1.5.7
libffi 3.3_3
libpng 1.6.37
libpthread-stubs 0.4
librsvg 2.50.5
libtiff 4.3.0
libx11 1.7.1
libxau 1.0.9
libxcb 1.14_1
libxdmcp 1.1.3
libxext 1.3.4
libxml2 2.9.10_2
libxrender 0.9.10
lzo 2.10
mpdecimal 2.5.1
ocaml 4.12.0
ocaml-zarith 1.12_1
opam 2.0.8
openssl@1.1 1.1.1k
pango 1.48.5
pcre 8.44
pixman 0.40.0
pkg-config 0.29.2_3
python@3.9 3.9.5
readline 8.1
sqlite 3.35.5
xorgproto 2021.4
xz 5.2.5

# opam list

# Packages matching: installed
# Name         # Installed # Synopsis
base-bigarray      base
base-threads      base
base-unix        base
cairo2         0.6.2    Binding to Cairo, a 2D Vector Graphics Libra
conf-adwaita-icon-theme 1      Virtual package relying on adwaita-icon-them
conf-cairo       1      Virtual package relying on a Cairo system in
conf-findutils     1      Virtual package relying on findutils
conf-gmp        3      Virtual package relying on a GMP lib system 
conf-gtk3        18     Virtual package relying on GTK+ 3
conf-gtksourceview3   0+2     Virtual package relying on a GtkSourceView-3
conf-pkg-config     2      Check if pkg-config is installed and create 
coq           8.13.1   pinned to version 8.13.1
coqide         8.13.1   IDE of the Coq formal proof management syste
csexp          1.5.1    Parsing and printing of S-expressions in Can
dune          2.8.5    Fast, portable, and opinionated build system
dune-configurator    2.8.5    Helper library for gathering system configur
lablgtk3        3.1.1    OCaml interface to GTK+3
lablgtk3-sourceview3  3.1.1    OCaml interface to GTK+ gtksourceview librar
num           1.4     The legacy Num library for arbitrary-precisi
ocaml          4.12.0   The OCaml compiler (virtual package)
ocaml-base-compiler   4.12.0   Official release 4.12.0
ocaml-config      2      OCaml Switch Configuration
ocaml-options-vanilla  1      Ensure that OCaml is compiled with no specia
ocamlfind        1.9.1    A library manager for OCaml
opam-depext       1.1.5    install OS distribution packages
result         1.5     Compatibility Result module
zarith         1.12    Implements arithmetic and logical operations

[davidnowak]

I have the same issue after the full re-install of homebrew, opam 2.1 and coqide 8.13.2, under macOS Catalina 10.15.7.

[foncteur]

I have a segfault with CoqIDE on a MacBook Air M1 too (macOS Big Sur version 11.3.1).
Here are the steps I did to install OCaml and Coq:

brew install ocaml
brew install opam
opam init
eval $(opam env)
opam install coq
opam install coqide
eval $(opam env)

and I get the following error:

(coqide:67401): Gtk-WARNING **: 09:58:51.408: Drawing a gadget with negative dimensions. Did you forget to allocate a size? (node header owner GtkNotebook)```

[davidnowak]

I have found a workaround: Just downgrade OCaml to 4.11.1.
The bug occurs with OCaml 4.12 and 4.13.

[davidnowak]

The bug is still there with Coqide 8.14.0.
The same workaround (downgrading OCaml to 4.11.2) works.

[Zimmi48]

@MSoegtropIMC: I think you should be aware of this. OCaml 4.12 / 4.13 are causing crashes for many Coq users on macOS. This means that the platform should probably stay on OCaml 4.10 or 4.11 for the time being.

[MSoegtropIMC]

Thanks for letting me know! My plan is to stay with 4.10.2 - or even go back to 4.7.1 except for Apple silicon, in case the plugin issue is severe.

[davidnowak]

It looks like this issue was solved with the release of lablgtk3 3.1.2.