extending the VSCode / Lean4 UI

Stream: general

[TongKe Xue]

I'm looking for advice on how to do the following (ideally some project that already does something similar that I can copy from).

The standard VSCode/Lean4 UI looks something like this:
e5.png

LHS = code; RHS = Lean4 server output

I would like a layout of

LHS = code, RHS Top = Lean4 server output; RHS Bot = output of other program

I want this "other program" to:

1. render output to RHS Bot
2. from vscode: get updates any time cursor row/col, or buffer state (even if not written to filesystem)
3. from Lean4: be able to query server state, eval exprs

One can think of it as a "poor man's lean4 copilot"; I want this "other program" to have access to full program (via file system), what I'm currently looking at (via vscode updates), be able to run tests (vs lean4 server).

Is there any open source project that already has this that I can copy code from? Ideally one where all communication is done over websockets/tcpsockets, thus enforcing no requirements on language used in "other program"

Thanks!

[Shreyas Srinivas]

See Paperproof as an example

[Shreyas Srinivas]

Concretely you are lookin for the ProofWidgets library

[Shreyas Srinivas]

But it won't be as lively as the infoview. that's not as customisable right now

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Note that PaperProof is implemented as a standalone VSCode extension rather than using ProofWidgets, so those are different approaches

[TongKe Xue]

I apologize if I'm misunderstanding something fundamental. Is the following correct:

1. ProofWidgets have two parts.
2. One is written in Lean and runs inside the Lean server.
3. One part is written in Typescript and runs inside the VSCode InfoView.

I want something a bit different. That I can write in Elixir/Rust, have it run in a separate process (perhaps even over multiple machines), and talk to both Lean4 server & VSCode via websockets/tcpsockets.

I don't want to use the word "Agent/Agentic"; but I want this to "have a mind of it's own", to be able to do its own thing, to (1) look at what I'm looking at in vscode, and (2) try to prove stuff independently, and surface anything it finds useful in the infoview.

Is the existing ProofWidgets/UserWidgets API the best starting place for this ? (One thing I really want, especially in using Exliir, is to "update my agent code" while the VSCode/Lean4 continues to run.)

[Shreyas Srinivas]

you can structure that by writing a server in your program with a well defined API that takes requests. Separately you can write your own vscode extension that checks whether this server exists and talks to it.

[Shreyas Srinivas]

The vscode extension can depend on the lean extension and call its methods

[TongKe Xue]

It's not clear to me. Is the advice here:

1. do these two separate parts without ProofWidget/UserWidget or
2. create a UserWidget that "wraps external Elixir/Rust process" by providing a basic API and routing everything to the UserWidget InfoView ?

[Shreyas Srinivas]

I am responding to what you said “I want this to have a mind of its own”

[Shreyas Srinivas]

Essentially you can do stuff with proofwidgets or write your own extension. In the former case there are limitations and the proofwidgets repository has documentation and examples

[Shreyas Srinivas]

In the latter case your only limitation is what the vscode extension API allows

[TongKe Xue]

Ah, this is my fault for not being clear. Let me try to rephrase this. Consider this:

theorem h1 : ... := sorry
theorem h2 : ... := sorry
theorem h3 : ... := sorry

depending on where the cursor is, the infoview is very reactive in showing the proof state at the location of the cursor.

I am looking for ways to build external tools that are "more independent"; I want my plugin to be notified of vscode cursor movement, but be a independent process that can do its own thing.

For example, imagine a system where:
c-1 = record current hypothesis / goal state, have external process try to solve it in parallel
c-2 = list all "external process search", allowing us to see how long it's been running for / killing processes

So to build something like this, I want some external elixir/rust process doing its own thing, talking to vscode/lean4 over websocket/tcpsocket.

So my question here is: besides the vscode/lean4 extension, is there anything else worth looking into that might have the right "architecture" to support something like this?

Thanks!

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Is the following correct:

1. ProofWidgets have two parts.
2. One is written in Lean and runs inside the Lean server.
3. One part is written in Typescript and runs inside the VSCode InfoView.

This is essentially right; there are three programs involved: the Lean LSP server, VSCode, and the infoview (the infoview is launched by VSC but it's sandboxed, so for all intents and purposes a separate program). Whenever actions are carried out in VSC, e.g. you move your cursor to another line, VSC informs the infoview about those actions, and the infoview in turns requests the LSP server to provide new information. See also Fig. 9 in the paper, and the explanation of widget APIs here.

you can structure that by writing a server in your program with a well defined API that takes requests. Separately you can write your own vscode extension that checks whether this server exists and talks to it.

I would strongly advise against writing your own extension; everything suggested here should be implementable as a widget.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I am looking for ways to build external tools that are "more independent"; I want my plugin to be notified of vscode cursor movement, but be a independent process that can do its own thing.

I don't think it follows from your proposed architecture that your agent has to be a separate process; you may as well run it as a parallel docs#Task in the LSP server. But if you really want a separate server program, that should be possible as well.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@TongKe Xue here is something to get you started (based on the LazyComputation demo). Note that /usr/bin/ps won't run in the Lean playground, but it might run for you locally.

module

public meta import Lean.Widget
public meta import ProofWidgets.Component.Basic

public meta section

open ProofWidgets
open Lean Meta Server Elab Tactic

structure EmptyArgs where
  deriving FromJson, ToJson

@[server_rpc_method]
def queryPsServer : EmptyArgs → RequestM (RequestTask String)
  | _ => RequestM.asTask do
    let res ← IO.Process.run { cmd := "/bin/ps" }
    return res

@[widget_module]
def runnerWidget : Component EmptyArgs where
  javascript := "
    import { RpcContext, mapRpcError } from '@leanprover/infoview'
    import * as React from 'react';
    const e = React.createElement;

    export default function(props) {
      const [contents, setContents] = React.useState('Run ps!')
      const rs = React.useContext(RpcContext)
      return e('button', { onClick: () => {
        setContents('Running..')
        rs.call('queryPsServer', props)
          .then(setContents)
          .catch(e => { setContents(mapRpcError(e).message) })
      }}, contents)
    }
  "

-- Put your cursor here
#widget runnerWidget

[Eric Wieser]

Am I right in thinking that #widget cannot respond to document changes below it?

[Eric Wieser]

And conversely, can I widget preserve state across re-renders if the document is changed above?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Eric Wieser said:

Am I right in thinking that #widget cannot respond to document changes below it?

What kind of changes are you thinking of? If you want to have a widget that sticks around at all times (e.g. like the goal display), you'd use the show_panel_widgets command.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Eric Wieser said:

And conversely, can I widget preserve state across re-renders if the document is changed above?

Widgets preserve the UI state for as long as they are visible, and reset the state when they appear again; so show_panel_widgets would also be the thing to use if you want the state to stick around for longer. There is some discussion of this under ProofWidgets4#141, but TLDR I'm not sure it'd be a good idea for widgets to preserve UI state across re-renders; it's clearer if the Lean file suffices to fully reconstruct the display.

[Eric Wieser]

I'm thinking of the case where you want a widget to do work in the background while edits are ongoing in the lean file

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Yes, in case there is still ambiguity about that, panel widgets preserve their state while the file is being edited; but they will lose state on certain actions, e.g. if the infoview were reopened.

Let's suppose we wish to provide an interface to control an army of prover agents that might be quite long-running. Here is how I would probably structure such a thing.

• A standalone server process that keeps track of the running proof jobs with API endpoints like /job_status, /start_job, etc.
• A panel widget to be used with show_panel_widgets which connects to the server, displays the running jobs, provides some UI to launch a new proof attempt for the sorry under the cursor, and communicates successful job outcomes back to the editor (e.g. by replacing the sorry with the found proof).
  • The "launch" button could also be implemented as an LSP code action, but iirc these are not very well-suited for long-running tasks.

The reason I'm suggesting a standalone server as opposed to keeping track of the jobs solely inside the widget JS code is that, per the above discussion, widgets do not preserve state across re-renders. A panel widget displayed via show_panel_widgets is not re-rendered often, but it would be re-rendered if you e.g. reopen the whole infoview.

One could maybe also store the state in the LSP file worker, but that only lasts as long as a given file worker, i.e., would be cleaned up if you close a Lean file and open another. Iirc there is no way to run custom code in the LSP watchdog (the only Lean server process which actually lives as long as the entire server).

If the background work you have in mind is quicker (seconds to minutes?), then you may be able to get away without the server component and store all state in the widget.