Stream: Coq users

Topic: Installing coqidetop dev with opam


view this post on Zulip Théo Zimmermann (Dec 03 2020 at 18:39):

If you wish to install coq master via opam, I recommend that you do not pin from git but you use the coq.dev package in the core-dev repo instead.

view this post on Zulip Théo Zimmermann (Dec 03 2020 at 18:39):

I.e. run opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev

view this post on Zulip Théo Zimmermann (Dec 03 2020 at 18:40):

Then, opam pin add coq dev.

view this post on Zulip Théo Zimmermann (Dec 03 2020 at 18:40):

Or something like that.

view this post on Zulip Théo Zimmermann (Dec 03 2020 at 18:41):

If you want to pin from git you will have to additionally install the coqide-server package (an opam package is provided in the repo) but I'm not expert enough in opam to tell you how to do this.

view this post on Zulip Enzo Crance (Dec 03 2020 at 18:54):

Thank you I'll try to find my way from your ideas.

view this post on Zulip Fabian Kunze (Dec 03 2020 at 19:01):

in general, opam exec -- your command runs command from the opam-context i think, but i agree with everything theo said

view this post on Zulip Enzo Crance (Dec 04 2020 at 15:27):

I wanted to try what you had suggested yesterday, butopam pin add coq dev throws an error I do not understand. It tries to find sources in a $HOME/dev file.

view this post on Zulip Fabian Kunze (Dec 04 2020 at 15:29):

opam pin coq coq.dev afaik

view this post on Zulip Enzo Crance (Dec 04 2020 at 15:30):

All these flavours of the command fail the same way. Must I reinstall Coq like that from a blank switch?

view this post on Zulip Fabian Kunze (Dec 04 2020 at 15:32):

what does opam pin list give?

view this post on Zulip Enzo Crance (Dec 04 2020 at 15:33):

coq.dev                                    git  git+https://github.com/coq/coq.git#master
coq-doc.dev                 (uninstalled)  git  git+file:///Users/cloudyhug/Desktop/coq-8.13#v8.13
coq-mathcomp-algebra.dev    (uninstalled)  git  git+https://github.com/math-comp/math-comp.git
coq-mathcomp-ssreflect.dev  (uninstalled)  git  git+https://github.com/math-comp/math-comp.git
coqide.dev                  (uninstalled)  git  git+file:///Users/cloudyhug/Desktop/coq-8.13#v8.13
coqide-server.dev           (uninstalled)  git  git+file:///Users/cloudyhug/Desktop/coq-8.13#v8.13
dune.2.7.1                                 git  git+https://github.com/ocaml/dune.git#master
itauto.~dev                                git  git+file:///Users/cloudyhug/Desktop/itauto#master

view this post on Zulip Enzo Crance (Dec 04 2020 at 15:34):

I had installed a Coq version from source before this one (thus the uninstalled ones). But the tool I want to test mentions the first one, the master branch of Coq. This is the one I have installed through opam pin add coq https://github.com/coq/coq.git#master

view this post on Zulip Fabian Kunze (Dec 04 2020 at 16:05):

the way I use coq master with vscoq is by ./configure -local in the coq git, then making it and and then exporting export PATH=~/Research/coq-git/bin:$PATH before I open code . in the terminal, thus avoiding opam altogether

view this post on Zulip Enzo Crance (Dec 04 2020 at 16:08):

Therefore dropping opam seems to be the solution. Not what I would have expected. I'll try to compile it locally like you said and see if it breaks the library I want to test.

view this post on Zulip Fabian Kunze (Dec 04 2020 at 16:11):

actually, I just tried installing master via opam and some problem with testsuite/misc/deps/αβ/γδ.vbreaks this.

view this post on Zulip Enzo Crance (Dec 04 2020 at 16:30):

./configure -local succeeds but warns me about CoqIde

LablGtk3 or LablGtkSourceView3 not found:
=> no CoqIde will be built.

I think this is what happens when building with opam too, the difference is, when one installs Coq through an opam pin, the outputs of the commands cannot be seen.

view this post on Zulip Enzo Crance (Dec 04 2020 at 16:31):

Weird that the stable versions do not need these libraries and get me a coqidetop.opt executable without any problem.

view this post on Zulip Enzo Crance (Dec 04 2020 at 16:57):

I tried to get these installed. Here is an extract from the error I get when running opam install lablgtk3:

$ opam install lablgtk3
The following actions will be performed:
  ∗ install conf-gtk3         18    [required by lablgtk3]
  ∗ install cairo2            0.6.1 [required by lablgtk3]
  ∗ install lablgtk3          3.1.1

∗ installed conf-cairo.1
[ERROR] The compilation of conf-gtk3 failed at
[ERROR] The compilation of cairo2 failed at

#=== ERROR while compiling conf-gtk3.18 =======================================#
# Package 'libpng', required by 'cairo', not found
#=== ERROR while compiling cairo2.0.6.1 =======================================#
c-test-2/test.c:2:10: fatal error: 'cairo.h' file not found
#  | #include <cairo.h>
#  |          ^~~~~~~~~
#  | 1 error generated.
# Error: failed to compile program

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫
┌─ The following actions failed
│ λ build cairo2    0.6.1
│ λ build conf-gtk3 18
└─
┌─ The following changes have been performed (the rest was aborted)
│ ∗ install conf-cairo        1
└─

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

Fun thing, I have already installed the required system packages.

$ brew install gtk+3
Warning: gtk+3 3.24.23 is already installed and up-to-date
$ brew install expat
Warning: expat 2.2.10 is already installed and up-to-date
$ brew install libpng
Warning: libpng 1.6.37 is already installed and up-to-date
$ brew install cairo
Warning: cairo 1.16.0_3 is already installed and up-to-date

At this point I am completely lost and I would not be surprised to learn that opam is too.

view this post on Zulip Fabian Kunze (Dec 04 2020 at 17:36):

coqide is the gui IDE bundled with coq, you don't need coqide for coqidetop.

view this post on Zulip Paolo Giarrusso (Dec 04 2020 at 18:41):

opam pin coq coq.dev is the wrong command here, @Enzo Crance, you must unpin coq first

view this post on Zulip Paolo Giarrusso (Dec 04 2020 at 18:42):

after

coq.dev                                    git  git+https://github.com/coq/coq.git#master

pinning coq.dev directly is a no-op. Unpinning then pinning will fix that.

view this post on Zulip Paolo Giarrusso (Dec 04 2020 at 18:43):

without checking that, I think "I installed coq.dev" gives you no guarantees whatsoever on what you installed — and that's the point because coq.dev stands for "some development version".

view this post on Zulip Paolo Giarrusso (Dec 04 2020 at 18:45):

generally, bypassing opam is not "the fix", it's just a workaround to not knowing the details of how to use opam — not that I'm blaming you for it, opam can be surprising (or sometimes pretty broken, but not here AFAIK).

view this post on Zulip Enzo Crance (Dec 04 2020 at 23:27):

Thank you for your answer @Paolo Giarrusso. I understand. Spending several hours just to get an IDE to work in a development branch and actually start to work is frustrating, and it is easy to get upset and blame the tool.
After a break (a good idea), I have successfully unpinned and reinstalled the dev branch. The command was opam pin coq --dev-repo to make it work. Now I have a 8.14+alpha version, but I still do not have a coqidetop.opt executable in the path. According to @Fabian Kunze, the coqideside is not the one to explore to answer my questions. Is there a way to get such an executable with an opam installation? Or do you mean the local installation would have worked, but I needed to ignore the warning about coqide? Again thank you very much for the help.

view this post on Zulip Paolo Giarrusso (Dec 05 2020 at 00:47):

I'm not an opam dev, and I can relate! I haven't tried but I'd remove all the unpinned, uninstalled entries to avoid problems, in particular the coqide-server one, and then follow Theo's tip

view this post on Zulip Paolo Giarrusso (Dec 05 2020 at 00:49):

but to be sure — I agree with Fabian that you don't need coqide, and in particular, you don't need cairo/lablgtk/...

view this post on Zulip Paolo Giarrusso (Dec 05 2020 at 00:50):

your message about the ./configure -local attempt doesn't say that coqidetop.opt was not created

view this post on Zulip Paolo Giarrusso (Dec 05 2020 at 00:51):

re "remote pin" — remove all the stale ones (so those for coq-8.13), in particular coqide-server.dev and coqide.dev

view this post on Zulip Paolo Giarrusso (Dec 05 2020 at 00:54):

but let's try things out a moment...

view this post on Zulip Paolo Giarrusso (Dec 05 2020 at 00:56):

@Théo Zimmermann regarding the core-dev repo, does it ever install coqidetop? it seems not

$ grep coqidetop core-dev/packages/*/*/files/*install
# NO RESULTS!
$ grep coqtop core-dev/packages/*/*/files/*instal
[lots of results]

view this post on Zulip Paolo Giarrusso (Dec 05 2020 at 00:58):

and it doesn't have a package for coqide-server only

view this post on Zulip Paolo Giarrusso (Dec 05 2020 at 00:59):

finally, to pin coqide-server.opam from the repo, it seems you should do:

opam unpin coqide-server
opam pin coqide-server .

view this post on Zulip Théo Zimmermann (Dec 05 2020 at 12:18):

Enzo Crance said:

Thank you for your answer Paolo Giarrusso. I understand. Spending several hours just to get an IDE to work in a development branch and actually start to work is frustrating, and it is easy to get upset and blame the tool.
After a break (a good idea), I have successfully unpinned and reinstalled the dev branch. The command was opam pin coq --dev-repo to make it work. Now I have a 8.14+alpha version, but I still do not have a coqidetop.opt executable in the path. According to Fabian Kunze, the coqideside is not the one to explore to answer my questions. Is there a way to get such an executable with an opam installation? Or do you mean the local installation would have worked, but I needed to ignore the warning about coqide? Again thank you very much for the help.

I need to repeat myself since you have obviously reinstalled from the git repository. There are two ways to install Coq dev version with opam:

view this post on Zulip Théo Zimmermann (Dec 05 2020 at 12:20):

When we started working on Dune in the dev repo, we didn't realize that users would pick up the opam files and try to install from there since we already provided (since forever) another way to opam install the dev version. That's why we didn't refrain from experimenting a separation into smaller packages, but it has led to much trouble from users.

view this post on Zulip Théo Zimmermann (Dec 05 2020 at 12:30):

To the point that I'm wondering if we shouldn't just remove the opam files from the dev repo (since nowadays, you don't need these files to use Dune): https://github.com/coq/coq/pull/13578

view this post on Zulip Kenji Maillard (Dec 05 2020 at 13:34):

Théo Zimmermann said:

I think I'm the culprit here who proposed this "solution" ignoring that it was discouraged. Sure it's not documented, but it also correspond to a use case for which I didn't find any straightforward documentation (setting up a non-standard coq version + libraries to hack things around and prototype).

view this post on Zulip Théo Zimmermann (Dec 05 2020 at 13:45):

Oh you're certainly not the only culprit. A lot of users have picked up on those opam files as soon as they were available, even before they were even tested.

view this post on Zulip Paolo Giarrusso (Dec 05 2020 at 13:55):

@Théo Zimmermann so why is coqidetop not mentioned by any of the install files in the core.dev repo?

view this post on Zulip Théo Zimmermann (Dec 05 2020 at 15:44):

I don't know (and I'm far from an expert in opam, so I can't comment on the point of this file) but it is exactly the same in the main opam-repository for released versions and it works, doesn't it?

view this post on Zulip Enzo Crance (Dec 07 2020 at 10:04):

Hello. Sorry for asking help again... I am willing to follow @Théo Zimmermann's instructions but still cannot install Coq from the core-dev repo. I removed all the pins related to Coq packages, and only kept the one on dune, because I need it for another library. Then I run successively

opam pin coq dev
opam pin coq coq.dev
opam pin add coq dev
opam pin add coq coq.dev

but all of them failed. The last one I tried is with the URL. The answer is the following:

$ opam pin add coq https://coq.inria.fr/opam/core-dev/packages/coq/coq.dev/
[coq.dev] downloaded from https://coq.inria.fr/opam/core-dev/packages/coq/coq.dev/
[ERROR] Error getting source from
        https://coq.inria.fr/opam/core-dev/packages/coq/coq.dev/:
          - Unknown archive type:
            /private/var/folders/0x/430g858n2z703mtpghf256y40000gn/T/opam-1604-9b8556/coq.dev

Again, I am sorry to spam the channel with install errors. Maybe I should switch to another topic under the Coq users stream, as this is no longer related to VSCoq? (now that I know the VSCoq error meant "missing executable")

view this post on Zulip Théo Zimmermann (Dec 07 2020 at 10:05):

I'll move the topic. You'll probably get more visibility and thus more answers.

view this post on Zulip Notification Bot (Dec 07 2020 at 10:07):

This topic was moved here from #VsCoq devs & users > Coq master branch and VSCoq by Théo Zimmermann

view this post on Zulip Théo Zimmermann (Dec 07 2020 at 10:09):

Did you do the opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev step?
What does opam repo list gives (I think that's the right command, although I cannot test).

view this post on Zulip Karl Palmskog (Dec 07 2020 at 10:10):

looks to me like running opam pin coq dev is the wrong command to run, and it could affect subsequent commands. I would recommend creating a completely new switch, adding the core-dev repo, then running:

opam pin add coq dev -k version

view this post on Zulip Enzo Crance (Dec 07 2020 at 10:13):

$ opam repo list
[NOTE] These are the repositories in use by the current switch. Use '--all' to
       see all configured repositories.

<><> Repository configuration for switch coq-8.13 <><><><><><><><><><><><><>  🐫
 1 coq-core-dev  https://coq.inria.fr/opam/core-dev
 2 coq-extra-dev https://coq.inria.fr/opam/extra-dev
 3 coq-released  https://coq.inria.fr/opam/released
 4 default       https://opam.ocaml.org/

view this post on Zulip Enzo Crance (Dec 07 2020 at 10:15):

This might come from a conflict in the repositories. I will try to make a brand new switch again, and make sure only this core-dev repo is added.

view this post on Zulip Karl Palmskog (Dec 07 2020 at 10:21):

there is to my knowledge no conflict between the repositories, but limiting what can be installed in a switch is generally a good idea. The key idea is that switches contain a ton of hidden state that can interfere with installation, so starting from a new one is a good approach.

view this post on Zulip Enzo Crance (Dec 07 2020 at 11:04):

Ok it finally worked.

  1. Installed a new switch
  2. Added only the core-dev repository
  3. opam pin add coq dev -k version
    Having several repositories was making the commands fail. Thank you all for your help!

Last updated: Feb 04 2023 at 21:02 UTC