Create a page dedicated to user interfaces.

[Zimmi48]

• Try to list all significant user interfaces, including discontinued ones.

• Organize this page in three categories: support extensions, standalone interfaces, and experimental / discontinued interfaces.

• Remove the user interface section from the Related Tools page.

• Mention prominently the User interfaces page on the index page.

Fix #123.

[Zimmi48]

cc @erikmd @Matafou @cpitclaudel @whonore @maximedenes @EugeneLoy @herbelin @ppedrot @gares @ejgallego @ale-f @Ptival @ybertot

Let me know if you have suggestion how to better describe your work.

Note that I have also created a Gitter chat room today (https://gitter.im/coq/user-interfaces) in the hope to foster discussions among user interface authors / maintainers and with Coq developers.

[Zimmi48]

For the record, and in order to avoid you from finding out how to compile the website, here is how this new page looks:

[maximedenes]

I like the idea of refreshing this page.

[Zimmi48]

The choice to mention the protocol used to communicate with Coq was mainly intended to provide an overview of the technology these different packages rely on, which might not be useful to users, but could be to author extension authors and to Coq developers. It also reflects how "modern" the extension is.

[Zimmi48]

It turns out that we actually have two actively maintained Vim extensions: Coqtail, and this fork of Coquille. I am of course bound to include both on this page. If anyone (@roptat, @whonore?) can tell me of any differences that could help to distinguish them, that would be helpful. Furthermore, how far apart are they both from each other? Is there any hope of having a single extension in the future? If it can help, coq-community could host such merger.

[cpitclaudel]

Neat, though I think the PG XML branch should move to the experimental / discontinued section. Also, it might help to mention distinguishing features (async editing in CoqIDE, completion and documentation in PG+Company-coq, etc.)

[whonore]

I haven't actually tried @roptat's fork but from glancing over the code it seems one of the biggest differences is that it is written as a Neovim plugin and so won't work on Vim. Coqtail currently only works for Vim although I do plan to support Neovim too when I eventually get around to it (whonore/Coqtail#13). There are some other differences in the interfaces but the basic features seem similar otherwise. But I think due to the difference in editor support it would be difficult to merge them as they are now.

[roptat]

I think we both have the same basic features, since we are both based on the same software initially :). I can't talk about coqtail, but here are some differences with the original coquille: it supports multiple versions of coq (8.6 -> 8.10), multithreading (you can navigate the file or do other operations while coq is busy, you can interrupt evaluation of a statement when it doesn't finish, and I think it's slightly faster than the original coquille too: with coqtocursor, I can start evaluation while parsing the file), and multiple sessions per nvim window (you can start coq in different buffers or tabs).

[Matafou]

I too find that it is a good idea to refresh this page, but wouldn't it be better to point to some page in coqwiki instead? This informations are likely to become outdated every now and then anyway.

By the way, is PG still the only IDE providing automatic indentation?

[maximedenes]

By the way, is PG still the only IDE providing automatic indentation?

I don't know how powerful PG's automatic indentation is, but VsCoq has a bit of it.

[whonore]

Coqtail and Coquille also support automatic indentation.

[Zimmi48]

I too find that it is a good idea to refresh this page, but wouldn't it be better to point to some page in coqwiki instead? This informations are likely to become outdated every now and then anyway.

Pointing to a wiki page or having a dedicated page on the official website does not convey the same meaning to the users, I think. I feel like having such a user interface page, and linking to it prominently from the front page sends a strong signal that we value the importance of user interfaces and the work of their authors / maintainers.

Note that wiki pages do get outdated much the same, and whereas it is indeed simpler to modify a wiki page, it is still quite easy to open a pull request to fix a page from the Coq website (maybe we should start adding direct links much like in the Sphinx reference manual).

I have some trouble understanding what Maxime and you mean by "refreshing this page" given that I'm creating a new page here. I'm refreshing some information initially found on the Related Tools page though, a page which, BTW, has been barely maintained over the years, and might be better suited as a simple wiki page since you mention the possibility.

[herbelin]

Hi, a few comments in passing:

I'm refreshing some information initially found on the Related Tools page though, a page which, BTW, has been barely maintained over the years

I can only support this. (In particular, in the years 2014-16, I tried to sollicitate some younger people to be active at maintaining the web site and I failed miserably.)

it supports multiple versions of coq (8.6 -> 8.10), multithreading (you can navigate the file or do other operations while coq is busy, you can interrupt evaluation of a statement when it doesn't finish, and I think it's slightly faster than the original coquille too: with coqtocursor, I can start evaluation while parsing the file), and multiple sessions per nvim window (you can start coq in different buffers or tabs).

... automatic indentation ...

I think that such a list of features is the kind of information that a page on graphical user interfaces should give. I don't think that interfaces can be reduced to what are the underlying communication technology (textual, XML, LSP, serapi, ...), graphical engine (html technologies, gtk+, ...) and host graphical interface (emacs, vim, vscode, ...) they rely on (even if it has indeed an impact on how easy it is to then implement various concrete features).

[Zimmi48]

Sorry for the time it took me to take the comments into account and update this PR. I'll leave a few more days before merging this in case someone wants to make further comments. Note that I tried mentioning a few features (and less the technology on which these user interfaces rely) but I cannot do much more given that I have no experience with most of these interfaces. This can be further refined by someone else after this PR is merged (or this could be done as a table in a wiki page).

[herbelin]

Sorry, I failed to pay attention that it was already merged. Do you want me to propose a patch?

[Zimmi48]

@herbelin I agree with everything you propose, and I don't think it is especially controversial, so I think you can just push a commit directly. If you prefer to leave time for feedback, you can also open a PR.

[herbelin]

I directly pushed the above suggestions as you suggested. However, I have more suggestions.

What do you think about changing:

"If you don't want to use any of the previously mentioned editors, you can use CoqIDE, which is developed and distributed alongside Coq. Like most of the more modern editor extensions, CoqIDE relies on Coq's XML protocol for IDEs, and implements all of the features provided by this protocol."

into:

"Alternatively, you can use CoqIDE, which is developed and distributed alongside Coq. CoqIDE relies on Coq's XML protocol for IDEs, and implements all of the features provided by this protocol, meaning in particular asynchronous evaluation."

Unless there is a political wish to deprecate coqide, I believe the proposed alternative text is more factual.

Then, couldn't the paragraph on vscode be equally mentioning asynchronous evaluation, or add a "see features at https://github.com/whonore/Coqtail/blob/master/README.md"?

Also, if I understand correctly the status of the fork of Coquille, shouldn't the init page rather say something like "Proof General for Emacs, Coqtail/Coquille for Vim/Neovim, VsCoq for VSCode"?

[Zimmi48]

What do you think about changing:

"If you don't want to use any of the previously mentioned editors, you can use CoqIDE, which is developed and distributed alongside Coq. Like most of the more modern editor extensions, CoqIDE relies on Coq's XML protocol for IDEs, and implements all of the features provided by this protocol."

into:

"Alternatively, you can use CoqIDE, which is developed and distributed alongside Coq. CoqIDE relies on Coq's XML protocol for IDEs, and implements all of the features provided by this protocol, meaning in particular asynchronous evaluation."

Unless there is a political wish to deprecate coqide, I believe the proposed alternative text is more factual.

Yes, your proposal is better as it doesn't seem to implicitly contain a deprecation notice. There is no reason to wish to deprecate CoqIDE as long as it continues to get volunteer maintainers and it reasonably works (which is the case today). On the other hand, there was a will to better emphasize the great editor support that Coq already has, and in particular the VSCoq extension since it is very accessible, but I think this objective is already achieved by the ordering of the presentation.

Then, couldn't the paragraph on vscode be equally mentioning asynchronous evaluation, or add a "see features at https://github.com/whonore/Coqtail/blob/master/README.md"?

Just be careful not to make the descriptions too long. Regarding asynchronous evaluation, I've just indicated that PG doesn't support it because I wasn't clear which of the extensions relying on the XML protocol support it ATM.

Also, if I understand correctly the status of the fork of Coquille, shouldn't the init page rather say something like "Proof General for Emacs, Coqtail/Coquille for Vim/Neovim, VsCoq for VSCode"?

The goal on the homepage was to be quite short and was not to be exhaustive. The initial reason to make a list was just to avoid mentioning only CoqIDE on the homepage. That's why I didn't initially care about explaining which extension was for which editor. Now, we could indeed mention "Coquille" and "NeoVim" as well on the homepage, but what happens when we learn that there is a new extension for Atom, JEdit, SublimeText, etc.? Maybe the text on the homepage should already be simplified back to:

To use Coq, you will need a user interface. Many editor support extensions are available (for Emacs, Vim, VSCode, etc.), as well as CoqIDE, a standalone IDE for Coq. The User interfaces page provides a full list, with more details. [...]

[Matafou]

FTR I think the a sync branch of pg can be omitted since it never reached a usable state. P

Le sam. 18 janv. 2020 à 12:04, Théo Zimmermann notifications@github.com a écrit :

What do you think about changing:

"If you don't want to use any of the previously mentioned editors, you can use CoqIDE, which is developed and distributed alongside Coq. Like most of the more modern editor extensions, CoqIDE relies on Coq's XML protocol for IDEs, and implements all of the features provided by this protocol."

into:

"Alternatively, you can use CoqIDE, which is developed and distributed alongside Coq. CoqIDE relies on Coq's XML protocol for IDEs, and implements all of the features provided by this protocol, meaning in particular asynchronous evaluation."

Unless there is a political wish to deprecate coqide, I believe the proposed alternative text is more factual.

Yes, your proposal is better as it doesn't seem to implicitly contain a deprecation notice. There is no reason to wish to deprecate CoqIDE as long as it continues to get volunteer maintainers and it reasonably works (which is the case today). On the other hand, there was a will to better emphasize the great editor support that Coq already has, and in particular the VSCoq extension since it is very accessible, but I think this objective is already achieved by the ordering of the presentation.

Then, couldn't the paragraph on vscode be equally mentioning asynchronous evaluation, or add a "see features at https://github.com/whonore/Coqtail/blob/master/README.md"?

Just be careful not to make the descriptions too long. Regarding asynchronous evaluation, I've just indicated that PG doesn't support it because I wasn't clear which of the extensions relying on the XML protocol support it ATM.

Also, if I understand correctly the status of the fork of Coquille, shouldn't the init page rather say something like "Proof General for Emacs, Coqtail/Coquille for Vim/Neovim, VsCoq for VSCode"?

The goal on the homepage was to be quite short and was not to be exhaustive. The initial reason to make a list was just to avoid mentioning only CoqIDE on the homepage. That's why I didn't initially care about explaining which extension was for which editor. Now, we could indeed mention "Coquille" and "NeoVim" as well on the homepage, but what happens when we learn that there is a new extension for Atom, JEdit, SublimeText, etc.? Maybe the text on the homepage should already be simplified back to:

To use Coq, you will need a user interface. Many editor support extensions are available (for Emacs, Vim, VSCode, etc.), as well as CoqIDE, a standalone IDE for Coq. The User interfaces page provides a full list, with more details. [...]

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/coq/www/pull/128?email_source=notifications&email_token=ABFSL2SPAWTMZ7FYZA3TXW3Q6LO2DA5CNFSM4JBXBT2KYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEJJVZ3Q#issuecomment-575888622, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFSL2UVJQ6VXUHD4M4FWL3Q6LO2DANCNFSM4JBXBT2A .

[herbelin]

Yes, your proposal is better as it doesn't seem to implicitly contain a deprecation notice.

OK, I shall commit it.

Just be careful not to make the descriptions too long. Regarding asynchronous evaluation, I've just indicated that PG doesn't support it because I wasn't clear which of the extensions relying on the XML protocol support it ATM.

A way to make the VsCoq description shorter while highlighting the features could be:

"VsCode users can use the VsCoq extension initially authored by C.J. Bell and now actively maintained by Maxime Dénès as part of coq-community (see features)."

Or to have the name C.J. Bell only on the VsCoq page (I don't know what C.J. and Maxime would prefer).

Anyway, that's just a suggestion so that the descriptions are balanced. Staying with current vscode text is also ok.

Maybe the text on the homepage should already be simplified back to:

To use Coq, you will need a user interface. Many editor support extensions are available (for Emacs, Vim, VSCode, etc.), as well as CoqIDE, a standalone IDE for Coq. The User interfaces page provides a full list, with more details. [...]

Yes, looks very good.

By the way, which spelling to use, VsCode or VSCode? By consistency with VsCoq, VsCode looks nicer. On the other side, the web seems to say VSCode.

[maximedenes]

I agree with everything you propose, and I don't think it is especially controversial, so I think you can just push a commit directly.

I don't know whether it is this suggestion which lead to a commit being directly pushed to Coq's master (https://github.com/coq/coq/commit/927c683116c17a4746afdc4000ba2015591d3ba2), but I think the idea here was that we can be a bit more flexible for coq-www patches than for coq patches. Let's keep making PRs for all commits on Coq itself.

[herbelin]

Yes, I pushed directly on the suggestion of @zimmi48. Making PRs is good to me, and this is what I would prioritary recommend too. Of course, PRs also put some responsivity/responsibility constraints on sets of reviewers. This is far from an easy goal (e.g. I have 34 Coq PRs open, @ejgallego has 33), but this is certainly something we should reach, finding the good balance between time spend for coding and time spent for reviewing. Having pools of reviewers seems to improve things and we can certainly experiment yet more approaches...

What is your own view?

[maximedenes]

Yes, I pushed directly on the suggestion of @Zimmi48.

Again, I believe that @Zimmi48 suggested to push directly to this repository, not the Coq one. Is that correct, @Zimmi48 ?

My own view is that at least for the Coq repo, we should stay with the current status quo of no direct commit without a PR.

[herbelin]

Ah sorry for the misunderstanding, I thought you were talking about coq-www.

About coq/coq@927c683, I did not realize it was on the coq archive. I arrived to https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md from https://coq.inria.fr/user-interfaces.html without noticing it was a file from the archive (I did not check but implicitly thought that I was on the wiki). I'm surprised that online edition worked then. Isn't there a configuration problem?

[Are you ok with the modification? I can perfectly do a PR then]

[maximedenes]

I did not realize it was on the coq archive

That's what I thought, I was wondering due to a confusion with this PR. But I see what you say, it is more like a confusion with the wiki.

In any case, I'm ok with the change, so no special action to be taken, I just wanted to understand what had happened. It would be nice if we could disable direct editing of files in the coq repo (at least preventing to push directly such edits), but I don't know if GitHub has such a fine-grained setting.

[Zimmi48]

It would be nice if we could disable direct editing of files in the coq repo (at least preventing to push directly such edits), but I don't know if GitHub has such a fine-grained setting.

As was discussed privately with Maxime and Hugo, this could happen because branch protection is currently not enforced for admins (core devs). GitHub supports enforcing branch protection even for admins. I suggest discussing this at the next Coq Call.