Andrew Appel (Jun 20 2023 at 13:23): Andrew Appel (Jun 20 2023 at 13:23):The coq web site, under "user interfaces", lists several IDEs for Coq, but not a single one of them is actually supported and fully usable. Can any one recommend what IDE I should use, if at the same time I want to use the Coq Platform?
Here are the listed ones, with their limitations:
So I have two (related) questions, really:
Gaëtan Gilbert (Jun 20 2023 at 13:25):
- Proof General: "Unfortunately, this branch is mostly unmaintained and quite unstable."
That's about "Proof General also has an experimental async branch" so don't use the async branch
Gaëtan Gilbert (Jun 20 2023 at 13:26):and vscoq1 still works fine AFAIK
Théo Zimmermann (Jun 20 2023 at 13:54):I guess we should just fix the user-interface page to point to https://github.com/coq-community/vscoq/tree/vscoq1 instead of https://github.com/coq-community/vscoq for VsCoq.
Théo Zimmermann (Jun 20 2023 at 13:56):@Andrew Appel I wonder though, is it on purpose that you are trying to make it sound worse than it actually is by pointing to issues with experimental or discontinued branches, by overinterpreting CEP#68, etc., or is this what users really perceive when looking at this page?
Andrew Appel (Jun 20 2023 at 14:06):I'm not trying to make it sound worse than it is. I am a Coq user, just trying to figure out from the Coq documentation what IDE to use. I have been using CoqIDE for many years, and would be happy to continue using it. But after switching to an M2 Mac, on which CoqIDE is quite unreliable, I honestly don't know what to do, and the Coq documentation on the main web site is not helpful. I suppose I should use Proof General; my colleague down the hall with an M1 Mac uses Proof General. But the Coq web site is a bit confusing on that point.
Andrew Appel (Jun 20 2023 at 14:08):As for "overinterpreting CEP#68", how should I interpret that? There are two serious bug reports about CoqIDE, and the only "response" is CEP#68. If it is likely that CoqIDE will be fixed in 8.17.1, that would make me very happy, but the only way I can interpret CEP#68 is that this is unlikely. Am I wrong?
Andrew Appel (Jun 20 2023 at 14:10):From @Théo Zimmermann 's response, I learn that perhaps I should use vscoq1 instead.
Théo Zimmermann (Jun 20 2023 at 14:14):Andrew Appel said:
As for "overinterpreting CEP#68", how should I interpret that? There are two serious bug reports about CoqIDE, and the only "response" is CEP#68. If it is likely that CoqIDE will be fixed in 8.17.1, that would make me very happy, but the only way I can interpret CEP#68 is that this is unlikely. Am I wrong?
CEP#68 is not a response to these bug reports, but rather a response to pull requests like https://github.com/coq/coq/pull/17421, which try to add new features to CoqIDE. Core devs are not ready to spend more time supporting new features in CoqIDE. That's what CEP#68 means. Bugs, and especially major bugs and regressions, should still be addressed until CoqIDE is retired (which won't happen for a while). The fact that these two bugs were not addressed yet doesn't mean that we think they are not worth being addressed.
Théo Zimmermann (Jun 20 2023 at 14:20):The main issue with CoqIDE bugs that are specific to macOS is that we are short in people who have the required hardware to reproduce and debug them.
Pierre Courtieu (Jun 20 2023 at 14:37):"ProofGeneral async" should be removed from the site imho, it has never been released.
Théo Zimmermann (Jun 20 2023 at 14:47):OK, if you open a PR doing so, I will merge it. Otherwise, I will prepare a more significant update to this webpage (but probably not before the CUDW).
Théo Winterhalter (Jun 20 2023 at 14:51):I think on macOS vscoq1 is by far the best option. I use it on a daily basis, and never looked back to ProofGeneral.
Benjamin Pierce (Jun 20 2023 at 15:06):A variant of Andrew's question: In early August, I plan to release a new version of the Software Foundations series, updated to recommend the latest Coq version and GUI. My understanding is that VSCoq2 _might_ be fully released by then, but whatever GUI is recommended also needs to be very easy to install along with the rest of Coq...
Théo Zimmermann (Jun 20 2023 at 15:10):VsCoq2 will become easy to install once it is shipped in the Coq Platform. This is planned, but it won't happen in time for early August I think, given the delay that we have seen for the release of a Coq 8.17-based Platform (mostly due to infrastructure and system dependencies).
Andrew Appel (Jun 20 2023 at 15:16):Théo Winterhalter said:
I think on macOS vscoq1 is by far the best option. I use it on a daily basis, and never looked back to ProofGeneral.
Thank you. I've installed vscode (took 1 minute), installed vscoq1 (took less than 1 minute), and it's working already.
Benjamin Pierce (Jun 20 2023 at 15:21):Thanks, Théo -- I'll recommend vscoq1, then, but include a note to watch for the vscoq2 release at some point.
Karl Palmskog (Jun 20 2023 at 15:23):from what I understand of VsCoq2 development, it's only going to be officially usable in Coq 8.18.0. And this means that even with the next Platform release, 8.18.0 will not be included there, so VsCoq2+Platform will only come with the subsequent Platform release in 2024.
Karl Palmskog (Jun 20 2023 at 15:26):with that said, I think this is why we wanted and pushed for interim maintenance of VsCoq1. It's unfortunate some intended links for VsCoq1 are going to VsCoq2 now (I will have to address this in Awesome Coq as well).
Bhakti Shah (Jun 20 2023 at 16:22):I would add that I’ve worked on fairly large projects in the last ~6 months using both vscoq1 and coq-lsp (on 8.16), and the user experience has been pretty good in both cases, though lsp has some caveats for the setup which are in the readme, and vscoq1 is a bit buggy with the recommended prettify-symbols-mode
Emilio Jesús Gallego Arias (Jun 20 2023 at 17:44):coq-lsp should work pretty well with software foundations, and moreover can support coqdoc/markdown natively which can be pretty useful to students. Moreover it will be deployed as a fully working web extension too.
There is a bit of backlog in solving the last key features before we consider coq-lsp "1.0" ready, but fortunately we found a solution for all of them, so I expect the next release to do well in that sense.
Emilio Jesús Gallego Arias (Jun 20 2023 at 17:50):Also it was a bit by chance, but coq-lsp works very well on native windows
Karl Palmskog (Jun 20 2023 at 19:13):vcs-prettify-symbols-mode is unmaintained, we didn't manage to find a maintainer (https://github.com/coq-community/manifesto/issues/130). So I suppose it shouldn't be recommended.
Maxime Dénès (Jun 24 2023 at 18:54):Karl Palmskog said:
from what I understand of VsCoq2 development, it's only going to be officially usable in Coq 8.18.0. And this means that even with the next Platform release, 8.18.0 will not be included there, so VsCoq2+Platform will only come with the subsequent Platform release in 2024.
8.18.0 is not going to be included in a platform release in 2023?
Karl Palmskog (Jun 24 2023 at 19:11):the Platform release for 8.17 will likely be in July or August. If you look at interval times between Platform releases in the past, I don't see a new Platform release happening until about 6 months after that, and v8.18 hasn't happened yet
Karl Palmskog (Jun 24 2023 at 19:14):let's say 8.18+rc1 comes in late August or September. The whole release process for Platform packages will typically take 2-3 months.
Karl Palmskog (Jun 24 2023 at 19:34):the Platform is at this point a part-time engagement for 1+3 people, all with other high-pressure "distractions". Lowering lead times is possible, but the only way I could see a significant speedup of Platform release processes is with dedicated engineer time.
Hugo Herbelin (Jun 26 2023 at 12:39):Regarding an update of the user interface page on the web site, I now published a few comments I wrote a few months ago. I volunteer to make a new version of the page.
Hugo Herbelin (Jun 26 2023 at 12:39):Regarding what to recommend, my experience with vscode is that:
Hugo Herbelin (Jun 26 2023 at 12:39):Comparatively, coqide is based: on gtk+3 which has a smaller community, on lablgtk which has an even smaller community; moreover, even among OCaml people, gtk+3 is somehow considered as old-fashioned compared to web-technology-based rendering of vscode (from what I understand). So, in the long term, I don't see how coqide could really be pushed further.
Hugo Herbelin (Jun 26 2023 at 12:40):Renouncing to coqide does not mean renouncing to the nice features that have been already implemented in Coqide. One of the key point for the future in my opinion is to have a modular approach to GUIs. It does not make sense to talk about vscoq1, vscoq2, coqide, coq-lsp as independent GUIs. In my opinion, what is important is to think in terms of components and features. A server (over LSP) is defined by the set of features it provides (highlighting, searching, returning type information, expanding notations, ...). A client (over LSP) is defined by the set of graphical access to features it provides. LSP is even not strictly necessary if we can be modular enough., that is if we think in terms of graphical features, semantic features, communication protocol.
Hugo Herbelin (Jun 26 2023 at 12:40):Regarding vscoq2 vs coq-lsp, they have to be seen as part of a mutual emulation, not as a competition internal to the Coq development team. My 2p is that they should eventually share API.
Last updated: Oct 13 2024 at 01:02 UTC