Editor-decoupled file-watching proof-state-outputing tool

Stream: general

[Castedo Ellerman]

I'm very new to Lean but very old to computers. I like loose coupling [7] between my computer tools, especially to my editor. I'm happy with stable standard LSP [8], but dislike the tight editor-to-Lean coupling via non-standard LSP extensions. I lament the possibility that one must choose from a tiny set of editors to enjoy the InfoView benefits of the VS Code extension.

Are there any documents or pointers that folks can share on how to set up an "editor-decoupled file-watching proof-state-outputting tool"?

I have found related Zulip topics [10] and [11] (thx @Julian Berman) but those aren't about file-watching tools.

By "file-watching" I mean a tool that watches for changes to source files (and then outputs useful updated information based on those source files). The output could be terminal output or a local web page. Here are some examples of such "editor-decoupled file-watching tools" (from non-Lean contexts):

• Quarto [1] "Use your favorite tools including ... any text editor."
• Vite [2] "Instantly reflect changes as you save, no matter how big your app is."
• Vitest [3] "Smart & instant watch mode"
• live-server [4]
• nodemon [5] "reload, automatically"
• entr [6] "Run arbitrary commands when files change"

Note how Vite and live-server work well with web browser developer tools [9] with zero coupling to particular editors. I suspect that web browser developer tools provide essential information for HTML/CSS/JS/DOM development that exceeds, in complexity, what InfoView provides for a Lean proof (in two completely different contexts, obviously).

File-watching tools are "interactive" with source files and the UI of a file-watching tool, rather than the UI of an editor.

Please note, I do not question the value of an IDE approach for most users, especially new users.

Thank you,
Castedo

PS: I have hooked up standard LSP features for Lean into Vim 9: https://castedo.gitlab.io/vim9-lean

[7] https://en.wikipedia.org/wiki/Loose_coupling
[8] https://en.wikipedia.org/wiki/Language_Server_Protocol
[10] https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/InfoView.20in.20a.20Web.20Browser.3F/with/539918689
[11] https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Lean.20.2B.20Zed.20integration/with/505673863
[1] https://quarto.org/docs/get-started/hello/text-editor.html
[2] https://vite.dev/
[3] https://vitest.dev/
[4] https://www.npmjs.com/package/live-server
[5] https://nodemon.io/
[6] https://eradman.com/entrproject/
[9] https://developer.chrome.com/docs/devtools/overview

[Thomas Murrills]

Welcome! :) I’m unfamiliar with these tools, but to pin things down a bit, let me ask: do any of them have any access to the editor state? (My limited understanding is no; that you’re asking about watching only the file.) If not, then without access to the cursor position (and only access to the file), how do you envision choosing which proof state to display? Perhaps there is a way, but just to clarify what you’re looking for. :)

[Castedo Ellerman]

Thomas Murrills said:

do any of them have any access to the editor state?

No, no editor state. However, some of these file-watching tools parse source files into rich in-memory representations (e.g. of the HTML Document Object Model). Then the non-editor tool can have persistent state about what part of the output is of interest.

how do you envision choosing which proof state to display?

By whatever means is loosely coupled from the editor. :smiley:

Some quick ideas: Maybe the name of a theorem as a CLI parameter. Maybe the source code is reprinted entirely in a local web page and the user selects a line and the tool keeps track of line. Maybe the user can insert '#foobar' in the source and that triggers that part of the document to get lots of proof state printed. I'm new to Lean proofs, so I'm not sure.

[Shreyas Srinivas]

How would you make this work with lean’s incredibly flexible syntax system?

[Castedo Ellerman]

Shreyas Srinivas said:

How would you make this work with lean’s incredibly flexible syntax system?

With a setup that is built on top of Lean software that works with Lean's incredibly flexible syntax system.

[Shreyas Srinivas]

But that's essentially what lean elaborator does and the LSP lets you access

[Snir Broshi]

I interpret the request as asking for a lake exe ... that opens something like the infoview (plus ProofWidgets?) in a browser rather than using vscode-lean4. AFAICT the only issue is the cursor location. Perhaps something like Verso's output with clickable tiny ellipses between every tactic is the answer?

[Castedo Ellerman]

Shreyas Srinivas said:

But that's essentially what lean elaborator does and the LSP lets you access

I see no "But". Seems fine to me for a non-editting file-watching proof-state-outputting tool to call LSP. I am assuming we're talking about calling a Lean LSP server process of lake serve or lean --server).

I see that VSCodium automatically detects file changes and reloads source files. So as a strange extreme case, the "non-editting" tool can be VSCodium with the Lean extension merely opening a folder, not being used as an editor, only being used to see InfoView, and then the odd VS-hating user can use an independent editor that only supports plain standard LSP. The user changes files in their fav editor and VSCodium (not being used as an editor) automatically updates the InfoView. This is obviously is a bizarre work flow but it is illustrative.

So we could view a more ideal tool as the above bizarre solution with VSCode ripped out and only keeping the file-watching, LSP calling, and InfoView displaying functionality. I assume the Lean LSP server does not watch for file changes.

With a little bit more work I imagine the LSP server process can open a UNIX domain socket at a standard file path so it can be shared by separate editor and non-editor tool processes.

[Snir Broshi]

Snir Broshi said:

I interpret the request as asking for a lake exe ... that opens something like the infoview (plus ProofWidgets?) in a browser rather than using vscode-lean4. AFAICT the only issue is the cursor location. Perhaps something like Verso's output with clickable tiny ellipses between every tactic is the answer?

But given that the point is avoiding coupling, I guess that as long as this is technically easy to achieve (e.g. if the existing LSP accepts requests that move the cursor, plus can provide the current HTML/CSS/JS that should be displayed in the infoview on request) then that's already not coupled and satisfies the request

[Castedo Ellerman]

Snir Broshi said:

asking for a lake exe

To be "file-interactive" the tool needs to be able to watch/monitor file paths and update ouput when files change. A quick look at https://lean-lang.org/doc/reference/latest/IO/Files___-File-Handles___-and-Streams/ makes me think Lean IO does not support watching/monitoring files or that the Lean language would not be the right programming lanuage for the top-level process. But I'm not sure.

[Henrik Böving]

Just because its not in the standard library doesn't mean its impossible. If you only care about linux you could for example just bind inotify and do your thing.

[Malvin Gattinger]

This reminds me of some discussions about getting the InfoView to work with emacs, e.g. here - I never tried these things out but one of them seemed to run the infoview in the browser, maybe the methods used for that could help you too?

[Castedo Ellerman]

Malvin Gattinger said:

run the infoview in the browser, maybe the methods used for that could help you too?

Maybe. Assuming a non-editor file-watching tool does not already exist, one path I might go down is using those methods you point out: building something in TypeScript on top of lean4-info.

That said, my inclination, currently, is to go down a different path of building a minimalistic tool in Lean with as few extra dependencies as possible (apart from what Lean already requires, so no TypeScript/React/Node.js/etc...).

At the moment I'm focusing on learning more Lean, both at programming language and theorem prover, so I have a better appreciation and am less clueless about what is so valuable about InfoView. I also need to learn more about the LSP features in Lean at a low-level.

I am imagining a tool, built in Lean, that runs in parallel as a separate process with only very loose-coupling to an editor, merely sharing access to a file system access and a process running the Lean LSP server.

[Snir Broshi]

Castedo Ellerman said:

with as few extra dependencies as possible (apart from what Lean already requires, so no TypeScript/React/Node.js/etc...)

So you don't view widgets as part of Lean? Without React I think you won't get the "Try this" feature. I assume the neovim/emacs extensions have some workaround to support this, but surely this is a part of Lean itself.

[Castedo Ellerman]

Snir Broshi said:

Castedo Ellerman said:

with as few extra dependencies as possible (apart from what Lean already requires, so no TypeScript/React/Node.js/etc...)

So you don't view widgets as part of Lean?

No. But I'm happy to say "_____ Lean" if there is some commonly understood adjective for the Lean software that get installed by:

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

Without React I think you won't get the "Try this" feature. I assume the neovim/emacs extensions have some workaround to support this, but surely this is a part of Lean itself.

I'm not familiar with Widgets yet. I don't know what dependencies need to be installed to make these React-based Widgets work in a standard modern web brower.

In my mind there is very much a difference between "a Lean" installed by elan-init.sh and "a Lean" that requires the dependencies of a React app.

[Julian Berman]

How quickly do you want to find out what the results of searching for react give you in the core Lean repository ;)?

[Snir Broshi]

Castedo Ellerman said:

In my mind there is very much a difference between "a Lean" installed by elan-init.sh and "a Lean" that requires the dependencies of a React app.

It sounds like this was disproven

[Castedo Ellerman]

Julian Berman said:

How quickly do you want to find out what the results of searching for react give you in the core Lean repository ;)?

The point of your retorical question is unclear to me. Correct, there are references to React in the core Lean repository, yet "Lean" ≠ "https://github.com/leanprover/lean4".

Just to make sure we're all on the same page, the line

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

is from the Lean manual installation page. If there is some phrase of "_____ Lean" for that which is installed by elan-init.sh, I'm happy to use it.

In the absense of such a phrase, it make sense to me, for example, to say that the Lean GitHub Action "installs and uses Lean" even though it omits software required to enable React functionality.

[Castedo Ellerman]

Snir Broshi said:

It sounds like this was disproven

Incorrect.

[Castedo Ellerman]

We all agree there is functionality in the core Lean repository which depends on React. It should also be clear to all that elan-init.sh and the Lean GitHub Action does not install software that includes the requirements of a React app. In my mind, these are two examples of "Lean" that are very much different. I'm honestly confused what @Snir Broshi and @Julian Berman are trying to claim.

[Julian Berman]

I'm not sure a semantic discussion is very interesting -- but to clarify, I was making sure you were aware that Lean, which indeed is https://github.com/leanprover/lean4 (it's what's generally installed via elan, its version manager), has a dependency in its core repository on React when it comes to widgets, which are important language features. I haven't really made a claim personally -- I don't think a filesystem-event-based tool is very promising, or at least I don't know what one would want out of one that isn't either https://www.npmjs.com/package/@leanprover/infoview or https://github.com/leanprover-community/repl depending on how I'd interpret your requests above, but as I've said elsewhere, if you feel like building a tool that works precisely a way you have in mind, I'm certainly not one to tell you not to.

[Castedo Ellerman]

Julian Berman said:

Lean, which indeed is https://github.com/leanprover/lean4 (it's what's generally installed via elan, its version manager), has a dependency in its core repository on React when it comes to widgets, which are important language features.

@Julian Berman I'm a bit confused by this statement. In my containerized interactive shell environment I have Lean installed via elan. And then I have installed neovim and git cloned github.com/Julian/lean.nvim (and 'nvim-lua/plenary.nvim').

I have not installed any software that supports JavaScript doing import * as React from 'react'.

The lean.nvim README says it has

 infoview which can show ... interactive widget support (for most widgets renderable as text)

So lean.nvim is showing widgets without React, correct? so React is not a dependency for most widgets renderable as text, correct?

[Julian Berman]

Perhaps an analogy: imagine you're writing a web browser. A user using your thing can visit a web site, and the code of that website tells your browser "execute this JS and render this CSS". If you write a browser that doesn't do those things, of course you'll do nothing with the thing the site is asking to make happen.

Lean (including core parts of it, with no third party dependency involved) includes pieces which tell your editing environment "run this react code" during certain interactions. Concretely: some RPC responses contain bits of JS you are "supposed to" execute with certain dependencies installed.

And yes lean.nvim does not do so (it does not embed a JS engine, though who knows, some day it may optional support doing so to get full support). Instead in my analogy it does the equivalent of if your home grown web browser tried to introspect the JavaScript that is supposed to execute and when it thinks it knows what's supposed to happen it invokes an internal reimplementation of what that JS would do to the DOM.

Again to me it's not very interesting to debate whether one should call an editor environment that doesn't support feature X of Lean still "Lean", but I did feel like +1ing Snir's point that widgets exist and make sure to mention that a large majority of Lean's current user base use and rely on them.

[Castedo Ellerman]

Julian Berman said:

Concretely: some RPC responses contain bits of JS you are "supposed to" execute with certain dependencies installed.

Wow! That is unexpected. I had no idea. Good to know, thanks!

Julian Berman said:

Snir's point that widgets exist and make sure to mention that a large majority of Lean's current user base use and rely on them

Yep, we are all on the same page that this is true.

[Castedo Ellerman]

Julian Berman said:

if you feel like building a tool that works precisely a way you have in mind, I'm certainly not one to tell you not to.

I actually prefer not building this tool and prefer finding out someone else has built it or is building it. And it looks like I'm luck! @Willem vanhulle is creating "Lean-TUI": https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Lean-TUI.20.28self-contained.20infoview.29/with/569977578

Lean-TUI sounds like it is an "editor-decoupled proof-state-outputing tool" that is achieving the effect of "file-watching" although differently than I imagined. It is file-watching I think by sharing the same Lean LSP process with an editor. That sharing I imagine is also very good for memory usage too. I will try Lean-TUI and confirm. Sounds very promissing @Willem vanhulle and makes much more sense to me that doing tight-coupling between Lean and specific editors. Loose-coupling between editors and language is the main point of LSP.

Julian Berman said:

I don't know what one would want out of one that isn't either https://www.npmjs.com/package/@leanprover/infoview or https://github.com/leanprover-community/repl

In those repos I don't see any file-watching CLI tool ... like Lean-TUI.

[Willem vanhulle]

Thanks for mentioning my project. Indeed, it is early stage, but i already published a pre-release that is easier to test here https://crates.io/crates/lean-tui
screenshot.png

[Castedo Ellerman]

So far Lean-TUI seems like a promising approach. However it does not take advantage of React. So I a presume there are certain widget features that will be missing from Lean-TUI. I'm hoping I can help document missing functionality.

There is a 2nd approach which is to output proof-state via a local web server that serves a React app that can support Lean widgets. It most likely would use https://www.npmjs.com/package/@leanprover/infoview. As a placeholder name we can call it Lean-LocalWebApp. When run as an LSP client, it would run much like lean-tui proxy. But rather than opening a local UNIX domain socket ~/.cache/lean-tui/lean-tui.sock it instead opens a local TCP/IP port for HTTP, much like Jupyter Notebook and many others. A user opens http://localhost:12345 with their web browser rather than a 2nd terminal window running lean-tui view.

[Willem vanhulle]

Castedo Ellerman zei:

HTTP, much like Jupyter Note

That should not be too hard to accomplish. The program is decoupled. You need replace the bridge between the TUI and proxy in https://codeberg.org/wvhulle/lean-tui/src/branch/main/src/tui_ipc

[Castedo Ellerman]

Here are updates to my previous statements, beliefs, and plans based on y'all's insights, especially @Willem vanhulle for demonstrating a novel approach in https://crates.io/crates/lean-tui that had not occured to me. Thank you!

Castedo Ellerman said:

Thomas Murrills said:

do any of them have any access to the editor state?

No, no editor state. However, some of these file-watching tools parse source files ...

how do you envision choosing which proof state to display?

By whatever means is loosely coupled from the editor. :smiley:

I correct myself: yes, there is editor state. There is tight coupling to the Lean LSP messages of lake serve but not to the editor, which can be any editor with generic LSP support.

I was originally imaginging "file-system-watching". But the approach @Willem vanhulle takes with Lean-TUI of "editor-file-watching" seems much more promissing and valuable. One run mode of Lean-TUI is as an LSP proxy. It does "editor-file-watching" by intercepting the LSP messages between editor and lake serve.

Julian Berman said:

... -- I don't think a filesystem-event-based tool is very promising, ...

I agree that a filesystem-event-based tool as I originally imagined is less promissing than the LSP proxy approach @Willem vanhulle has taken with Lean-TUI.

[Snir Broshi]

btw I found #general > InfoView in a Web Browser? and #lean4 > need help setting up lean4-infoview which seem to be the same request but older

[Castedo Ellerman]

Based on looking at all these links, including those, and reflecting on what I've learned so far. I think I see some novel approaches via external web browser that would work with any LSP editor. I figured I would start sharing these ideas once I get a little bit better informed about a lot of Lean stuff and when there's an "Editors" channel here on Zulip to start new topics not in "general".