Stream: Coq users

Topic: Installing coqide


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

view this post on Zulip Guillaume Melquiond (Jan 12 2021 at 07:04):

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.

view this post on Zulip Paolo Giarrusso (Jan 12 2021 at 10:45):

(deleted)

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

view this post on Zulip Paolo Giarrusso (Jan 13 2021 at 00:24):

Any chance you don’t have the native dependencies of Coqide installed?

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

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

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

view this post on Zulip Paolo Giarrusso (Jan 13 2021 at 00:27):

probably you need opam install opam-depext first

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

view this post on Zulip Paolo Giarrusso (Jan 13 2021 at 00:28):

oh, you must install them by hand?

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

view this post on Zulip Karl Palmskog (Jan 13 2021 at 00:31):

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

view this post on Zulip Karl Palmskog (Jan 13 2021 at 00:32):

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

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

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

view this post on Zulip Karl Palmskog (Jan 13 2021 at 00:46):

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.

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

view this post on Zulip Karl Palmskog (Jan 13 2021 at 00:48):

you can list switches by opam switch and change to a switch with opam switch <name>

view this post on Zulip Karl Palmskog (Jan 13 2021 at 00:49):

also, one should run eval $(opam env) after entering a switch

view this post on Zulip SoundLogic (Jan 13 2021 at 01:18):

OK, that worked. Thank you so much!

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

view this post on Zulip Gaëtan Gilbert (May 02 2022 at 14:13):

those are just warnings, ignore them

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

view this post on Zulip Gaëtan Gilbert (May 02 2022 at 14:16):

oh I didn't notice the icons
someone else probably knows

view this post on Zulip Lingyuan Ye (May 02 2022 at 14:17):

Thanks! and anyway I may as well just hide the tool bar for sanity...

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

view this post on Zulip Paolo Giarrusso (May 02 2022 at 20:23):

the icons didn't work for me either in the last installation from opam

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

view this post on Zulip Paolo Giarrusso (May 02 2022 at 20:55):

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

view this post on Zulip Paolo Giarrusso (May 02 2022 at 20:57):

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?

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

view this post on Zulip Guillaume Melquiond (May 03 2022 at 08:32):

That is possibly https://gitlab.gnome.org/GNOME/adwaita-icon-theme/-/issues/184

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

view this post on Zulip Michael Soegtrop (May 03 2022 at 09:37):

Which suggests that the names we use are now in "legacy" and we might need to do something in CoqIDE to enable it ...

view this post on Zulip Michael Soegtrop (May 03 2022 at 09:38):

Or that the "legacy" stuff has been removed ...

view this post on Zulip Paolo Giarrusso (May 03 2022 at 10:22):

What’s your version?

view this post on Zulip Paolo Giarrusso (May 03 2022 at 10:24):

(for the Adwaita package)

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

view this post on Zulip Paolo Giarrusso (May 03 2022 at 10:31):

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.

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

view this post on Zulip Michael Soegtrop (May 03 2022 at 12:02):

There might exists a separate legacy package ...

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

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

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

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

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

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

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

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

view this post on Zulip Théo Zimmermann (May 04 2022 at 09:08):

Isn't the error message quite confusing though? Could we get rid of it?

view this post on Zulip Karl Palmskog (May 04 2022 at 09:10):

"This likely means your installation is broken" is a bad message for something you can ignore

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

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

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

view this post on Zulip 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: Feb 06 2023 at 13:03 UTC