Merge pull request #227 from coq/update-ui-list

Most needed changes to Coq's UI page.

pages/user-interfaces.html

@@ -28,36 +28,19 @@
 mode <a href="https://proofgeneral.github.io/">Proof General</a>, that
 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.
 </li>
 
 <li>
-<strong>Vim/NeoVim</strong> users can use the actively
-maintained <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>.
+<strong>Vim/NeoVim</strong> users can use the <a href="https://github.com/whonore/Coqtail">Coqtail</a>
+extension.  NeoVim users can also test the experimental support for
+<a href="https://github.com/tomtomjhj/vscoq.nvim">VsCoq's vscoqtop server</a>
+or for <a href="https://github.com/tomtomjhj/coq-lsp.nvim">coq-lsp</a>.
 </li>
 
 </ul>
 
 </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.
-</p>
-
 </div>
 
 <div class="frameworklinks">
@@ -77,23 +60,13 @@
 <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).
+a standalone desktop application which is developed and distributed alongside Coq.
 </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.
+entirely in your browser.
 </p>
 
 </div>
@@ -117,6 +90,11 @@
 uncertain:
 <ul>
 <li>
+A <a href="https://github.com/EugeneLoy/coq_jupyter/">Jupyter kernel for Coq</a>
+(supports Coq 8.6 and newer versions using <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="http://coqoon.github.io/">Coqoon</a> Eclipse plugin was
 initially based upon
 the <a href="https://bitbucket.org/coqpide/pidetop/src/PIDEtop/">PIDEtop