From 4523e2e477b551c19b1f299e663f4f5d2a9ba027 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 30 Jun 2023 18:22:28 +0200 Subject: [PATCH 01/14] June 2023 update of the user interfaces page. --- pages/user-interfaces.html | 146 ++++++++++++++++++++----------------- 1 file changed, 79 insertions(+), 67 deletions(-) diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html index 5f10a226b0..eaa278dc6c 100644 --- a/pages/user-interfaces.html +++ b/pages/user-interfaces.html @@ -2,32 +2,21 @@ <#include "incl/header.html">
-
Editor-support packages
+
Most popular user interfaces

-Coq projects can be developed with a variety of editors thanks to +Coq projects can be developed with a variety of editors thanks to great support provided through user-contributed extensions. Here, we list such support extensions that are actively used and maintained:

  • -Visual Studio Code and VSCodium users can use either of -the VsCoq -extension, which is actively maintained by several contributors as part -of coq-community, or -the new coq-lsp extension, -which is based on an implementation of the Language -Server Protocol standard, with custom extensions. - -coq-lsp 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 coq-lsp's FAQ -for more information. + Visual Studio Code and VSCodium users can use + the VsCoq 1 +extension, which is maintained by several contributors as part + of coq-community.
  • @@ -36,15 +25,14 @@ can be extended by the minor Coq mode Company-Coq. 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. +here +for an excerpt of Coq-specific features.
  • -Vim/NeoVim users can use the actively -maintained Coqtail +Vim/NeoVim users can use the +Coqtail extension. This extension is partly based upon a previous, and now unmaintained, Vim extension called Coquille. @@ -55,82 +43,98 @@

    -An experimental alternative to the editors mentioned above is the -computational notebook interface provided by Jupyter. -A Jupyter kernel -for Coq 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, CoqIDE is +a stand-alone interface +developed and distributed alongside Coq. +CoqIDE comes with standard basic Emacs-like edition bindings +and with some specific Coq-related features (e.g. for searching, printing, debugging) but, as an editor, it is +not as complete as a general-purpose editor could be (for instance it +does not have automatic indentation). +

    + +

    +As a way to try Coq without installing anything, you can also +use JsCoq which loads Coq +entirely in your browser. However, it is limited to conduct +actual projects: e.g., it lacks access to the VM and native computing +machineries of Coq, and running in the browser is slower.

-
Standalone interfaces
+
Towards a modular design of Coq user interfaces based on the LSP protocol
- -

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

- -

-As a way to try Coq without installing anything, you can -use JsCoq. 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. -

- + The Language + Server Protocol (LSP) is a common protocol for user + interfaces. 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: + +

+ Both provides the ability of continuous and asynchronous document + checking as well as position-based document navigation (an + interaction model introduced in Wenzel's Isabelle/JEdit which + 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 FAQ + 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"). +

+

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

-
Experimental / discontinued interfaces
+
A selected list of experimental or historical interfaces

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

    +
  • A Jupyter kernel +for Coq 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. +
  • The Coqoon Eclipse plugin was initially based upon -the PIDEtop -Coq plugin (following Wenzel's asynchronous PIDE framework). -Support for more recent versions of Coq (8.7 and 8.8) relies -on Coq's -XML protocol for IDEs. +the discontinued PIDEtop +Coq plugin (following Wenzel's asynchronous PIDE framework and using the +Coq's +XML protocol for IDEs).
  • The PeaCoq online web @@ -149,8 +153,16 @@
  • Pcoq (discontinued in 2003) was a first experiment at proof-by-pointing. +
    • +
  • ...

+

+ Know more on the design of Coq user interfaces, or contribute to Coq UI wishes. +

+ +
+
From c3e4177b2b389bfc31244787517e82b9c64e54c0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 30 Jun 2023 20:29:51 +0200 Subject: [PATCH 02/14] Update pages/user-interfaces.html MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Théo Zimmermann --- pages/user-interfaces.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html index eaa278dc6c..cde3cbec9d 100644 --- a/pages/user-interfaces.html +++ b/pages/user-interfaces.html @@ -77,8 +77,8 @@
Towards a modular design of Coq user interfaces based on the LSP protocol
The Language - Server Protocol (LSP) is a common protocol for user - interfaces. Two interfaces, each composed of a VS Code + Server Protocol (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:
    From 7557336401c4fd0d3a07a2293723cd3385a18d8f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 30 Jun 2023 20:37:06 +0200 Subject: [PATCH 03/14] Update pages/user-interfaces.html MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Théo Zimmermann --- pages/user-interfaces.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html index cde3cbec9d..40ed72db18 100644 --- a/pages/user-interfaces.html +++ b/pages/user-interfaces.html @@ -158,7 +158,7 @@

- Know more on the design of Coq user interfaces, or contribute to Coq UI wishes. + Learn more on the design of Coq user interfaces, or contribute to Coq UI wishes.

From 962ea839c4194a9533b6ffb6e5eabc4d0410ad66 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 30 Jun 2023 20:40:13 +0200 Subject: [PATCH 04/14] Update pages/user-interfaces.html MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Théo Zimmermann --- pages/user-interfaces.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html index 40ed72db18..1c14439cd6 100644 --- a/pages/user-interfaces.html +++ b/pages/user-interfaces.html @@ -86,7 +86,7 @@
  • coq-lsp

    • - Both provides the ability of continuous and asynchronous document + Both provide the ability of continuous and asynchronous document checking as well as position-based document navigation (an interaction model introduced in Wenzel's Isabelle/JEdit which departs from the model of splitting the buffer into a validated zone From b28b5b218f96fcf99edaefdc6298d541ed3eb1e6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 30 Jun 2023 20:43:14 +0200 Subject: [PATCH 05/14] Update links --- pages/user-interfaces.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html index 1c14439cd6..f835c88eb0 100644 --- a/pages/user-interfaces.html +++ b/pages/user-interfaces.html @@ -142,12 +142,12 @@ 2014 to 2016).

  • -The ProofWeb online web interface +The ProofWeb online web interface for Coq (and other proof assistants) was also focused on teaching (in 2006-2007).
  • -ProverEditor was an +ProverEditor was an experimental Eclipse plugin with support for Coq (in 2005-2006).
  • From 609751c4672651aaeb1da39c90c509864a0bc645 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 1 Jul 2023 16:45:51 +0200 Subject: [PATCH 06/14] Update pages/user-interfaces.html MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Théo Zimmermann --- pages/user-interfaces.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html index f835c88eb0..86e58c3e3f 100644 --- a/pages/user-interfaces.html +++ b/pages/user-interfaces.html @@ -74,7 +74,7 @@
    -
    Towards a modular design of Coq user interfaces based on the LSP protocol
    +
    Towards an LSP-based modular design of Coq user interfaces
    The Language Server Protocol (LSP) is a standard protocol for interfacing From 5c34c5b50758558f6886bf0d27332617ba7b2058 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 1 Jul 2023 16:47:09 +0200 Subject: [PATCH 07/14] Update pages/user-interfaces.html MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Théo Zimmermann --- pages/user-interfaces.html | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html index 86e58c3e3f..98c9431e5c 100644 --- a/pages/user-interfaces.html +++ b/pages/user-interfaces.html @@ -132,9 +132,7 @@ The Coqoon Eclipse plugin was initially based upon the discontinued PIDEtop -Coq plugin (following Wenzel's asynchronous PIDE framework and using the -Coq's -XML protocol for IDEs). +Coq plugin (following Wenzel's asynchronous PIDE framework).
  • The PeaCoq online web From 72a92f02a1c135ef8e42e5528549f245ad082412 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 1 Jul 2023 17:03:20 +0200 Subject: [PATCH 08/14] Update pages/user-interfaces.html MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Théo Zimmermann --- pages/user-interfaces.html | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html index 98c9431e5c..fc733461b1 100644 --- a/pages/user-interfaces.html +++ b/pages/user-interfaces.html @@ -64,9 +64,9 @@
    From 2a122661b1acb28a49f0576c5ab6e7a85d9c25ea Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 1 Jul 2023 17:03:07 +0200 Subject: [PATCH 09/14] Update status PG mode in coq-lsp and vscoq2. --- pages/user-interfaces.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html index fc733461b1..b72eedb151 100644 --- a/pages/user-interfaces.html +++ b/pages/user-interfaces.html @@ -86,7 +86,7 @@
  • coq-lsp

    • - Both provide the ability of continuous and asynchronous document + Both servers provide the extra ability of continuous and asynchronous document checking as well as position-based document navigation (an interaction model introduced in Wenzel's Isabelle/JEdit which departs from the model of splitting the buffer into a validated zone From eb6a8c9c89943c2454d94f046410dd721bd0d7de Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 1 Jul 2023 17:04:19 +0200 Subject: [PATCH 10/14] Shorten description of CoqIDE. --- pages/user-interfaces.html | 4 ---- 1 file changed, 4 deletions(-) diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html index b72eedb151..db7731ec88 100644 --- a/pages/user-interfaces.html +++ b/pages/user-interfaces.html @@ -46,10 +46,6 @@ Otherwise, CoqIDE is a stand-alone interface developed and distributed alongside Coq. -CoqIDE comes with standard basic Emacs-like edition bindings -and with some specific Coq-related features (e.g. for searching, printing, debugging) but, as an editor, it is -not as complete as a general-purpose editor could be (for instance it -does not have automatic indentation).

    From cdca7c89159c72748fbf9b264da8187d6d48b958 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 1 Jul 2023 17:05:59 +0200 Subject: [PATCH 11/14] Remove useless ... in selected list of experimental/historical UIs. --- pages/user-interfaces.html | 1 - 1 file changed, 1 deletion(-) diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html index db7731ec88..c468184b2a 100644 --- a/pages/user-interfaces.html +++ b/pages/user-interfaces.html @@ -148,7 +148,6 @@ Pcoq (discontinued in 2003) was a first experiment at proof-by-pointing. -

  • ...

    • From 0a945b7c34386bd714012ff352b27f46ef87add4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 1 Jul 2023 17:06:54 +0200 Subject: [PATCH 12/14] stand-alone -> standalone --- pages/user-interfaces.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html index c468184b2a..877535a8fe 100644 --- a/pages/user-interfaces.html +++ b/pages/user-interfaces.html @@ -44,7 +44,7 @@

    Otherwise, CoqIDE is -a stand-alone interface +a standalone interface developed and distributed alongside Coq.

    From 1cdf2bb14c4c30fde07e318d5f2eb1291412b74e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 1 Jul 2023 17:59:50 +0200 Subject: [PATCH 13/14] Update pages/user-interfaces.html MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Théo Zimmermann --- pages/user-interfaces.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html index 877535a8fe..61e2899b9c 100644 --- a/pages/user-interfaces.html +++ b/pages/user-interfaces.html @@ -52,7 +52,7 @@ As a way to try Coq without installing anything, you can also use JsCoq which loads Coq entirely in your browser. However, it is limited to conduct -actual projects: e.g., it lacks access to the VM and native computing +actual projects: it lacks access to the VM and native computing machineries of Coq, and running in the browser is slower.

    From 3390eaf34ebe11f2de089cc8b399a1f9ff8c137b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 1 Jul 2023 18:01:17 +0200 Subject: [PATCH 14/14] Update pages/user-interfaces.html MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Théo Zimmermann --- pages/user-interfaces.html | 2 ++ 1 file changed, 2 insertions(+) diff --git a/pages/user-interfaces.html b/pages/user-interfaces.html index 61e2899b9c..87750e7331 100644 --- a/pages/user-interfaces.html +++ b/pages/user-interfaces.html @@ -72,6 +72,7 @@
    Towards an LSP-based modular design of Coq user interfaces
    +

    The Language Server Protocol (LSP) is a standard protocol for interfacing IDEs and programming language tools. Two interfaces, each composed of a VS Code @@ -81,6 +82,7 @@

  • VsCoq 2
  • coq-lsp
    • +

    Both servers provide the extra ability of continuous and asynchronous document checking as well as position-based document navigation (an