Support proof assistants

artagnon commented 2 years ago

Coq implements a custom XML protocol described here to step through proofs, and update the goal and window at each step. Unfortunately, this has the consequence that many of the nice features that are otherwise available to languages going the LSP route are unavailable to Coq. The consumers of this protocol are CoqIDE, VSCoq, and Proof General.

Other proof assistants such as Isabelle/HOL have poor VSCode support and roll their own IDEs. Lean and Agda, in particular, do not suffer from this issue, because it is not a traditional "interactive proof assistant", whence one steps through proofs. In its VSCode extension for Lean, it automatically evaluates the entire buffer and stops at the first error. F* did suffer from this issue, and I happen to be the primary author of its LSP server: the work was stalled because there was no way to step through proofs via LSP.

This is a stark deficiency of the Language Server Protocol, and I feel that we can do better.

artagnon commented 2 years ago

The problem seems to be quite complicated, considering that there are many esoteric proof assistants like PVS and VDM, each with their own custom extensions. To break the problem up, I suggest we try to standardize some of the features required by Isabelle, Coq, Agda, and Lean in the initial draft.

Lean seems to be the easiest, as it defines 2 custom extensions in the toplevel and 8 more in infoview.ts. The core data structures are neatly separated out.

Isabelle defines several new "PIDE/" custom extensions, and its core data structures are:

/* decorations */

export interface Decoration_Options {
  range: number[],
  hover_message?: MarkdownString | MarkdownString[]
}

export interface Decoration
{
  "type": string
  content: Decoration_Options[]
}

export interface Document_Decorations {
  uri: string
  entries: Decoration[]
}

/* caret handling */

export interface Caret_Update
{
  uri?: string
  line?: number
  character?: number
  focus?: boolean
}

/* dynamic output */

export interface Dynamic_Output
{
  content: string
}

/* state */

export interface State_Output
{
  id: number
  content: string
  auto_update: boolean
}

export interface State_Id
{
  id: number
}

export interface Auto_Update
{
  id: number
  enabled: boolean
}

/* preview */

export interface Preview_Request
{
  uri: string
  column: number
}

export interface Preview_Response
{
  uri: string
  column: number
  label: string
  content: string
}

/* Isabelle symbols */

export interface Symbols
{
  entries: [symbol.Entry]
}

export interface Entries<T>
{
  entries: T[]
}

export interface Session_Theories
{
  session_name: string
  theories: string[]
}

Agda seems to define several new commands, and core data structures. The situation is very unclear, because it does a bunch of "document management" in the extension.

The current situation of Coq is similar to that of Agda, where it defines a bunch of custom commands, and the document management is done on the client side. However, @ejgallego is currently working on a coq-lsp (private), which promises to do the document management on the server side. The situation for Coq will hopefully become clearer next week, when I meet him.

michaelmesser commented 2 years ago

Idris is also interested in this issue.

ejgallego commented 2 years ago

All of Coq Isabelle and Lean have adopted LSP to various degrees, and I would be surprised if this issue has not been already raised at MS by @leodemoura .

From the Coq part, we've been experimenting with LSP since 2017 I believe, and it is still not clear to us what kind of extensions we would like to see; at least in the Coq side, lack of proper incremental document processing is blocking further progress.

If I had to ask something now, I'd ask for a richer display language.

artagnon commented 2 years ago

Not sure if this is what you mean, but we could extend TextDocumentPositionParams as:

interface TextDocumentPositionParams {
    /**
     * The text document.
     */
    textDocument: TextDocumentIdentifier

    /**
     * The position inside the text document.
     */
    position: Position

    /**
     * Indicates that the document has been processed by an interactive proof assistant from
     * the beginning upto this point.
     * If filled in, many LSP capabilities will be disabled beyond this point.
     */
    processedUpto?: Position
}

Since all the language feature LSP calls use TextDocumentPositionParams in some way, this would be the least ugly way of supporting the case of incremental document processing.

ejgallego commented 2 years ago

LSP supports (in fact requires) incremental document processing, it is Coq which doesn't.

michaelmesser commented 2 years ago

@ejgallego

If I had to ask something now, I'd ask for a richer display language.

Idris is interested in that as well. There was some discussion on adding semantic tokens to MarkupContent.

gebner commented 2 years ago

Hi, I'm one of the main developers of the Lean editor interface.

Roughly speaking, we use two major extensions to the LSP protocol (implemented using custom requests and notifications).

The $/lean/fileProgress notification, which contains the regions of the files that are still being processed by the Lean server. (See https://github.com/leanprover/lean4/issues/503 and for the specification.) These regions are shown as colored orange bars on the side of the editor. Isabelle has a similar feature.
A custom RPC protocol used to communicate the goal state. This requires a bit of complexity, since we show popups showing all the implicits arguments when the user hovers over a subterm (and plan to do more in the future). The client needs to communicate which terms are still shown (and could be used for a popup request) so that the server does not garbage collect them; the RPC protocol uses reference counting for this. We also use this RPC protocol to show better diagnostic messages (i.e. where you can hover over terms, and collapse long trace messages).

For other language features (like go-to-definition, find-references, semantic highlighting, symbol search, etc.), we use the regular LSP requests. The Lean process contains the LSP server and you can directly use it with any editor (although it will be awkward to use for proving since there is no dedicated display for goal states).

Generally speaking, I am very reserved about possibilities for the standardization of proving-specific requests. Standardization only makes sense if most editors implement the feature, and in a way that we all like. Furthermore, these features are coupled very tightly to the UX design of the prover. Different proof assistants clearly have very different views of how user interaction should work. I'd hate to have a standard prescribe Lean-style prover interaction to Coq users, or vice versa.

One thing that might be worth pushing in the LSP protocol though is clearer handling of long-running processing like we have in proof assistants, where one part of the document might have all language features available and the rest not (yet). IIRC, for example it is hard to provide semantic highlights via LSP for partially processed files (@kha might have more details on this).

Lean seems to be the easiest, as it defines 2 custom extensions in the toplevel and 8 more in infoview.ts. The core data structures are neatly separated out.

These are the vscode extension commands and has nothing to do with the LSP protocol used by Lean. For the extensions implemented by Lean 4, please check this file: https://github.com/leanprover/lean4/blob/7d8cb848341fac5ac42bb4bb80a756d5a348a3ca/src/Lean/Data/Lsp/Extra.lean

(In Lean 3 we had a very similar architecture; except that we used a nonstandard JSON-based protocol instead of LSP. The two protocols for Lean 3 and Lean 4 have on a high level essentially the same requests. I'm only mentioning this for completeness.)

ejgallego commented 2 years ago

Thanks a lot @gebner for the very detailed feedback, for sure $/lean/fileProgress seems like something most provers would like to use; I'm unsure how this functionality overlaps with the recent additions to the protocol for server-initiated progress reports.

Some related discussions about progress I could find are:

Related to progress, and pull diagnostics, something Isabelle has is the viewport notification; LSP devs have suggested to add it to the Pull Diagnostics request, IMHO that would be very useful for all the ITP users too, see https://github.com/microsoft/language-server-protocol/issues/718#issuecomment-1206503252

This way, we can understand what the user is seeing on the screen.

Regarding goals support, I do indeed agree that the general models of interaction are too diverse as to come up with a general solution; I wonder if the general case of using a side panel is also present in some other non-proof language servers; maybe LSP could provide support for this kind of side-panel setup in a generic enough way.

microsoft / language-server-protocol

Support proof assistants #1414