I did everything as https://coq.inria.fr/opam-using.html says, however, coqc is version 8.14, yet coqide still starts Coq 8.13.2. It's very weird since I got this output:
✦ ❯ opam install coqide
The following actions will be performed:
∗ install lablgtk3 3.1.1 [required by lablgtk3-sourceview3]
∗ install conf-adwaita-icon-theme 1 [required by coqide]
∗ install lablgtk3-sourceview3 3.1.1 [required by coqide]
∗ install coqide 8.14.0
===== ∗ 4 =====
Do you want to continue? [Y/n] y
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
:down: retrieved coqide.8.14.0 (cached)
:down: retrieved lablgtk126.96.36.199 (cached)
:down: retrieved lablgtk3-sourceview188.8.131.52 (cached)
∗ installed conf-adwaita-icon-theme.1
∗ installed lablgtk184.108.40.206
∗ installed lablgtk3-sourceview220.127.116.11
∗ installed coqide.8.14.0
So it seems I do have coqide 8.14. How do I start it?
How do you expect to start it? Through a shell command line? If so, you can type
which coqide, just to make sure that the one you start if the one you just compiled with Opan.
Well, I guess this is my question. "which coqide" gives me "/home/veky/.opam/default/bin/coqide", which really seems like "the one I just compiled with opam". The whole opam thing is quite mysterious to me, I don't really know _where_ it installs anything, and don't know how I could figure it out (other than by trapping disk access:).
This seems fine to me. If you type
opam show coqide, it should tell you
all-installed-versions: 8.14.0 [default]. (Just to make sure 8.14.0 was installed in
default.) Alternatively, you can also type
opam switch, it should tell you that
default is the current switch.
@Vedran Čačić it's not clear how you did try to start coqide; please do describe it. Still: (1) there's probably no "icon" or such that lets you start coqide 8.14.0 (2) can you try to start the new coqide by (a) closing the old one and (b) typing
coqide & at command-line prompt (c) if/when that starts a new coqide windo, checking its version? That should be 8.14.0.
I'm sorry for bothering you, the problem has solved itself upon restarting my shell. But yes, the situation before restarting was as described: I could start both coqc and coqide from the command line, yet coqc would report the version as 8.14.0 and coqide as 8.13.2. That's what led me down the wrong lane... I thought it would be impossible for coqc to not require shell restart, while coqide requiring it. But apparently it is so.
Also, https://coq.inria.fr/opam-using.html doesn't mention anything about restarting the shell. Maybe it should, at least for the benefit of literalists like me. :-D
Thanks for your help anyway!
when it is needed opam should print a message, iirc
Is it ever needed? This is weird... Do you need multiple switches for that to happen?
What might have happened is that the shell that was used is one of those that cache the location of the executable. So, you run
coqide, you notice the wrong version, you install
coqide, you rerun
coqide, but since the shell did remember the location of the original one (e.g.,
/usr/bin/coqide), it will keep running it despite the new one being installed elsewhere (e.g.,
~/.opam/default/bin/coqide). For example, Posix/Bourne's shells have a
hash -r to clear the cache without having to restart the shell.
Thanks for reminding me; that's indeed a much more likely reason for
which and the shell to disagree.
Last updated: Jan 27 2023 at 01:03 UTC