Théo Zimmermann (Dec 03 2020 at 18:39): 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.
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
Théo Zimmermann (Dec 03 2020 at 18:40):Then, opam pin add coq dev.
Théo Zimmermann (Dec 03 2020 at 18:40):Or something like that.
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.
Enzo Crance (Dec 03 2020 at 18:54):Thank you I'll try to find my way from your ideas.
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
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.
Fabian Kunze (Dec 04 2020 at 15:29):opam pin coq coq.dev afaik
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?
Fabian Kunze (Dec 04 2020 at 15:32):what does opam pin list give?
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
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
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
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.
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.
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.
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.
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.
Fabian Kunze (Dec 04 2020 at 17:36):coqide is the gui IDE bundled with coq, you don't need coqide for coqidetop.
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
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.
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".
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).
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.
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
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/...
Paolo Giarrusso (Dec 05 2020 at 00:50):your message about the ./configure -local attempt doesn't say that coqidetop.opt was not created
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
Paolo Giarrusso (Dec 05 2020 at 00:54):but let's try things out a moment...
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]
and it doesn't have a package for coqide-server only
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 .
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 wasopam pin coq --dev-repoto make it work. Now I have a 8.14+alpha version, but I still do not have acoqidetop.optexecutable in the path. According to Fabian Kunze, thecoqideside 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 aboutcoqide? 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:
core-dev repo: in this case, coqidetop will be available by default (without installing coqide);coqide-server package from the same repo). 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.
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
Kenji Maillard (Dec 05 2020 at 13:34):Théo Zimmermann said:
- the discouraged way, using the opam file in the repo: if you do it that way, you also need to install the separate
coqide-serverpackage from the same repo).
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).
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.
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?
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?
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")
Théo Zimmermann (Dec 07 2020 at 10:05):I'll move the topic. You'll probably get more visibility and thus more answers.
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
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).
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
$ 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/
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.
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.
Enzo Crance (Dec 07 2020 at 11:04):Ok it finally worked.
core-dev repositoryopam pin add coq dev -k versionLast updated: Feb 04 2023 at 21:02 UTC