Matthieu Sozeau (Sep 14 2022 at 15:34): Matthieu Sozeau (Sep 14 2022 at 15:34):I'm surprised, having just updated my opam coq.dev (and coq-core.dev) to the latest version to not find _opam/bin/coqidetop.opt anymore...
Matthieu Sozeau (Sep 14 2022 at 15:35):Meaning, my vscoq can't work
Gaëtan Gilbert (Sep 14 2022 at 15:44):it's in coqide-server not coq-core
Matthieu Sozeau (Sep 14 2022 at 15:45):Hmm, ok
Matthieu Sozeau (Sep 14 2022 at 15:45):opam search coqide
# Packages matching: match(*coqide*)
# Name # Installed # Synopsis
coq dev Coq is a formal proof management system.
coqide -- IDE of the Coq formal proof management system
So I don't have a coqide-server package...
Matthieu Sozeau (Sep 14 2022 at 15:53):It seems to be missing from the core-dev repo... @Enrico Tassi maybe you have an idea what's going on?
Enrico Tassi (Sep 14 2022 at 16:12):sadly no, I'm too swamped to follow opam in these weeks
Théo Zimmermann (Sep 14 2022 at 16:12):Indeed, the package is missing and should be added.
Théo Zimmermann (Sep 14 2022 at 16:18):Did it used to work up to 8.16? In this case, it would be a bug in the PR that did the split: https://github.com/coq/opam-coq-archive/pull/1923
Karl Palmskog (Sep 14 2022 at 16:18):define "package". Do you mean there should be a separate coqidetop.dev package?
Matthieu Sozeau (Sep 14 2022 at 16:19):A coqide-server package I guess, as it used to be?
Karl Palmskog (Sep 14 2022 at 16:19):I can confirm that coqidetop.opt gets installed with 8.16.0 at least.
Matthieu Sozeau (Sep 14 2022 at 16:21):That's strange that nobody noticed this before, maybe the coqide target installed coqidetop.opt anyway?
Théo Zimmermann (Sep 14 2022 at 16:23):Indeed, it probably does if it is not in scope. But not a lot of people are using the coq.dev package for day to day development I think.
Karl Palmskog (Sep 14 2022 at 16:25):I use it for command line testing and then I use proofgeneral, which does not use coqidetop, I believe.
Karl Palmskog (Sep 14 2022 at 16:25):I suspect a strong correlation between coq.dev usage and Emacs
Gaëtan Gilbert (Sep 14 2022 at 16:29):cc @Emilio Jesús Gallego Arias
Matthieu Sozeau (Sep 14 2022 at 16:34):Well, too bad, I want to develop in vscode and not install lablgtk :) Just using the coqide-server package from github.com/coq/coq works
Emilio Jesús Gallego Arias (Sep 15 2022 at 11:21):Yes, indeed we forgot about the coqide-server package
Emilio Jesús Gallego Arias (Sep 15 2022 at 11:21):sorry about hat
Emilio Jesús Gallego Arias (Sep 15 2022 at 11:21):that
Théo Zimmermann (Sep 15 2022 at 11:24):Matthieu opened a PR adding it.
Karl Palmskog (Sep 15 2022 at 11:26):indeed, but please help figure out errors if you have time: https://github.com/coq/opam-coq-archive/pull/2308
Karl Palmskog (Sep 17 2022 at 09:46):should coqide-server.dev be a dependency of coqide.dev? Right now, it isn't, so I guess people who build coqide.dev from scratch will get runtime errors. https://github.com/coq/opam-coq-archive/blob/master/core-dev/packages/coqide/coqide.dev/opam
Paolo Giarrusso (Sep 17 2022 at 11:55):I can't imagine good reasons against the dependency, _and_ the coq/coq version has the dep: https://github.com/coq/coq/blob/4002111e7f0ada53a86a37a7134a04cebc231bdd/coqide.opam
Karl Palmskog (Sep 17 2022 at 11:57):hmm, so coqide.dev should depend only on coqidetop.dev? Can someone from the core team such as @Emilio Jesús Gallego Arias confirm this is as intended even for opam users?
Paolo Giarrusso (Sep 17 2022 at 11:58):that's not what happens tho
Paolo Giarrusso (Sep 17 2022 at 11:58):the coq/coq coqide-server depends on coq-core — but I suspect that at least coqide should depend on coq-stdlib as well
Karl Palmskog (Sep 17 2022 at 12:00):I guess the question is what should happen when someone starts with a fresh opam switch and does opam install coqide.dev. Should they get Stdlib or not? I guess not getting Stdlib is a conservative option since the user may be a HoTT fan
Paolo Giarrusso (Sep 17 2022 at 12:01):there's indeed a policy question; but building the stdlib probably isn't harmful for HoTT fans except build times
Karl Palmskog (Sep 17 2022 at 12:04):OK, I'm declaring this above my (nonexistent) pay grade. I'll do a PR which at least adds the coqide-server dep to coqide.dev. But then there are even more mysterious stuff, such as why the coqide.dev package in the Coq repo doesn't even depend on lablgtk3-sourceview3.
Paolo Giarrusso (Sep 17 2022 at 12:05):yeah, I hope that one is an issue with autogeneration, and not a conscious decision?
Paolo Giarrusso (Sep 17 2022 at 12:08):what about having (for both dev and non-dev) coqide-core and coqide packages, parallel to coq-core and coq? That lets you opt-in to "no stdlib", without affecting users who want things as-is.
Karl Palmskog (Sep 17 2022 at 12:09):hm, then we also get coqide-server-core and coqide-server packages I think. The cores multiply
Paolo Giarrusso (Sep 17 2022 at 12:11):Good question, but at least coqide-server did not exist for long.
Paolo Giarrusso (Sep 17 2022 at 12:12):and anyway, since I guess packages should converge with coq/coq eventually, such changes must be led by core devs.
Karl Palmskog (Sep 17 2022 at 12:12):ah, so a Coq Call question. That escalated quickly
Paolo Giarrusso (Sep 17 2022 at 12:14):not worth it just for .dev, but for release packages it seems worth the time — it's a follow-up to the stdlib split IMHO?
Karl Palmskog (Sep 17 2022 at 12:15):yes, I guess the topic might be: can we please sort out the Coq opam package dependency graph
Paolo Giarrusso (Sep 17 2022 at 12:16):and .dev should eventually align as well... To automate releases/updates via dune-release, upgrades, etc
Karl Palmskog (Sep 17 2022 at 12:30):OK, I'm declaring coqide.dev from the core-dev opam repo borked. It installs, but I don't even get a coqide executable...
Karl Palmskog (Sep 17 2022 at 12:35):There's been some parsimonious changes since I last tried CoqIDE apparently:
/path/to/switch/lib$ ls coqide/
dune-package META opam
I suppose it is because coqide is marked as optional in ide/coqide/dune, so Dune does not try to build it. And similarly, I suppose it is the reason for lablgtk3-sourceview3 to not be declared a dependency, since the coqide binary is an optional component of the coqide package.
Karl Palmskog (Sep 17 2022 at 12:45):OK, that sounds to me like a bug in ide/coqide/dune... Should we report it?
Karl Palmskog (Sep 17 2022 at 12:46):wait, what the heck... if I installed coqide-server.dev package first, as it should be, then I actually get coqide binary. Dune magic?
Paolo Giarrusso (Sep 17 2022 at 15:02):It's worth a bug report — you can link https://github.com/coq/coq/pull/16505, which tries the naive fix
Karl Palmskog (Sep 17 2022 at 16:51):it occurs to me that there is an argument for making coqide-server package a dependency of the coq.dev package. Otherwise, when the new Coq-related packages are deployed and people use opam to install coq, they will not be able to use VS Code / VsCoq without figuring out that they need to install coqide-server as well. Hardly intuitive.
Paolo Giarrusso (Sep 17 2022 at 17:11):And that also matches the old setup, right?
Karl Palmskog (Sep 17 2022 at 17:13):it seems you get coqidetop through coq for 8.16, yes.
Karl Palmskog (Sep 17 2022 at 19:46):oh wait, I think we should add a conflict for coqide-server as well with old Coq, because of the coqidetop clash:
conflicts: [
"coq" { < "8.17" }
]
That makes sense. FWIW, https://github.com/coq/coq/pull/16505 is just about the optional bug that you and Guillaume pointed out, and the lablgtk dependency.
Paolo Giarrusso (Sep 18 2022 at 12:54):wait, what the heck... if I installed coqide-server.dev package first, as it should be, then I actually get coqide binary. Dune magic?
AFAICT, the real thing is that coqide.opa builds coqide.exe iff lablgtk3-sourceview3 is pre-installed.
And similarly, I suppose it is the reason for lablgtk3-sourceview3 to not be declared a dependency, since the coqide binary is an optional component of the coqide package.
Does that mean that dune should infer that dependency? I'll believe you, but I didn't get dune to auto-infer it; manually specifying it in dune-project worked. (Modulo the part where the outputs are not actually auto-generated).
Paolo Giarrusso (Sep 18 2022 at 12:55):BTW, do you know the whole # This file is generated by dune, edit dune-project instead? That's not quite right, because generate_opam_files is disabled in coq/dune-project:
; After Dune 2.8 we can use this, but let's wait for the build consolidation PR
; (generate_opam_files true)
Paolo Giarrusso said:
Does that mean that dune should infer that dependency?
It is not a matter of inferring. It is explicitly written in ide/coqide/dune:
(library
(name coqide_gui)
...
(libraries coqide-server.protocol coqide-server.core lablgtk3-sourceview3))
I think we should just remove the autogenerated message from the packages in the core-dev repo, it seems obvious we'll have to tweak over time...
Paolo Giarrusso (Sep 18 2022 at 16:51):@Guillaume Melquiond I understand, but as I said it didn't work (I tried) and other opam deps are declared explicitly in dune-project. Among other reasons, you're pointing to an ocaml library name, not an opam package name, and how should dune correctly map among the two? Or (worse) deduce the needed version bounds
Paolo Giarrusso (Sep 18 2022 at 16:53):And again as I said, I could well be wrong and you're welcome to improve/replace my MR if you have better.
Guillaume Melquiond (Sep 18 2022 at 17:22):Paolo Giarrusso said:
Among other reasons, you're pointing to an ocaml library name, not an opam package name, and how should dune correctly map among the two?
Because the dune file explicitly gives this mapping:
(executable
...
(package coqide)
...
(libraries coqide_gui))
It seems like you are asking me what is the rationale behind the behavior of Dune. Sorry, I have no answer.
Paolo Giarrusso (Sep 18 2022 at 19:29):Ah, two misunderstandings:
Paolo Giarrusso (Sep 18 2022 at 19:54):lablgtk3-sourceview3 when that library isn't installed? Here they match, but it could also come from opam package toto-tata, no? Paolo Giarrusso (Sep 18 2022 at 20:14):okay, the only irregular name seems findlib.* coming from ocamlfind, and the libraries coming with OCaml — everything else goes by pkg_name or pkg_name.sth, so I guess there's at least a convention.
Matthieu Sozeau (Sep 19 2022 at 20:07):BTW, there is a slight problem with the .dev packages: one will naturally do opam upgrade coq.dev from time to time, but that's useless and one should always do upgrade coq-core.dev to get the actual updated coq. I'm not sure we can do anything about it but warn.
Paolo Giarrusso (Sep 19 2022 at 20:15):That seems a surprising opam bug: if you pin to a git branch URL, opam update will do the right thing, so why not for packages with the same URL?
Matthieu Sozeau (Sep 20 2022 at 06:21):Somehow the commit hash should be part of the version I guess
Matthieu Sozeau (Sep 20 2022 at 06:22):In my case I did an explicit opam upgrade coq.dev, if I do a general update + upgrade then it’s fine I guess
Guillaume Melquiond (Sep 20 2022 at 06:30):I think you are supposed to do an update (otherwise Opam does not notice that the Git repository was modified), and then you can do a pinpointed upgrade; no need for a general upgrade.
Matthieu Sozeau (Sep 20 2022 at 07:32):Ok, I’ll try that
Karl Palmskog (Sep 27 2022 at 09:16):The following tasks were carried out:
coqide-server package was added to the core-dev opam repocoqide package in the Coq GitHub repo was changed to unconditionally build CoqIDEHowever, we still have the following issue (or not, depending on viewpoint): coqidetop was previously (8.16.0 and below) installed as part of the coq opam package, but now it's not anymore. So people who install coq from the core-dev opam repo can't use CoqIDE or VsCoq unless they figure out that they need to install the coqide-server package.
Do we fix this? For example, the coq opam package could be changed to include a dependency on coqide-server to preserve the behavior from 8.16.0 and lower. Should someone open a PR to do this?
Matthieu Sozeau (Sep 27 2022 at 09:25):I believe coq should depend on coqide-server indeed
Karl Palmskog (Sep 27 2022 at 09:26):OK, then I can just do a straight PR to add this, unless someone else wants to
Karl Palmskog (Sep 27 2022 at 09:49):https://github.com/coq/coq/pull/16549
Karl Palmskog (Sep 27 2022 at 09:50):is a changelog entry even needed for this?
Emilio Jesús Gallego Arias (Sep 27 2022 at 10:31):Yeah, both options are IMHO Ok, to add the dep, or to ask users to install the coqide-server package
Emilio Jesús Gallego Arias (Sep 27 2022 at 10:33):I think that eventually coq will remove the dependency on coqide-server, so a plan for that is needed anyways.
Karl Palmskog (Sep 27 2022 at 10:34):We currently don't have any way to signal to users that an opam package is missing using error messages (from say CoqIDE or VsCoq). So unless something is developed in this direction, I think coqidetop should be preserved as part of coq package. This was the previous behavior, after all...
Karl Palmskog (Sep 27 2022 at 10:39):but it would indeed be good with a longer-term plan how a possible transition away from coqidetop could look like (e.g., via this)
Emilio Jesús Gallego Arias (Sep 27 2022 at 11:05):It seems sensible to me that coqide would depend on coqide-server no?
Emilio Jesús Gallego Arias (Sep 27 2022 at 11:06):Yes it was the previous behavior, but the point of the package split was precisely to allow us to refine this behavior
Emilio Jesús Gallego Arias (Sep 27 2022 at 11:06):in particular help users not to install things they don't need
Emilio Jesús Gallego Arias (Sep 27 2022 at 11:07):Not a big deal either way
Emilio Jesús Gallego Arias (Sep 27 2022 at 11:08):But I don't think it would be a big deal that 8.17 announcement has something like "the Coq xml protocol server has now been split to the coqide-server` package, users relying on this server (such as VsCoq < XX) must install it"
Karl Palmskog (Sep 27 2022 at 11:23):I think one should discuss the "semantics" of the coq package in some Coq WG or similar. It's right now a joint responsibility between Coq core team and volunteers. For example:
Karl Palmskog (Sep 27 2022 at 11:23):it seems like most of the install time of coq is taken up by compiling the Stdlib, so I think some people might not even want that
Karl Palmskog (Sep 27 2022 at 11:27):if we exclude coqide-server from coq, I think this should be done for 8.18 and be coordinated with CoqIDE and VsCoq maintainers. They could add an error message like:
coqidetop not found. If you are using opam, please install the coqide-server package
The issue is that the coq-stdlib split is not a very good one. It really should be stdlib and a prelude since much of Coq doesn't even work without the prelude being present in some form. We don't have a well-defined prelude since some plugins are loaded outside of the prelude etc. but then plugins are in coq-core...
Ali Caglayan (Sep 27 2022 at 11:41):We need to sit down together and sort out what goes where at some point.
Ali Caglayan (Sep 27 2022 at 11:41):I'm in favour of breaking up the stdlib into smaller pieces that people can pick and choose as they please.
Gaëtan Gilbert (Sep 27 2022 at 11:41):the prelude seems pretty well defined to me? it's the stuff in init/
Ali Caglayan (Sep 27 2022 at 11:42):Yes but then things like program and extraction are not there.
Gaëtan Gilbert (Sep 27 2022 at 11:42):so?
Ali Caglayan (Sep 27 2022 at 11:42):Those plugins are included in coq-core
Ali Caglayan (Sep 27 2022 at 11:43):For me, prelude should be the minimal possible .v file setup needed to run Coq (all features in coq-core)
Karl Palmskog (Sep 27 2022 at 11:43):it's a bit annoying if something technically part of coq-core can't be used without installing the whole stdlib
Ali Caglayan (Sep 27 2022 at 11:44):Agda for instance has a separate stdlib and a builtins that gets shipped with the core agda package.
Ali Caglayan (Sep 27 2022 at 11:45):I believe it is the same case for lean too, but it has been a while since I have checked.
Ali Caglayan (Sep 27 2022 at 11:45):The main advantage being to avoid what Karl described
Gaëtan Gilbert (Sep 27 2022 at 11:47):for me prelude is just the autoloaded stuff
Declare ML Module works fine for extraction & co
and I really want to have all the ml stuff still in coq-core so that I can dune build it without missing random plugins (so eg I don't want to put ltac2 in a separate package)
Matthieu Sozeau (Sep 27 2022 at 11:52):@Karl Palmskog I've added a point on the subject to the Coq Call, it seems our viewpoints are different on the purpose of the coq opam package indeed
Karl Palmskog (Sep 27 2022 at 11:53):@Matthieu Sozeau OK, I will try to participate in the call on this, thanks.
Karl Palmskog (Sep 27 2022 at 13:25):and while we are thinking of opam packages, it's not obvious that coqide should depend directly on coq, since people who may not want the stdlib could still use coqide.
Théo Zimmermann (Sep 27 2022 at 16:02):Indeed, coq is just a compat layer, so it's not even clear that any package for Coq >= 8.17 should depend on it (why not directly depend on coq-core + coq-stdlib or whatever else you precisely need?).
Last updated: Oct 13 2024 at 01:02 UTC