SoundLogic (Jan 12 2021 at 02:18): SoundLogic (Jan 12 2021 at 02:18):I'm trying to install coqide through opam, but it seems to be not producing the actual file that it is trying to install (bin/coqide), which I'm not sure how to fix.
sophia@wingsofthought:~$ opam install coqide
The following actions will be performed:
- install coqide 8.13.0
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[coqide.8.13.0] downloaded from cache at https://opam.ocaml.org/cache
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] The installation of coqide failed at "make install-ide-bin install-ide-files install-ide-info install-ide-devfiles".
#=== ERROR while installing coqide.8.13.0 =====================================#
# context 2.0.5 | linux/x86_64 | ocaml-base-compiler.4.09.0 | https://opam.ocaml.org/#0187bf9e
# path ~/.opam/4.09.0/.opam-switch/build/coqide.8.13.0
# command ~/.opam/opam-init/hooks/sandbox.sh install make install-ide-bin install-ide-files install-ide-info install-ide-devfiles
# exit-code 2
# env-file ~/.opam/log/coqide-24307-2dea01.env
# output-file ~/.opam/log/coqide-24307-2dea01.out
### output ###
# rm -f
# make --warn-undefined-variable --no-builtin-rules -f Makefile.build install-ide-bin install-ide-files install-ide-info install-ide-devfiles
# make[1]: Entering directory '/home/sophia/.opam/4.09.0/.opam-switch/build/coqide.8.13.0'
# install -d "/home/sophia/.opam/4.09.0/bin"
# install bin/coqide "/home/sophia/.opam/4.09.0/bin"
# install: cannot stat 'bin/coqide': No such file or directory
# make[1]: *** [Makefile.ide:201: install-ide-bin] Error 1
# make[1]: Leaving directory '/home/sophia/.opam/4.09.0/.opam-switch/build/coqide.8.13.0'
# make: *** [Makefile.make:178: submake] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - install coqide 8.13.0
+-
- No changes have been performed
Unfortunaly, Opam only shows the last lines of a failed compilation, not the first ones. So, you first need to recover the output of the configure script by looking at the output-file line above, so that we have a clue as to why it thought it was impossible to build coqide.
Paolo Giarrusso (Jan 12 2021 at 10:45):(deleted)
SoundLogic (Jan 13 2021 at 00:13):The output file seems to contain the same as what appears after ### output ###, the rm -f to Error 2.
Paolo Giarrusso (Jan 13 2021 at 00:24):Any chance you don’t have the native dependencies of Coqide installed?
SoundLogic (Jan 13 2021 at 00:24):Uh, how would I check? I previously had a coqide installed, but wanted to upgrade to the new 8.13 stuff because it looks really cool. Also I have coq installed at 8.13.
Paolo Giarrusso (Jan 13 2021 at 00:26):I’d guess you don’t, because opam is unlikely to install them silently without you doing something for it. Does somebody have good instructions for this?
Paolo Giarrusso (Jan 13 2021 at 00:27):Ah! https://coq.inria.fr/opam-using.html has instructions. Read the part about opam-depext coqide.
Paolo Giarrusso (Jan 13 2021 at 00:27):probably you need opam install opam-depext first
Karl Palmskog (Jan 13 2021 at 00:27):for example, on my ubuntu system:
$ opam-depext lablgtk3-sourceview3
# Detecting depexts using vars: arch=x86_64, os=linux, os-distribution=ubuntu, os-family=debian
# The following system packages are needed:
libcairo2-dev
libexpat1-dev
libgtk-3-dev
libgtksourceview-3.0-dev
pkg-config
oh, you must install them by hand?
SoundLogic (Jan 13 2021 at 00:28):It looks like it is fine?
sophia@wingsofthought:~$ opam-depext coq
# Detecting depexts using vars: arch=x86_64, os=linux, os-distribution=debian, os-family=debian
# The following system packages are needed:
findutils
libgmp-dev
m4
perl
# All required OS packages found.
sophia@wingsofthought:~$ opam-depext coqide
# Detecting depexts using vars: arch=x86_64, os=linux, os-distribution=debian, os-family=debian
# The following system packages are needed:
adwaita-icon-theme
findutils
libcairo2-dev
libexpat1-dev
libgmp-dev
libgtk-3-dev
libgtksourceview-3.0-dev
m4
perl
pkg-config
# All required OS packages found.
I never use CoqIDE, but it installed fine for me:
∗ installed conf-pkg-config.1.3
∗ installed conf-adwaita-icon-theme.1
∗ installed conf-cairo.1
∗ installed conf-gtk3.18
∗ installed conf-gtksourceview3.0+2
∗ installed result.1.5
∗ installed csexp.1.3.2
∗ installed dune-configurator.2.7.1
∗ installed cairo2.0.6.2
∗ installed lablgtk3.3.1.1
∗ installed lablgtk3-sourceview3.3.1.1
∗ installed coqide.8.13.0
opam 2.0.5 has some bugs, it may be worth upgrading to 2.0.7, creating a new switch and installing coq and coqide from scratch
SoundLogic (Jan 13 2021 at 00:33):I observe if I try to install the version of dune-configurator mentioned there, it mentions on actions performed upgrade dune-configurator 1.0.0 to 2.7.1 which suggests some things are rather out of date perhaps? I'll try upgrading opam.
SoundLogic (Jan 13 2021 at 00:44):I seem to have gotten a very similar result with the upgrading, though I don't know about a 'new switch' so if that didn't happen then... uh, that might be the issue I don't know.
sophia@wingsofthought:~$ opam install coqide
The following actions will be performed:
- install coqide 8.13.0
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> retrieved coqide.8.13.0 (cached)
[ERROR] The installation of coqide failed at "make install-ide-bin install-ide-files install-ide-info install-ide-devfiles".
#=== ERROR while installing coqide.8.13.0 =====================================#
# context 2.1.0~beta3 | linux/x86_64 | ocaml-base-compiler.4.09.0 | https://opam.ocaml.org/#c481c7aa
# path ~/.opam/4.09.0/.opam-switch/build/coqide.8.13.0
# command ~/.opam/opam-init/hooks/sandbox.sh install make install-ide-bin install-ide-files install-ide-info install-ide-devfiles
# exit-code 2
# env-file ~/.opam/log/coqide-27043-6d07ae.env
# output-file ~/.opam/log/coqide-27043-6d07ae.out
### output ###
# rm -f
# make --warn-undefined-variable --no-builtin-rules -f Makefile.build install-ide-bin install-ide-files install-ide-info install-ide-devfiles
# make[1]: Entering directory '/home/sophia/.opam/4.09.0/.opam-switch/build/coqide.8.13.0'
# install -d "/home/sophia/.opam/4.09.0/bin"
# install bin/coqide "/home/sophia/.opam/4.09.0/bin"
# install: cannot stat 'bin/coqide': No such file or directory
# make[1]: *** [Makefile.ide:201: install-ide-bin] Error 1
# make[1]: Leaving directory '/home/sophia/.opam/4.09.0/.opam-switch/build/coqide.8.13.0'
# make: *** [Makefile.make:178: submake] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - install coqide 8.13.0
+-
- No changes have been performed
an opam switch is a completely new set of opam packages that you can change to on command. For example:
opam switch create 4.09.0.coq8.13 4.09.0
gives you a clean "package environment" to install coq and coqide from scratch.
Karl Palmskog (Jan 13 2021 at 00:47):it may be worth trying since sometimes the default opam switch may end up in a bad state
Karl Palmskog (Jan 13 2021 at 00:48):you can list switches by opam switch and change to a switch with opam switch <name>
Karl Palmskog (Jan 13 2021 at 00:49):also, one should run eval $(opam env) after entering a switch
SoundLogic (Jan 13 2021 at 01:18):OK, that worked. Thank you so much!
Lingyuan Ye (May 02 2022 at 14:10):Hi there, I'm new to coq, and I have just installed the coqide via source file (I'm on an M1 mac). The script runs successfully, but after installation something does not work quite, see the screenshots attached. Any idea how to fix this? Screenshot-2022-05-02-at-22.07.11.png Screenshot-2022-05-02-at-22.07.13.png
Gaëtan Gilbert (May 02 2022 at 14:13):those are just warnings, ignore them
Lingyuan Ye (May 02 2022 at 14:15):yes, I can run code just fine, but the icons also does not appear in the IDE interface, which isn't that big a deal, but I'm wondering whether there's some easy way to get that right...
Gaëtan Gilbert (May 02 2022 at 14:16):oh I didn't notice the icons
someone else probably knows
Lingyuan Ye (May 02 2022 at 14:17):Thanks! and anyway I may as well just hide the tool bar for sanity...
Théo Zimmermann (May 02 2022 at 20:05):It probably means that you are missing some external dependency. You built Coq from source directly without using opam nor the Coq Platform scripts, right? If you used these, then the icons should have been there, I think.
Paolo Giarrusso (May 02 2022 at 20:23):the icons didn't work for me either in the last installation from opam
Paolo Giarrusso (May 02 2022 at 20:54):Just reinstalled coqide to confirm and yes, same symptoms. And I do have the theme:
$ brew info adwaita-icon-theme
adwaita-icon-theme: stable 42.0 (bottled)
Icons for the GNOME project
https://developer.gnome.org
/opt/homebrew/Cellar/adwaita-icon-theme/42.0 (5,031 files, 16.6MB) *
Poured from bottle on 2022-04-05 at 15:43:51
From: https://github.com/Homebrew/homebrew-core/blob/HEAD/Formula/adwaita-icon-theme.rb
License: LGPL-3.0-or-later or CC-BY-SA-3.0
==> Dependencies
Build: gettext ✔, gtk+3 ✔, intltool ✘, pkg-config ✔
Required: librsvg ✔
==> Analytics
install: 17,845 (30 days), 33,975 (90 days), 127,645 (365 days)
install-on-request: 9,244 (30 days), 14,484 (90 days), 53,023 (365 days)
build-error: 0 (30 days)
Ditto for last platform:
$ opam sw __coq-platform.2022.04.0~8.15~2022.04
$ coqide
(coqide:45272): Gtk-WARNING **: 22:55:08.152: Error loading theme icon 'document-save' for stock: Icon 'document-save' not present in theme Adwaita
(coqide:45272): Gtk-WARNING **: 22:55:08.153: Error loading theme icon 'window-close' for stock: Icon 'window-close' not present in theme Adwaita
(coqide:45272): Gtk-WARNING **: 22:55:08.153: Error loading theme icon 'go-down' for stock: Icon 'go-down' not present in theme Adwaita
(coqide:45272): Gtk-WARNING **: 22:55:08.153: Error loading theme icon 'go-up' for stock: Icon 'go-up' not present in theme Adwaita
(coqide:45272): Gtk-WARNING **: 22:55:08.153: Error loading theme icon 'go-jump' for stock:
(coqide:45272): Gtk-WARNING **: 22:55:08.153: Error loading theme icon 'go-bottom' for stock: Icon 'go-bottom' not present in theme Adwaita
(coqide:45272): Gtk-WARNING **: 22:55:08.153: Error loading theme icon 'system-run' for stock: Icon 'system-run' not present in theme Adwaita
(coqide:45272): Gtk-WARNING **: 22:55:08.153: Error loading theme icon 'process-stop' for stock: Icon 'process-stop' not present in theme Adwaita
(coqide:45272): Gtk-WARNING **: 22:55:08.153: Error loading theme icon 'go-top' for stock: Icon 'go-top' not present in theme Adwaita
Ditto for $ opam sw __coq-platform.2021.11.0~8.13~2021.1, so I'd conjecture some breaking change to adwaita broke CoqIDE in the last month?
Paolo Giarrusso (May 03 2022 at 08:26):(https://gitlab.gnome.org/GNOME/adwaita-icon-theme/-/compare/41.0...42.0 is too big to spot renamings easily)
Guillaume Melquiond (May 03 2022 at 08:32):That is possibly https://gitlab.gnome.org/GNOME/adwaita-icon-theme/-/issues/184
Michael Soegtrop (May 03 2022 at 09:35):@Paolo Giarrusso : can you check if you actually have the icon files?
On MacPorts I get:
Adwaita$ pwd
/opt/local/share/icons/Adwaita
Adwaita$ find . -iname "document-save*"
./96x96/actions/document-save-as-symbolic.symbolic.png
./96x96/actions/document-save-symbolic.symbolic.png
./16x16/legacy/document-save-as.png
./16x16/legacy/document-save.png
./16x16/actions/document-save-as-symbolic.symbolic.png
./16x16/actions/document-save-symbolic.symbolic.png
./64x64/actions/document-save-as-symbolic.symbolic.png
./64x64/actions/document-save-symbolic.symbolic.png
./32x32/legacy/document-save-as.png
./32x32/legacy/document-save.png
./32x32/actions/document-save-as-symbolic.symbolic.png
./32x32/actions/document-save-symbolic.symbolic.png
./24x24/legacy/document-save-as.png
./24x24/legacy/document-save.png
./24x24/actions/document-save-as-symbolic.symbolic.png
./24x24/actions/document-save-symbolic.symbolic.png
./22x22/legacy/document-save-as.png
./22x22/legacy/document-save.png
./scalable/actions/document-save-symbolic.svg
./scalable/actions/document-save-as-symbolic.svg
./48x48/legacy/document-save-as.png
./48x48/legacy/document-save.png
./48x48/actions/document-save-as-symbolic.symbolic.png
./48x48/actions/document-save-symbolic.symbolic.png
./512x512/legacy/document-save-as.png
./512x512/legacy/document-save.png
Which suggests that the names we use are now in "legacy" and we might need to do something in CoqIDE to enable it ...
Michael Soegtrop (May 03 2022 at 09:38):Or that the "legacy" stuff has been removed ...
Paolo Giarrusso (May 03 2022 at 10:22):What’s your version?
Paolo Giarrusso (May 03 2022 at 10:24):(for the Adwaita package)
Paolo Giarrusso (May 03 2022 at 10:26):for me:
$ find /opt/homebrew/Cellar/adwaita-icon-theme/42.0/share/icons/Adwaita -iname "document-save*"
/opt/homebrew/Cellar/adwaita-icon-theme/42.0/share/icons/Adwaita/96x96/actions/document-save-as-symbolic.symbolic.png
/opt/homebrew/Cellar/adwaita-icon-theme/42.0/share/icons/Adwaita/96x96/actions/document-save-symbolic.symbolic.png
/opt/homebrew/Cellar/adwaita-icon-theme/42.0/share/icons/Adwaita/16x16/actions/document-save-as-symbolic.symbolic.png
/opt/homebrew/Cellar/adwaita-icon-theme/42.0/share/icons/Adwaita/16x16/actions/document-save-symbolic.symbolic.png
/opt/homebrew/Cellar/adwaita-icon-theme/42.0/share/icons/Adwaita/64x64/actions/document-save-as-symbolic.symbolic.png
/opt/homebrew/Cellar/adwaita-icon-theme/42.0/share/icons/Adwaita/64x64/actions/document-save-symbolic.symbolic.png
/opt/homebrew/Cellar/adwaita-icon-theme/42.0/share/icons/Adwaita/32x32/actions/document-save-as-symbolic.symbolic.png
/opt/homebrew/Cellar/adwaita-icon-theme/42.0/share/icons/Adwaita/32x32/actions/document-save-symbolic.symbolic.png
/opt/homebrew/Cellar/adwaita-icon-theme/42.0/share/icons/Adwaita/24x24/actions/document-save-as-symbolic.symbolic.png
/opt/homebrew/Cellar/adwaita-icon-theme/42.0/share/icons/Adwaita/24x24/actions/document-save-symbolic.symbolic.png
/opt/homebrew/Cellar/adwaita-icon-theme/42.0/share/icons/Adwaita/scalable/actions/document-save-symbolic.svg
/opt/homebrew/Cellar/adwaita-icon-theme/42.0/share/icons/Adwaita/scalable/actions/document-save-as-symbolic.svg
/opt/homebrew/Cellar/adwaita-icon-theme/42.0/share/icons/Adwaita/48x48/actions/document-save-as-symbolic.symbolic.png
/opt/homebrew/Cellar/adwaita-icon-theme/42.0/share/icons/Adwaita/48x48/actions/document-save-symbolic.symbolic.png
Michael Soegtrop said:
Or that the "legacy" stuff has been removed ...
The issue that @Guillaume Melquiond found sounds related — gtk worked around that by readding legacy icons (https://gitlab.gnome.org/GNOME/gtk/-/commit/5a0ffbbb4568e39bdf26006e1bf18c1c1d0d597a). And 42.0 has commits like e.g. "fullcolor: legacy icons purge" —
https://gitlab.gnome.org/GNOME/adwaita-icon-theme/-/commit/f24f640e44aab45730be9ff64dcf46a0a7639a94. Beware the gitlab diff shown is not complete — you just see the first 20 files changed, but there are 9 pages.
Michael Soegtrop (May 03 2022 at 12:01):Paolo Giarrusso said:
What’s your version?
Oldish:
adwaita-icon-theme @3.38.0 gnome/adwaita-icon-theme
So my assumption is that the "legacy" stuff got removed.
We should find out when the new icons have been introduced and I guess need to change CoqIDE then.
I am not sure how feasible it is to make a version specific adwaite opam package - I guess it would be quite hard.
Michael Soegtrop (May 03 2022 at 12:02):There might exists a separate legacy package ...
Filippo A. E. Nuccio (May 04 2022 at 07:56):Hi All, I am very new to Coq, I have been using Lean for a couple of years and I thought I want to give Coq a try. I had some problems with the installation (I am on Win), because I get the following message when I launch CoqIDE:
CoqIDE.png
Filippo A. E. Nuccio (May 04 2022 at 07:56):Yet a window opens and I could type a trivial lemma and it seems to work. Should I worry, is it a known issue on Win?
Karl Palmskog (May 04 2022 at 07:59):Looks like it's this issue. You may want to try using VsCode+VsCoq as a workaround.
Filippo A. E. Nuccio (May 04 2022 at 07:59):Oh, I can use VSCode! That's great, since I am used to it from the Lean experience.
Karl Palmskog (May 04 2022 at 08:01):the experience is a bit different though since VsCoq uses a "processed up to here" indicator. You use Alt+Down and Alt+Up to step one sentence down and up, respectively
Filippo A. E. Nuccio (May 04 2022 at 08:03):Hmm, I guess I am seeing what you mean. I cannot obtain any sensible message in the righ pane.
Filippo A. E. Nuccio (May 04 2022 at 08:05):Oh no, it is simply that I haven't told VSCode yet where my Coq installation is... :face_palm:
Michael Soegtrop (May 04 2022 at 09:07):@Filippo A. E. Nuccio : there is nothing to worry about - it can't find image loaders, but then CoqIDE doesn't use any (this is for JPEG, TIFF and so on).
Théo Zimmermann (May 04 2022 at 09:08):Isn't the error message quite confusing though? Could we get rid of it?
Karl Palmskog (May 04 2022 at 09:10):"This likely means your installation is broken" is a bad message for something you can ignore
Filippo A. E. Nuccio (May 04 2022 at 10:06):Michael Soegtrop said:
Filippo A. E. Nuccio : there is nothing to worry about - it can't find image loaders, but then CoqIDE doesn't use any (this is for JPEG, TIFF and so on).
Thanks!
Michael Soegtrop (May 04 2022 at 11:50):Théo Zimmermann said:
Isn't the error message quite confusing though? Could we get rid of it?
Yes, but it is a bit of work to figure out what is going on and how to fix it. It would help if one could set arbitrary environment variables in the environment file introduced by @Enrico Tassi.
Enrico Tassi (May 04 2022 at 12:05):Hum, now that I found Unix.putenv one can make coqide read the file as well, but one has to process it before Gtk.init is called I guess.
Michael Soegtrop (May 04 2022 at 13:02):I guess so, yes. On Windows this would make things simpler - on Mac currently not, because the current install method has no way to change files, but this might change, so that I could get rid of the wrapper scripts.
Last updated: Sep 30 2023 at 06:01 UTC