Stream: Coq users

Topic: Trouble installing CoqIDE.8.18.0 on Mac OS X


view this post on Zulip Flo (Florent Schaffhauser) (Mar 06 2024 at 15:40):

Hi! I am trying to install CoqIDE.8.18.0 on my machine with macOS Sonoma 14.3.1 and it seems to fail at the step where lablgtk3 is supposed to be installed:

#=== ERROR while compiling lablgtk3.3.1.4 =====================================#
# context     2.1.5 | macos/arm64 | ocaml-base-compiler.5.1.1 | https://opam.ocaml.org#3f84051b
# path        ~/.opam/with-coq/.opam-switch/build/lablgtk3.3.1.4
# command     ~/.opam/opam-init/hooks/sandbox.sh build dune build -p lablgtk3 -j 7
# exit-code   1
# env-file    ~/.opam/log/lablgtk3-50000-5edd1b.env
# output-file ~/.opam/log/lablgtk3-50000-5edd1b.out
### output ###
# [...]
# #define GLIB_DEPRECATED_MACRO_IN_2_30_FOR(f) GLIB_DEPRECATED_MACRO_FOR (f)
#                                              ^
# /opt/homebrew/Cellar/glib/2.78.4/include/glib-2.0/glib/gmacros.h:1299:3: note: expanded from macro 'GLIB_DEPRECATED_MACRO_FOR'
#   _GLIB_GNUC_DO_PRAGMA(GCC warning G_STRINGIFY (Deprecated pre-processor symbol: replace with #f))
#   ^
# /opt/homebrew/Cellar/glib/2.78.4/include/glib-2.0/glib/gmacros.h:1296:33: note: expanded from macro '_GLIB_GNUC_DO_PRAGMA'
# #define _GLIB_GNUC_DO_PRAGMA(x) _Pragma(G_STRINGIFY (x))
#                                 ^
# <scratch space>:80:6: note: expanded from here
#  GCC warning "Deprecated pre-processor symbol: replace with \"const\""
#      ^
# 6 warnings generated.

I tried brew upgrade glib already but I get the same error as above after that.

Would anyone have any clue or recommendation? Thanks in advance!

view this post on Zulip Michael Soegtrop (Mar 06 2024 at 16:52):

Can you try the Coq Platform "from sources" method described here: https://github.com/coq/platform/blob/main/doc/README_macOS.md#installation-by-compiling-from-sources-using-opam?

For just Coq and CoqIDE you can use extent "i" = "IDE" (the script will ask you).

view this post on Zulip Flo (Florent Schaffhauser) (Mar 06 2024 at 17:18):

Thanks! I tried (using "i"= "IDE" when asked by the script) and it seemed to work but then I ran into trouble again:

[ERROR] The compilation of lablgtk3.3.1.4 failed at "dune build -p lablgtk3 -j 4".

I should say that I picked the following version:

(2): Coq 8.18.0 (released Sep 2023) with a package pick based on mathcomp 2.1

and not

(1): Coq 8.18.0 (released Sep 2023) with the first package pick from Nov 2023

Anyway, contrary to what was happening earlier, the installation kept going after hitting an error while installing lablgtk3. At the end, I got the following message:

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build lablgtk3 3.1.4
+-
+- The following changes have been performed (the rest was aborted)
| - install cairo2                  0.6.4
| - install camlp-streams           5.0.1
| - install conf-adwaita-icon-theme 2
| - install conf-cairo              1
| - install conf-findutils          1
| - install conf-gmp                4
| - install conf-gtk3               18
| - install conf-gtksourceview3     0+2
| - install conf-pkg-config         3
| - install coq                     8.18.0
| - install coq-core                8.18.0
| - install coq-stdlib              8.18.0
| - install coqide-server           8.18.0
| - install csexp                   1.5.2
| - install dune                    3.11.1
| - install dune-configurator       3.10.0
| - install ocamlfind               1.9.5~relocatable
| - install zarith                  1.13
+-

view this post on Zulip Flo (Florent Schaffhauser) (Mar 06 2024 at 17:19):

More detail about the install error for lablgtk3:

#=== ERROR while compiling lablgtk3.3.1.4 =====================================#
# context              2.1.5 | macos/arm64 | ocaml-option-flambda.1 ocaml-variants.4.14.1+options | https://opam.ocaml.org#3f84051b
# path                 ~/.opam/CP.2023.11.0~8.18~mc2/.opam-switch/build/lablgtk3.3.1.4
# command              ~/.opam/opam-init/hooks/sandbox.sh build dune build -p lablgtk3 -j 4
# exit-code            1
# env-file             ~/.opam/log/lablgtk3-70674-a1b9d5.env
# output-file          ~/.opam/log/lablgtk3-70674-a1b9d5.out
### output ###
# [...]
# #define alloc_tuple CAML_DEPRECATED("alloc_tuple", "caml_alloc_tuple") caml_alloc_tuple
#                     ^
# /Users/florent/.opam/CP.2023.11.0~8.18~mc2/lib/ocaml/caml/misc.h:58:3: note: expanded from macro 'CAML_DEPRECATED'
#   CAML_PREPROWARNING(name1 is deprecated: use name2 instead)
#   ^
# /Users/florent/.opam/CP.2023.11.0~8.18~mc2/lib/ocaml/caml/misc.h:56:31: note: expanded from macro 'CAML_PREPROWARNING'
# #define CAML_PREPROWARNING(x) _Pragma(CAML_MAKEWARNING2(x))
#                               ^
# <scratch space>:70:6: note: expanded from here
#  GCC warning "\"alloc_tuple\" is deprecated: use \"caml_alloc_tuple\" instead"
#      ^
# 36 warnings generated.

view this post on Zulip Flo (Florent Schaffhauser) (Mar 06 2024 at 17:32):

I do have a previous version of the Coq Platform on my machine, using Coq 8.16.1. I don't know if this is the source of the problem.

view this post on Zulip Paolo Giarrusso (Mar 12 2024 at 19:23):

The output doesn't show the real problem, the error appears truncated

view this post on Zulip Paolo Giarrusso (Mar 12 2024 at 19:25):

and the error lists more complete log files. But if these logs are to be believed, it seems like the building lablgtk release treats deprecation warnings as errors, which is a design mistake in the build, no matter the reason why you get deprecation warnings

view this post on Zulip Flo (Florent Schaffhauser) (Mar 12 2024 at 21:14):

Thanks for sharing your feedback :thank_you: I have tried several things since my previous message, but to no avail. I'll try to start from scratch at some point!


Last updated: Jun 23 2024 at 04:03 UTC