Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Proposal for updating the user interfaces page. #218

Closed
wants to merge 14 commits into from
Closed

Proposal for updating the user interfaces page. #218

Changes from 12 commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
4523e2e
June 2023 update of the user interfaces page.
herbelin Jun 30, 2023
c3e4177
Update pages/user-interfaces.html
herbelin Jun 30, 2023
7557336
Update pages/user-interfaces.html
herbelin Jun 30, 2023
962ea83
Update pages/user-interfaces.html
herbelin Jun 30, 2023
b28b5b2
Update links
herbelin Jun 30, 2023
609751c
Update pages/user-interfaces.html
herbelin Jul 1, 2023
5c34c5b
Update pages/user-interfaces.html
herbelin Jul 1, 2023
72a92f0
Update pages/user-interfaces.html
herbelin Jul 1, 2023
2a12266
Update status PG mode in coq-lsp and vscoq2.
herbelin Jul 1, 2023
eb6a8c9
Shorten description of CoqIDE.
herbelin Jul 1, 2023
cdca7c8
Remove useless ... in selected list of experimental/historical UIs.
herbelin Jul 1, 2023
0a945b7
stand-alone -> standalone
herbelin Jul 1, 2023
1cdf2bb
Update pages/user-interfaces.html
herbelin Jul 1, 2023
3390eaf
Update pages/user-interfaces.html
herbelin Jul 1, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
145 changes: 75 additions & 70 deletions pages/user-interfaces.html
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,32 +2,21 @@
<#include "incl/header.html">

<div class="framework">
<div class="frameworklabel">Editor-support packages</div>
<div class="frameworklabel">Most popular user interfaces</div>
<div class="frameworkcontent">

<p>
Coq projects can be developed with a variety of editors thanks to
Coq projects can be developed with a variety of <strong>editors</strong> thanks to
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The whole wording of this paragraph sounds bizarre to me

great support provided through user-contributed extensions. Here, we
list such support extensions that are actively used and maintained:
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The below can be hardly called "extensions" IMHO.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As I wrote below it does refer to the particular way Coq support is implemented, so that's an unecessary technical detail to the user here. We could use instead "editor support for Coq"

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, I now understand what you mean! I think this is because we understand "user-contributed extensions" differently. You think of extensions to Coq while I think of extensions to editors (and I don't know what Hugo had in mind). We could change this to say "user-contributed editor support packages" to clarify.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes I prefer that. For example in the emacs world people don't talk about extensions but about "modes", so I was trying to find out a more common terminology.


<ul>

<li>
<strong>Visual Studio Code</strong> and <strong>VSCodium</strong> users can use either of
the <a href="https://github.com/coq-community/vscoq">VsCoq
extension</a>, which is actively maintained by several contributors as part
of <a href="https://github.com/coq-community/manifesto">coq-community</a>, or
the new <a href="https://github.com/ejgallego/coq-lsp">coq-lsp extension</a>,
which is based on an implementation of the <a
href="https://microsoft.github.io/language-server-protocol">Language
Server Protocol</a> standard, with custom extensions.

<tt>coq-lsp</tt> provides continous document checking and position-based
document navigation (an interaction model similar to what is found in e.g.,
Lean, and which departs from the model found in other Coq user interfaces).
See <tt>coq-lsp's</tt> <a
href="https://github.com/ejgallego/coq-lsp/blob/main/etc/FAQ.md">FAQ</a>
for more information.
<strong>Visual Studio Code</strong> and <strong>VSCodium</strong> users can use
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is coq-lsp out of this list?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Because this first part is about "Most popular user interfaces": it is set to change in the future when LSP-based extensions become more prevalent.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Most popular seems like an strange notion, but if that's the criteria coq-lsp may have already more users than for example Coq + VIM already.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The title may not be the most accurate. The goal was to separate the extensions that we know have been used for years already, from the ones that are still new and experimental, but probably represent the future.

It's hard to tell how many users Coqtail has, but for what this is worth (not a lot), it has twice as many stars on GitHub (compared to coq-lsp) and it had about as many users in the Coq Community Survey 2022 as jsCoq (although jsCoq has many more stars on GitHub).

the <a href="https://github.com/coq-community/vscoq/tree/vscoq1">VsCoq 1
extension</a>, which is maintained by several contributors as part
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am not sure who maintains what is relevant in this page.

of <a href="https://github.com/coq-community/manifesto">coq-community</a>.
</li>

<li>
Expand All @@ -36,15 +25,14 @@
can be extended by the minor Coq
mode <a href="https://github.com/cpitclaudel/company-coq">Company-Coq</a>.
Proof General was one of the first user interface for proof
assistants, and is one of the most used user interface for Coq today.
Proof General and Company-Coq give access to many productivity
shortcuts, including auto-completion and documentation. On the other
hand, async proof processing is not supported.
assistants. See e.g.
<a href="https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General/">here</a>
for an excerpt of Coq-specific features.
</li>

<li>
<strong>Vim/NeoVim</strong> users can use the actively
maintained <a href="https://github.com/whonore/Coqtail">Coqtail</a>
<strong>Vim/NeoVim</strong> users can use the
<a href="https://github.com/whonore/Coqtail">Coqtail</a>
extension. This extension is partly based upon a previous, and now
unmaintained, Vim extension
called <a href="https://github.com/the-lambda-church/coquille">Coquille</a>.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

IMHO time to remove this info from here too.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Agreed.

Expand All @@ -55,102 +43,119 @@
</p>

<p>
An experimental alternative to the editors mentioned above is the
computational notebook interface provided by Jupyter.
A <a href="https://github.com/EugeneLoy/coq_jupyter/">Jupyter kernel
for Coq</a> is available if you want to try this interface, for
instance for pedagogical or readability purposes. One of the
advantages of using a Jupyter notebook is that you can save and
display a selection of intermediate proof steps, which your reader
will see without the need to reexecute the document.
Otherwise, <a href="https://coq.inria.fr/refman/practical-tools/coqide.html">CoqIDE</a> is
a <strong>standalone</strong> interface
developed and distributed alongside Coq.
</p>

<p>
As a way to try Coq without installing anything, you can also
use <a href="https://jscoq.github.io/">JsCoq</a> which loads Coq
entirely in <strong>your browser</strong>. However, it is limited to conduct
actual projects: e.g., it lacks access to the VM and native computing
herbelin marked this conversation as resolved.
Show resolved Hide resolved
machineries of Coq, and running in the browser is slower.
</p>

</div>

<div class="frameworklinks">
<ul>
<li><a class="extlink" href="https://github.com/coq-community/vscoq">VsCoq (VS Code)</a></li>
<li><a class="extlink" href="https://github.com/ejgallego/coq-lsp">coq-lsp (VS Code)</a></li>
<li><a class="extlink" href="https://proofgeneral.github.io/">Proof General (Emacs)</a></li>
<li><a class="extlink" href="https://github.com/whonore/Coqtail">Coqtail (Vim)</a></li>
<li><a class="extlink" href="https://github.com/coq-community/vscoq/tree/vscoq1">VsCoq 1</a></li>
<li><a class="extlink" href="https://proofgeneral.github.io/">Proof General</a></li>
<li><a class="extlink" href="https://github.com/whonore/Coqtail">Coqtail</a></li>
<li><a href="refman/practical-tools/coqide.html">CoqIDE</a></li>
<li><a class="extlink" href="https://jscoq.github.io/">JsCoq</a></li>
</ul>
</div>
</div>

<div class="framework">
<div class="frameworklabel">Standalone interfaces</div>
<div class="frameworklabel">Towards an LSP-based modular design of Coq user interfaces</div>
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is the point of this section? IMHO it is very confusing, see my full review for more concrete thoughts.

<div class="frameworkcontent">

<p>
Alternatively, you can
use <a href="https://coq.inria.fr/refman/practical-tools/coqide.html">CoqIDE</a>,
which is developed and distributed alongside Coq. CoqIDE relies
on <a href="https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md">Coq's
XML protocol for IDEs</a> and implements all of the features provided
by this protocol, meaning in particular asynchronous evaluation.
CoqIDE comes with standard basic Emacs-like bindings
and with some specific Coq-related bindings but, as an editor, it is
not as complete as a general-purpose editor could be (for instance it
does not have automatic indentation).
</p>

<p>
As a way to try Coq without installing anything, you can
use <a href="https://jscoq.github.io/">JsCoq</a>. JsCoq loads Coq
entirely in your browser. However, it is too limited to conduct
actual projects: it lacks access to the VM and native computing
machineries of Coq, and may hit out-of-memory and stack-overflow
failures quicker than native versions of Coq.
</p>

The <a href="https://microsoft.github.io/language-server-protocol">Language
Server Protocol</a> (LSP) is a standard protocol for interfacing
IDEs and programming language tools. Two interfaces, each composed of a VS Code
client and of a Coq server communicating over a proof-assistant-specific
extension of LSP are at an experimental stage of development:
<ul>
<li><a href="https://github.com/coq-community/vscoq">VsCoq 2</a></li>
<li><a href="https://github.com/ejgallego/coq-lsp">coq-lsp</a></li>
</ul>
herbelin marked this conversation as resolved.
Show resolved Hide resolved
<p>
Both servers provide the extra ability of continuous and asynchronous document
Copy link
Member

@ejgallego ejgallego Jul 3, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it is not the job of this page to compare the servers. Comparing options could be useful but that should be done in its own section and include other interfaces. Moreover keeping these comparisons accurate as the tools change is hard.

checking as well as position-based document navigation (an
interaction model introduced in Wenzel's Isabelle/JEdit which
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It might be worth mentioning that VsCoq2 also supports switching to a legacy-style mode of interaction if it doesn't make the text too long.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What about "Both provides the extra ability ..."? (In the case of coq-lsp, afaiu, the server supports evaluation to a chosen position but the client does not - yet? - give access to it.)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

IMO, what the users most care about is what is accessible for the client. But OK to me if you do not want to make a comparison here.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

IIUC, Emilio is not fully convincent that it is worth to support the PG mode and this is why the client is bridled. I temporarily wrote "Both servers provides the extra ability" until it is clear what is the intent of coq-lsp developers.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK for now, but if coq-lsp doesn't support the legacy mode on purpose, it will be important to make the distinction when we start to advertise these two options more.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I still don't see it. But I'm fine with the current state FWIW.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah OK, my mistake. I understand what you meant now.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK for now, but if coq-lsp doesn't support the legacy mode on purpose, it will be important to make the distinction when we start to advertise these two options more.

Technically coq-lsp does support checking to a point, and indeed it uses internally in an essential way (for example the way click to show goals works today is exactly like that)

The reason I didn't put an option for that is that 0 users do prefer the old mode, which has pretty bad latency properties. However there is a chicken and egg design problem here, in the sense that once you are used to the more eager mode, you never want to go back. Design in this sense should not work IMO by having the user do these choices. (Neither lean of isabelle allow that for example). If something, coq-lsp can read the power profile and be more eager / conservative, but always you want to do a bit of prefetching as Isabelle does, even in low power mode (which can the properly limited by the DM to have the right CPU / mem bounds)

Anyways we need a better setup for the start of the page than to expose all these very technical things IMHO.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The reason I didn't put an option for that is that 0 users do prefer the old mode

You are always criticizing others when they make claims without evidence or false claims, but then you come and make such strong claims yourself. Do I need to remind you that Clément said explicitly that he didn't like the new mode from his experience with other proof assistants that use it?

Copy link
Member

@ejgallego ejgallego Jul 4, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@Zimmi48 , I'm sorry to hear you think that me pointing out that a claim seems incorrect to me sounds like a critic; it is for sure not my intention to critizise (and not something I enjoy) but to point out that once I have reviewed what the code is doing I found different. I'd be happy to hear how could I do better in this sense.

In this case I have discussed with maybe a dozen users about their preferences, (and actually I'd love to run a true study on this), and none of the users did prefer the old mode, when we enabled it the bad latency alone makes a big impact on the usability (sample size here is N=3 tho, so again pretty low).

Note that I took Clément feedback into account, indeed you want to check less for example when you are in low power mode etc..., which IIUC that was a core problem he had with other systems. For example I understood that he'd be fine with the current hint Isabelle uses (and that is planned, but requires a bit more work on the core engine)

I was just trying to clarify, based on what Hugo had asked me in person, what was the status of such a feature in coq-lsp and why we didn't put an option to that. If there is interest in having such a mode I'm happy to add and option to enable it as it is only a one-line change in the engine (as I pointed out to Hugo in person)

departs from the model of splitting the buffer into a validated zone
and an unvalidated zone, as found in other Coq user interfaces; see
e.g. this <a href="https://github.com/ejgallego/coq-lsp/blob/main/etc/FAQ.md">FAQ</a>
for more information, where in the text, "coq-lsp" should be read as
"coq-lsp or VsCoq 2" and "VsCoq" should be read as "VsCoq 1").
</p>
<p>
The features provided by the two servers are available to any
editor implementing the protocol, e.g. Emacs, Vim, jsCoq, or even another
VS Code client. In turn, any new feature eventually added to the
servers becomes available for integration by their clients.
</p>
</div>

<div class="frameworklinks">
<ul>
<li><a href="refman/practical-tools/coqide.html">CoqIDE</a></li>
<li><a class="extlink" href="https://jscoq.github.io/">JsCoq</a></li>
<li><a class="extlink" href="https://github.com/coq-community/vscoq/tree/vscoq1">VsCoq 2</a></li>
<li><a class="extlink" href="https://github.com/coq-community/vscoq/tree/vscoq1">coq-lsp</a></li>
</ul>
</div>
</div>

<div class="framework">
<div class="frameworklabel">Experimental / discontinued interfaces</div>
<div class="frameworklabel">A selected list of experimental or historical interfaces</div>
<div class="frameworkcontent">

<p>
There have been many experiments over the years. Here are some
Here are some
additional user interfaces that have stayed at the experimental level
or whose maintenance has been discontinued and or is currently
or whose maintenance has either been discontinued or is currently
uncertain:
<ul>
<li> A <a href="https://github.com/EugeneLoy/coq_jupyter/">Jupyter kernel
for Coq</a> is available if you want to try this interface, for
instance for pedagogical or readability purposes. One of the
advantages of using a Jupyter notebook is that you can save and
display a selection of intermediate proof steps, which your reader
will see without the need to reexecute the document.
</li>
<li>
The <a href="http://coqoon.github.io/">Coqoon</a> Eclipse plugin was
initially based upon
the <a href="https://bitbucket.org/coqpide/pidetop/src/PIDEtop/">PIDEtop
the discontinued <a href="https://bitbucket.org/coqpide/pidetop/src/PIDEtop/">PIDEtop
Coq plugin</a> (following Wenzel's asynchronous PIDE framework).
Support for more recent versions of Coq (8.7 and 8.8) relies
on <a href="https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md">Coq's
XML protocol for IDEs</a>.
</li>
<li>
The <a href="https://github.com/Ptival/PeaCoq">PeaCoq</a> online web
interface for Coq was focused on teaching (actively developed from
2014 to 2016).
</li>
<li>
The <a href="http://prover.cs.ru.nl">ProofWeb</a> online web interface
The <a href="http://carol.dimap.ufrn.br/proofweb">ProofWeb</a> online web interface
for Coq (and other proof assistants) was also focused on teaching (in
2006-2007).
</li>
<li>
<a href="http://provereditor.gforge.inria.fr">ProverEditor</a> was an
<a href="http://www-sop.inria.fr/everest/Julien.Charles/papers/08-08-08-uitp.pdf">ProverEditor</a> was an
experimental Eclipse plugin with support for Coq (in 2005-2006).
</li>
<li>
<a href="https://www-sop.inria.fr/lemme/pcoq/">Pcoq</a> (discontinued
in 2003) was a first experiment at <a href="https://www-sop.inria.fr/croap/ctcoq/help/pbp.html">proof-by-pointing</a>.
</li>
</ul>
</p>
<p>
Learn more on the <a href="https://github.com/coq/coq/wiki/Basic-architecture-of-Coq-User-Interfaces">design of Coq user interfaces</a>, or contribute to <a href="https://github.com/coq/coq/wiki/GUIWishes">Coq UI wishes</a>.
</p>

</div>
</div>

</div>
</div>
Expand Down