Vedran Čačić (Oct 29 2021 at 04:28): Vedran Čačić (Oct 29 2021 at 04:28):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 lablgtk3.3.1.1 (cached)
:down: retrieved lablgtk3-sourceview3.3.1.1 (cached)
∗ installed conf-adwaita-icon-theme.1
∗ installed lablgtk3.3.1.1
∗ installed lablgtk3-sourceview3.3.1.1
∗ installed coqide.8.14.0
Done.
So it seems I do have coqide 8.14. How do I start it?
Guillaume Melquiond (Oct 29 2021 at 04:32):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.
Vedran Čačić (Oct 29 2021 at 04:53):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:).
Guillaume Melquiond (Oct 29 2021 at 05:29):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.
Paolo Giarrusso (Oct 29 2021 at 05:50):@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.
Vedran Čačić (Oct 29 2021 at 06:50):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!
Enrico Tassi (Oct 29 2021 at 07:08):when it is needed opam should print a message, iirc
Paolo Giarrusso (Oct 29 2021 at 07:10):Is it ever needed? This is weird... Do you need multiple switches for that to happen?
Guillaume Melquiond (Oct 29 2021 at 07:27):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.
Paolo Giarrusso (Oct 29 2021 at 07:40):Thanks for reminding me; that's indeed a much more likely reason for which and the shell to disagree.
Last updated: Oct 01 2023 at 18:01 UTC