Lean-TUI (self-contained infoview)

Stream: Editors & UIs

[Willem vanhulle]

I am creating a TUI with Ratatui for Lean. It is accompanied by a proxy LSP that intercepts Lake LSP. It can be used for anyone who doesnt want to use VS Code's info view, but still wants to be able to see proof state changing while developing (Helix, or any other editor with LSP client).

Try it out here: https://codeberg.org/wvhulle/lean-tui/src/branch/main

Here is a screenshot of the before / after feature with the proof of infinite primes focused

image.png

[Notification Bot]

This topic was moved here from #lean4 dev > Lean-TUI (self-contained infoview) by Patrick Massot.

[Castedo Ellerman]

Wow! This is great to hear. I was getting ready to build something like this myself, but what you've done sounds way better than what I was going to make! :sweat_smile:

Here is a topic I started recently trying to find out whether something like Lean-TUI exists: #general > Editor-decoupled file-watching proof-state-outputing tool

[Willem vanhulle]

Castedo Ellerman said:

Wow! This is great to hear. I was getting ready to build something like this myself, but what you've done sounds way better than what I was going to make! :sweat_smile:

Here is a topic I started recently trying to find out whether something like Lean-TUI exists: #general > Editor-decoupled file-watching proof-state-outputing tool

I should maybe have waited a bit for posting it since it’s mostly a prototype written in one day. Please give me a few days to improve it a bit.

[Willem vanhulle]

Published an easier to install package on https://crates.io/crates/lean-tui

[Castedo Ellerman]

Willem vanhulle said:

I should maybe have waited a bit for posting it since it’s mostly a prototype written in one day.

No! I'm glad you posted about your prototype because:

1. we all can make smarter plans being aware of the smart work you're doing
2. prototypes are great for testing, learning, seeing what works, what does not work, etc...
3. this week I am learning Lean via textbook/tutorials etc... and I can use both Lean-TUI and VSCodium and https://castedo.gitlab.io/vim9-lean/ and start documenting what is missing pros/cons, between VSCodium vs not.

Please give me a few days to improve it a bit.

Great to hear you want to improve the prototype, thank you!

[Willem vanhulle]

Here is a better diagram of the architecture of this editor plugin

image.png

[Willem vanhulle]

As can be found on https://codeberg.org/wvhulle/lean-tui

[Castedo Ellerman]

Regarding the protocol over the Unix socket between lean-tui proxy and lean-tui view, what is the possibility of that being a stable protocol and compatible with other applications in other programming languages?

[Willem vanhulle]

Castedo Ellerman zei:

?

I haven't researched previous work on this, but I needed things that are explicitly not in the LSP protocol for displaying proof state and navigating in it.

[Castedo Ellerman]

My question is a bit ambiguous. I didn't mean "stable protocol" as in a protocol that already exists. I just mean something the you and/or Lean community establish that can transmit over local unix domain socket. My experience here is a little weak. I'm somewhat familiar with Google Protocol Buffers (Protobuf) which sounds nice, but I haven't used it much.

[Willem vanhulle]

Castedo Ellerman zei:

My question is a bit ambiguous. I didn't mean "stable protocol" as in a protocol that already exists. I just mean something the you and/or Lean community establish that can transmit over local unix domain socket. My experience here is a little weak. I'm somewhat familiar with Google Protocol Buffers (Protobuf) which sounds nice, but I haven't used it much.

If you like pain, go for Google Protocol Buffers ;). In this case, the latency over the Unix socket is microseconds at most and the data size is very small, so I wouldn't bother trying to do better than JSON

[Castedo Ellerman]

Willem vanhulle said:

In this case, the latency over the Unix socket is microseconds at most and the data size is very small, so I wouldn't bother trying to do better than JSON

OK, that makes sense. The overhead of profobuf for low-level performance is not worth it. There is one thing that seems better than "just JSON" which is something like .proto files which allow language independent definition of the messages/records/fields. And then libraries for specific languages that will correctly serialize/deserialize based on those definitions. Do you have a recommendation on how to define the JSON messages so that applications in Python or TypeScript or Rust or Lean can easily and correctly read/write those JSON messages?

[Willem vanhulle]

Castedo Ellerman said:

Willem vanhulle said:

In this case, the latency over the Unix socket is microseconds at most and the data size is very small, so I wouldn't bother trying to do better than JSON

OK, that makes sense. The overhead of profobuf for low-level performance is not worth it. There is one thing that seems better than "just JSON" which is something like .proto files which allow language independent definition of the messages/records/fields. And then libraries for specific languages that will correctly serialize/deserialize based on those definitions. Do you have a recommendation on how to define the JSON messages so that applications in Python or TypeScript or Rust or Lean can easily and correctly read/write those JSON messages?

There is something called JSON schema for specifying formats of JSON.

[Willem vanhulle]

But you would only use that when there are actual consumers down the road using completely different types front ends

[Castedo Ellerman]

Willem vanhulle said:

when there are actual consumers down the road using completely different types front ends

I think what I am starting to imagine is that long-term lean --serve eventually provides a socket connection like lean-tui proxy in some multi-language friendly JSON protocol. Then multiple different tools, including lean-tui view and "Lean-LocalWebApp" (#general > Editor-decoupled file-watching proof-state-outputing tool @ 💬) and potentially more can read that JSON protocol full of Lean specific stuff without needing to be an LSP protocol. Ideally this socket connection handles mutliple connections (I think).

If lean-tui supports this JSON protocol then the timing of lean --serve obsoleting lean-tui proxy and the timing of lean-tui view and Lean-LocalWebApp and clients working with either server/proxy can be decoupled.

[Julian Berman]

I think what I am starting to imagine is that long-term lean --serve eventually provides a socket connection like lean-tui proxy in some multi-language friendly JSON protocol.

This sentence is a pretty good description of what LSP itself is. It's a multi-language friendly protocol, specified to serialize to JSON (though in theory that choice could have been whatever your favorite serialization format is, say protobuf), and then it has mechanisms for adding extension requests which are specific to a single language or language server. Lean uses those, it schematizes what their parameters and responses are, and it defines when you're supposed to call them. I see you saying "without needing to be an LSP protocol" -- but in general being LSP is a plus, not a minus, it means you can pull any LSP client in any language you'd like and start talking to the thing. If you're asking for machine-readable LSP, this is discussed quite a bit on the LSP specification repo, e.g. https://github.com/microsoft/language-server-protocol/issues/67 and there's a bunch of JSON Schemas for LSP itself lying around, but also typescript people love typescript and typescript interfaces (just like Lean people love Lean, and JSON Schema people love JSON Schema), so in practice I think people generating different machine-readable formats is always a reality for schema languages.

[Willem vanhulle]

Julian Berman said:

I think what I am starting to imagine is that long-term lean --serve eventually provides a socket connection like lean-tui proxy in some multi-language friendly JSON protocol.

This sentence is a pretty good description of what LSP itself is. It's a multi-language friendly protocol, specified to serialize to JSON (though in theory that choice could have been whatever your favorite serialization format is, say protobuf), and then it has mechanisms for adding extension requests which are specific to a single language or language server. Lean uses those, it schematizes what their parameters and responses are, and it defines when you're supposed to call them. I see you saying "without needing to be an LSP protocol" -- but in general being LSP is a plus, not a minus, it means you can pull any LSP client in any language you'd like and start talking to the thing. If you're asking for machine-readable LSP, this is discussed quite a bit on the LSP specification repo, e.g. https://github.com/microsoft/language-server-protocol/issues/67 and there's a bunch of JSON Schemas for LSP itself lying around, but also typescript people love typescript and typescript interfaces (just like Lean people love Lean, and JSON Schema people love JSON Schema), so in practice I think people generating different machine-readable formats is always a reality for schema languages.

It also depends on the editor and indirectly the LSP client of the editor. Most editors implement a portion of the LSP protocol. Lean LSP server only emits a portion of the LSP protocol. Editors like Helix are very opinionated and refuse certain extensions like custom views or custom cursor tracking. You need to work around that somehow.

[Willem vanhulle]

Castedo Ellerman said:

Willem vanhulle said:

when there are actual consumers down the road using completely different types front ends

I think what I am starting to imagine is that long-term lean --serve eventually provides a socket connection like lean-tui proxy in some multi-language friendly JSON protocol. Then multiple different tools, including lean-tui view and "Lean-LocalWebApp" (#general > Editor-decoupled file-watching proof-state-outputing tool @ 💬) and potentially more can read that JSON protocol full of Lean specific stuff without needing to be an LSP protocol. Ideally this socket connection handles mutliple connections (I think).

If lean-tui supports this JSON protocol then the timing of lean --serve obsoleting lean-tui proxy and the timing of lean-tui view and Lean-LocalWebApp and clients working with either server/proxy can be decoupled.

What do you mean with timing and obsoleting?

[Castedo Ellerman]

Julian Berman said:

but in general being LSP is a plus, not a minus, it means you can pull any LSP client

To make sure we are on the same page: my understanding is only one LSP client process can connect to an LSP server process? and as lean --serve is currently implemented only one LSP client process can connect to the LSP server endpoint of lean -serve. Are both these statements true?

[Castedo Ellerman]

Willem vanhulle said:

If lean-tui supports this JSON protocol then the timing of lean --serve obsoleting lean-tui proxy and the timing of lean-tui view and Lean-LocalWebApp and clients working with either server/proxy can be decoupled.

What do you mean with timing and obsoleting?

I mean in the hypothetical future possibility that lean --serve serves a socket connection like lean-tui proxy and there are other clients like lean-tui view, like perhaps Lean-LocalWebApp, then people can mix-and-match those possibilties as they happen in the future. Whether anything is obsoleting I don' t know, but it would allow that possibilty. By timing I just mean the timing of future projects and possiblities of this mixing.

[Julian Berman]

Castedo Ellerman said:

To make sure we are on the same page: my understanding is only one LSP client process can connect to an LSP server process? and as lean --serve is currently implemented only one LSP client process can connect to the LSP server endpoint of lean -serve. Are both these statements true?

LSP is currently single-client. Searching found me https://github.com/microsoft/language-server-protocol/issues/67 which explicitly says there's no interest in changing that anytime soon, but also links to a somewhat "obvious" kind of tool which muxes incoming requests from multiple clients. I guess if I imagine where you're going with this, you want an editor and some non-editor second thing to connect to the same Lean server simultaneously? If so, lspmux or something like it would sound like maybe it's indeed relevant, but whether all the details work out needs checking.

[Castedo Ellerman]

Julian Berman said:

you want an editor and some non-editor second thing to connect to the same Lean server simultaneously?

Exactly! :this:

Willem and I have a prototype of this working now where we have our favorite editor (Helix and vim 9 respectively) connecting via stdio to a subprocess of (lean-tui proxy + lake server) and then also connecting to that very same process, but via a socket insted of stdio, is a non-editor second thing, which is lean-tui view (running in a terminal window as a separate process).

In the future, it might make sense for the subprocess of (lean-tui proxy + lake server) to be replaced with just (lake server).

And in the future another non-editor thing that can connect via socket might be "Lean-LocalWebApp" with Lean widget support.

[Willem vanhulle]

Add two more alternative display modes when PaperProof is installed:

• Deduction style tree (similar to the TypeScript implemented tree in VS Code)
• Proof steps and all goals and hypothesis in two separate panes

Deduction style screenshot:
deduction_style.png

Check out docs on how to switch display mode: https://codeberg.org/wvhulle/lean-tui

[Castedo Ellerman]

For those interested in technical disucssions relating to Lean-TUI, I have been submitting issues and discussions topics to https://codeberg.org/wvhulle/lean-tui/issues. @Julian Berman You might be interested in the LSP and lspmux related topic I'm wondering about: https://codeberg.org/wvhulle/lean-tui/issues/5

I'm communicating on codeberg.org because I think that's what @Willem vanhulle prefers, it seems a good forum for topics focused directly on what he is developing, and I like the idea of exploring forums that are not GitHub. Hopefully codeberg.org has enough of the positive features of GitHub.

[Willem vanhulle]

Added navigation with keyboard arrows and clicking for large proofs
semantic_tableau.png

And better tactic tree view
tactic_tree.png

For documentation and more see https://codeberg.org/wvhulle/lean-tui

[Willem vanhulle]

Better architecture diagram

[Willem vanhulle]

image.png

[Willem vanhulle]

Try it out at https://codeberg.org/wvhulle/lean-tui

[Willem vanhulle]

Based on some feedback from @Castedo Ellerman and seeing many people have interest in integration with web-frontends, I moved from Unix socket to a universal TCP port. This means people only have to know the JSON schema (which should be reasonably stable from now on) to communicate with the Lean back-end lean-dag. All business logic was moved into this Lean back-end, so Lean-TUI is now just a Rust front-end.

[Castedo Ellerman]

My understanding from the web is that Windows 10+ now support Unix domain sockets. So unix sockets is a good choice for a raw JSON stream. It's pretty safe that the unix socket path will not be reused whereas the TCP port space is more crowded. Idealy which socket is used if configurable which makes testing easier.

[Castedo Ellerman]

My main observation regarding listening on a local network TCP port is that it enables a WebSockets option for browser based web apps. This has security implications that require some thought about the protocol and user experience.

[Castedo Ellerman]

My recommendation is to decouple web based web apps connecting to local WebSockets TCP/IP ports and leave that for a separate local application. The separate location application can connect to the default unix domain socket.

[Willem vanhulle]

Castedo Ellerman said:

My recommendation is to decouple web based web apps connecting to local WebSockets TCP/IP ports and leave that for a separate local application. The separate location application can connect to the default unix domain socket.

@Castedo Ellerman I love your enthusiasm, but I don’t really understand what this has to do with Lean. Maybe this is the right moment to get your hands dirty and open some PRs on lean-dag? It is a great moment to practice your Lean skills.

[Castedo Ellerman]

Willem vanhulle said:

I don’t really understand what this has to do with Lean.

I assume by "this" you mean my recommendation. My recommendation has to do with your move from UNIX socket to TCP port. You said it was based on feedback from me. But this was my feedback: https://codeberg.org/wvhulle/lean-tui/issues/3 and I closed it as feedback to keep the WebSockets applications separate.

And you said the move is also due to people having an interest in integration with web-frontends. Web-front-ends need a WebSockets connection. Last time I checked your JSON protocol on the UNIX socket is not a WebSockets connection. So it can't be used by a web frontend. So i'm surprised you have moved to TCP because that just introduces risk of port collision.

Maybe this is the right moment to get your hands dirty and open some PRs on lean-dag? It is a great moment to practice your Lean skills.

Maybe. At this moment I have near-zero Lean skills for I have no Lean skills to practice with. :sweat_smile: But hopefully that changes in the not too distant future.

[Patrick Massot]

I think it would be more efficient for you to work with Lean a bit before investing too much time working on UI for Lean. Using Lean is very different from using other programming languages, and you may realize that a lot of common wisdom does not apply here.

[Patrick Massot]

Note this doesn’t mean there is nothing interesting and relevant to do about Lean UI (and I still have nightmares haunting me from the time I was forced to use VSCode because lean.nvim was not yet ready). I’m talking about effort optimization here.

[Willem vanhulle]

Does anyone here have any need to visualise monadic lean programs? I know there is separation logic and Hoare triples, but I don’t know if there is an actual demand for such a feature in a Lean Infoview UI?

[Snir Broshi]

Can you sketch an example in mspaint or similar to what you have in mind? Do you mean a tree of Hoare triples derivations?

[Willem vanhulle]

Snir Broshi zei:

Can you sketch an example in mspaint or similar to what you have in mind? Do you mean a tree of Hoare triples derivations?

I made a version inspired by Aeneas that shows backward and forward aspects of effects. It's just an idea, but I am new to Aeneas so it is not entirely clear what the most efficient display would be.

image.png

I am also experimenting with visualizations of pure functional programs

image.png

The idea is that users can use built-in rules for data / effect flow visualization or provide their own by importing the Lean backend https://codeberg.org/wvhulle/lean-dag

All logic was moved to the Lean back-end to make it easier for Lean users to contribute and maintain.

[Willem vanhulle]

Changes: make coloring consistent and show diagnostics next to nodes in diagram.

Get latest version 0.6.2 at https://crates.io/crates/lean-tui

Plain Goals View

Just shows the proof as a list of hypotheses and goals. When an error is active around the cursor position, it also shown. Select a hypotheses or goal and press g to move your cursor in your editor to the location where it was introduced. Press y to copy it to you clipboard for pasting elsewhere.

Hypotheses are blue. Goals are orange. Errors are red.


For the VS Code users: Yes, the official info view endorsed by the Lean organization is written for VS Code, However, I don't like VS Code and vendor lock-in. We should all try to move away from any Microsoft-owned product as soon as possible. Why? Take a look at for example "Embrace, extend, and extinguish" but also the recent news.

For the Neovim users, yes there existed an info view Lean plugin for Neovim already, but not yet for the other terminal editors (Zed, Kakoune, Helix, ...) since the Lean plugin relies on Neovim specific features. It is not a generic one.

Semantic Tableau View

Visualizes your active proof as a semantic tableau. This is based on how logicians traditionally render their deductions. Errors are often too long and would not fit in a node alone, so you can click on it to expand it in a popup at the top of the screen. Press escape to close the popup or select another node.

Again, press g to jump to the selected hypothesis or goal. Use the arrow keys or hjkl to jump with keyboard only.

 |

For Paperproof users: Paperproof was a big inspiration for this view. However, it is Web-based. I used their approach to move most of the logic into Lean and add an RPC method there.

Before/After View

Shows active goal state and on the left also the previous state. You can hide the previous state pane with p and also show the next pane with n (disabled by default).

In addition to the default colors, assumptions, or hypotheses that are added are highlighted in green. Removed ones are highlighted in red. Errors from cursor position are also shown if present.


Tactic Tree View

Shows a rendering of the proof displayed as compact Unicode tree on the left. On the right, you can see, active hypotheses and goals. The tree will update its location by focusing the active proof state at the cursor position.

The same key bindings and colors apply as other views.


Graphs of Functional Programs

There are display modes focused on everything that is not a tactic proof. These modes should be useful for functional or monadic programming. You can test them out with some test files in ./Samples

Data Flow (Experimental)

Use this for term-style proofs (without by or tactics). You can also use it for normal pure functional programs. It shows a graph of the local bindings and expected types throughout the program

The decomposition is based on a few built-in rules. However, not all Lean control flow has an accompanying rule. Please be patient as I add more rules or contribute yourself them to lean-prism. Rules can also be provided in user code and are picked up by LeanPrism (not tested yet).

Open the legend with L to see what all symbols and colors mean.


Effect Flow (Experimental)

When working doing programming in a monad, you are doing some kind of effectful computations. Every monadic assignment in Lean written as let <- COMPUTATION can be composed in two parts:

• What the computation produces, shown with a forward arrow
• What state changes are given back components (the effect), shown with a backward arrow

This decomposition is not implemented yet for all monads. Please contribute if you have time. You just need to specify how to compute the forward and backward expressions and have to label edges. You can also provide rules in user code (not tested yet).

The purple edges in the diagram are definition expansions (will be hide-able in future) and the blue ones are the monadic binds. Displaying errors is not implemented yet.

Open the legend with L to see what all symbols mean.


[Willem vanhulle]

Has anyone got the time to try out v0.6? @Julian Berman @Patrick Massot

[Julian Berman]

I haven't yet but I certainly mean to try it, I just have too much on my plate at this moment but certainly will try to give you some feedback (and again props for making something new and cool!)

[Willem vanhulle]

Julian Berman zei:

I haven't yet but I certainly mean to try it, I just have too much on my plate at this moment but certainly will try to give you some feedback (and again props for making something new and cool!)

Take your time. The front-end / UI features are relatively stable now. The Lean back-end is still being worked on.

Things you may want to look out for while testing: the tactic-style proof views, layout, information displayed, confusing things, whether it is actually helpful...

It has been a while that I actually did some real theorem proving, so it would nice to have some input from active Lean users.

[Patrick Massot]

Same as Julian. I’m definitely interested but time is very scarce.

[Willem vanhulle]

Patrick Massot zei:

time is very scarce

This is a small video/GIF to show basic usage scenario:

[Julian Berman]

What's not clear to me from that gif is does lean-tui not update what it shows when the cursor moves in the editor?

[Julian Berman]

That's pretty key functionality I think for an infoview is that what you see should relate to the cursor position in some tight way

[Willem vanhulle]

It updates while typing or when hovering.

[Willem vanhulle]

It’s just that helix is quite picky and does not sent hover unless you actually type or open the docs with a keybinding

Julian Berman said:

What's not clear to me from that gif is does lean-tui not update what it shows when the cursor moves in the editor?

[Willem vanhulle]

lean-tui-demo.webm
@Julian Berman
Longer video with keybindings as well and monad view