[WIP] Paperproof's Architecture

This post is about the internals of Paperproof.
It's useful if you want to work on paperproof, on vscode-lean4, or if you want to create your own vscode extension for Lean/Coq/etc. 

We have 3 pieces of code:

• extension codebase (code in /paperproof/extension)
  Typescript code that you download when you install the Paperproof vscode extension.
• webview codebase (code in /paperproof/app)
  Typescript code. Technically a part of the extension codebase, but it's best to separate them in your mind.
• Lean library codebase (code in /paperproof/lean).
  This is Lean code that you import when you do require Paperproof from git "https://github.com/Paper-Proof/paperproof.git"@"main"/"lean" and import Paperproof.

All of these pieces of code can talk to each other, and all of them possess different information about what the user is up to.

What does each codebase know

Below you can see my vscode editor.

To be able to work on Paperproof (or, really, on any vscode exension), it's a good idea to get a sense for "what kind of knowledge is available to what codebase". Below I will list some examples:

• extension codebase
  Knows everything the user is doing in the left panel (where your actual Lean theorems are).
  For example, you can get a plaintext of this file; you can get a file name; you can determine when the user clicked on  some line and character; you can determine what text the user just selected; you can subscribe to the "user typed something" event.
• webview codebase
  Controls everything in the panel on the right.
  Unlike the extension, webview will know when the user clicked on some green hypothesis rectangle. Consider this a normal webpage - you can determine if the user typed something within your <input/> field in the webview, you can determine if the user pressed some shortcut, you can send the ajax request. Anything a browser can do, a webview can do.
• Lean library codebase
  Even though extension codebase technically knows everything that's going on in your project (it can copy the contents of any file in your workspace!), it can only work with plaintext files. On the left of my editor, you can see Lean code - and extension on its own only sees it as, well, text. However, we frequently want to understand the structure of this code in a deeper manner.
  For example, I might want to determine if this Lean-looking plaintext even compiles.
  I might want to determine what goals and hypotheses were available at line 137 character 20.
  I might want to glean the entire history of this theorem by parsing this theorem's InfoTree.
  This is the kind of information that Lean compiler (an entity that's really good at converting plaintext into Lean, remember) knows, and we can ask Lean library about these things.

How these codebases talk to each other

So - extension, webview, and Lean library have access to different information, and we need some way to share this information between these codebases to make Paperproof work.

For example, every time the user clicks on a tactic within some theorem, we want to detect line and character of that mouse click (extension knows that); detect the InfoTree that belongs to that line and character (Lean library knows that); and display that InfoTree as a Paperproof tree in the webview (Webview can do that).

There are exactly three types of communication between these codebases:

• extension talks to webview via .postMessage() calls
• webview talks to extension via .postMessage() calls
• extension talks to Lean library via RPC calls

Extension → Webview; Webview → Extension

As just said, both of these communications happen via .postMessage() calls.

.postMessage() is a normal, widely supported browser api - it works in vscode (reminder that vscode is a browser-based editor, at the moment of writing it uses Chrome v128), and it will work in all modern browsers. Although widely supported, this api is rarely used in web development - working on a vscode extension was the first time I had to deal with it.

.postMessage() was developed to enable communication between a document and the iframe embedded in it. To quote the docs:

The Channel Messaging API allows two separate scripts running in different browsing contexts attached to the same document (e.g., two <iframe> elements, the main document and a single <iframe>) to communicate directly, passing messages between each other through two-way channels (or pipes) with a port at each end.
_{(From developer.mozilla.org/en-US/docs/Web/API/Channel_Messaging_API/Using_channel_messaging)}

As it stands, "webview" in a vscode editor is nothing more than an <iframe> embedded in a particular space in vscode's html, as you can see in the screenshot below.

So the conversation between our webview (embedded <iframe>) and extension (main document) happens via the .postMessage() calls as follows.

In webview:

const extension = acquireVsCodeApi();
extension.postMessage('hi hello');
addEventListener('message', (event) => {
  const messageFromExtension = event.data;
  ...
});

In extension:

const webview = vscode.window.createWebviewPanel(...);
webview.webview.postMessage('red blue green');
webview.webview.onDidReceiveMessage(async (message) => {
   const messageFromWebview = message;
   ...
}

Extension → Lean Library

Webview cannot directly talk to our Lean library, any such communicatin must happen with extension as an intermediary. Communication between the extension and  Lean library happens via "RPC calls".

In extension:

const connection = await leanClient.sendRequest("$/lean/rpc/connect", { uri: editor.document.uri.toString() });
const response = await leanClient.sendRequest("$/lean/rpc/call", {
   sessionId: connection.sessionId,
   method: 'getOurInfoTree'
})

In Lean library:

@[server_rpc_method]
def getOurInfoTree (params : InputParams) : RequestM (RequestTask OutputParams) := do
  withWaitFindSnapAtPos params.pos fun snap => do
    let parsedTree ← BetterParser snap.infoTree
    ...

We get leanClient from the vscode-lean4 extension (default Lean interface that gives you the InfoView). 

This setup is generally all you need to know, but if you'd like to get a good understanding of the internals of RPC requests, you can start by reading the vscode's official guide on Language Servers: link; and the corresponding Language Server implementation in Lean: link.

Lean objects of interest

Two most important Lean objects for Paperproof (and for Lean-Vscode) are Snapshot and InfoTree. 

In Lean, each command (command is a syntax category - e.g., theorem is a command, lemma  is a command, #lint is a command) is associated with a Snapshot Lean object.

Given a line number and a character number, we can determine the relevant Snapshot. For example, withWaitFindSnapAtPos { line: 708, character 20 } λ snapshot => do {} will return the snapshot for the subset_biUnion_of_mem theorem, just like any other line & character combination within that theorem.

Request handlers usually locate and access a single snapshot in the tree based on the cursor position using withWaitFindSnap, which will wait for elaboration if it is not sufficiently progressed yet. After the snapshot is available, they can access its data, in particular the command's Syntax tree and elaboration InfoTree, in order to respond to the request.
_{(From github.com/leanprover/lean4/blob/master/src/Lean/Server/README.md)}

The Snapshot object, in its turn, has snapshot.infoTree field, which gives us the InfoTree object. It contains a list of tactics, and all goals and hypotheses before and after each tactic was applied. To quote the docs again:

The InfoTree is the second central server metadata structure. It is filled during elaboration with various metadata that cannot (easily) be recovered from the kernel declarations in the environment: goal & subterm infos including the precise local & metavariable contexts used during elaboration, macro expansion steps, etc. Once a relevant Snapshot snap has been located, snap.infoTree.smallestInfo? and other functions from Lean.Server.InfoUtils can be used to further locate information about a document position. The command set_option trace.Elab.info true instructs Lean to display the InfoTree for the declarations occurring after it.
_{(From github.com/leanprover/lean4/blob/master/src/Lean/Server/README.md)}