Stream: Coq devs & plugin devs

Topic: coq.dev opam package not producing coqidetop.opt?


view this post on Zulip 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...

view this post on Zulip Matthieu Sozeau (Sep 14 2022 at 15:35):

Meaning, my vscoq can't work

view this post on Zulip Gaëtan Gilbert (Sep 14 2022 at 15:44):

it's in coqide-server not coq-core

view this post on Zulip Matthieu Sozeau (Sep 14 2022 at 15:45):

Hmm, ok

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Sep 14 2022 at 15:48):

So I don't have a coqide-server package...

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Sep 14 2022 at 16:12):

sadly no, I'm too swamped to follow opam in these weeks

view this post on Zulip Théo Zimmermann (Sep 14 2022 at 16:12):

Indeed, the package is missing and should be added.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Sep 14 2022 at 16:18):

define "package". Do you mean there should be a separate coqidetop.dev package?

view this post on Zulip Matthieu Sozeau (Sep 14 2022 at 16:19):

A coqide-server package I guess, as it used to be?

view this post on Zulip Karl Palmskog (Sep 14 2022 at 16:19):

I can confirm that coqidetop.opt gets installed with 8.16.0 at least.

view this post on Zulip Matthieu Sozeau (Sep 14 2022 at 16:21):

That's strange that nobody noticed this before, maybe the coqide target installed coqidetop.opt anyway?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Sep 14 2022 at 16:25):

I suspect a strong correlation between coq.dev usage and Emacs

view this post on Zulip Gaëtan Gilbert (Sep 14 2022 at 16:29):

cc @Emilio Jesús Gallego Arias

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2022 at 11:21):

Yes, indeed we forgot about the coqide-server package

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2022 at 11:21):

sorry about hat

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2022 at 11:21):

that

view this post on Zulip Théo Zimmermann (Sep 15 2022 at 11:24):

Matthieu opened a PR adding it.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Sep 17 2022 at 11:58):

that's not what happens tho

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Sep 17 2022 at 12:05):

yeah, I hope that one is an issue with autogeneration, and not a conscious decision?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Sep 17 2022 at 12:11):

Good question, but at least coqide-server did not exist for long.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Sep 17 2022 at 12:12):

ah, so a Coq Call question. That escalated quickly

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Sep 17 2022 at 12:16):

and .dev should eventually align as well... To automate releases/updates via dune-release, upgrades, etc

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Guillaume Melquiond (Sep 17 2022 at 12:43):

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.

view this post on Zulip Karl Palmskog (Sep 17 2022 at 12:45):

OK, that sounds to me like a bug in ide/coqide/dune... Should we report it?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Sep 17 2022 at 17:11):

And that also matches the old setup, right?

view this post on Zulip Karl Palmskog (Sep 17 2022 at 17:13):

it seems you get coqidetop through coq for 8.16, yes.

view this post on Zulip 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" }
]

view this post on Zulip Paolo Giarrusso (Sep 18 2022 at 12:52):

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.

view this post on Zulip 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).

view this post on Zulip 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)

view this post on Zulip Guillaume Melquiond (Sep 18 2022 at 13:30):

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))

view this post on Zulip Karl Palmskog (Sep 18 2022 at 13:31):

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...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Sep 18 2022 at 19:29):

Ah, two misunderstandings:

  1. I wasn't asking for a rationale — I thought you were disagreeing on how dune behaved.

view this post on Zulip Paolo Giarrusso (Sep 18 2022 at 19:54):

  1. All I'm asking about dune is, how should it know which opam package contains findlib library lablgtk3-sourceview3 when that library isn't installed? Here they match, but it could also come from opam package toto-tata, no?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Sep 20 2022 at 06:21):

Somehow the commit hash should be part of the version I guess

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Sep 20 2022 at 07:32):

Ok, I’ll try that

view this post on Zulip Karl Palmskog (Sep 27 2022 at 09:16):

The following tasks were carried out:

However, 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?

view this post on Zulip Matthieu Sozeau (Sep 27 2022 at 09:25):

I believe coq should depend on coqide-server indeed

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Sep 27 2022 at 09:49):

https://github.com/coq/coq/pull/16549

view this post on Zulip Karl Palmskog (Sep 27 2022 at 09:50):

is a changelog entry even needed for this?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2022 at 11:05):

It seems sensible to me that coqide would depend on coqide-server no?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2022 at 11:06):

in particular help users not to install things they don't need

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2022 at 11:07):

Not a big deal either way

view this post on Zulip 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"

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Sep 27 2022 at 11:40):

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...

view this post on Zulip Ali Caglayan (Sep 27 2022 at 11:41):

We need to sit down together and sort out what goes where at some point.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Sep 27 2022 at 11:41):

the prelude seems pretty well defined to me? it's the stuff in init/

view this post on Zulip Ali Caglayan (Sep 27 2022 at 11:42):

Yes but then things like program and extraction are not there.

view this post on Zulip Gaëtan Gilbert (Sep 27 2022 at 11:42):

so?

view this post on Zulip Ali Caglayan (Sep 27 2022 at 11:42):

Those plugins are included in coq-core

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Sep 27 2022 at 11:45):

The main advantage being to avoid what Karl described

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Sep 27 2022 at 11:53):

@Matthieu Sozeau OK, I will try to participate in the call on this, thanks.

view this post on Zulip 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.

view this post on Zulip 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: Feb 01 2023 at 14:03 UTC