web editor

Stream: lean4

[Kevin Buzzard]

How far away are we from a Lean 4 web editor? I'm thinking about making Lean 4 gamey teaching tools and right now installing Lean 4 is not a reasonable option for a wide class of mathematicians.

[Kevin Buzzard]

Note: I'm not in any hurry! Everything still needs a lot of work at my end.

[Sebastian Ullrich]

We're at least much closer thanks to @Wojciech Nawrocki's work on compiling Lean 4 to Wasm. However, someone would still have to compose the Wasm-compiled Lean server with e.g. the Monaco web editor. Afaik that hasn't been done before, all previous work is about connecting a web editor to a language server running on some, well, server somewhere else, Gitpod-style.

[Mac]

Since Lean 4 has a VSCode extension, one could probably use an existing web IDE that supports VSCode extension like Eclipse Che / Theia.

[Marc Huisinga]

This is what Sebastian meant with the Gitpod-style, which already supports VSCode in the browser in the same manner as Eclipse Theia. We already use that for the theorem prover lab. The Lean 3 web editor runs entirely in the browser, including the language server.

@Kevin Buzzard
This is the link to the gitpod version of the theorem prover lab: https://gitpod.io/#https://github.com/IPDSnelting/tba-2021
If your only goal is avoiding that people need to install Lean 4, this should be sufficient (up to 50h/month) and you should be able to copy the gitpod config files (.gitpod.Dockerfile and .gitpod.yml) from the github to set up your own: https://github.com/IPDSnelting/tba-all
To build an actual gamey teaching tool, we'd likely need a Monaco editor in the sense of Lean 3.

[Marc Huisinga]

Shoot, let me fix the links

[Wojciech Nawrocki]

With the LSP server architecture relying on the ability to spawn isolated processes, for a web editor I think at least a version of IO.Process.spawn which creates a WebWorker would have to be implemented.

[Gabriel Ebner]

There's also the brutal method of just starting the file worker directly (since the web editor only has a single file anyhow).

[Wojciech Nawrocki]

That could also work! One would probably have to adapt the worker somewhat, e.g. to do the full LSP initialization

[Mac]

Marc Huisinga said:

This is what Sebastian meant with the Gitpod-style, which already supports VSCode in the browser in the same manner as Eclipse Theia. We already use that for the theorem prover lab. The Lean 3 web editor runs entirely in the browser, including the language server.

In fact, if I am not mistaken, Gitpod uses Theia itself. I was just a little confused by Sebastian's statement about the web editor connecting to a language server somewhere else. But I guess I just misunderstood.

[Marc Huisinga]

Gitpod uses Theia itself

Gitpod did originally use Theia by default, but they switched to VSCode a few months ago. In fact, the Lean 4 extension does not work with Theia, only VSCode.

I was just a little confused by Sebastian's statement about the web editor connecting to a language server somewhere else. But I guess I just misunderstood.

You're not misunderstanding that, that's what all these fully-fledged IDEs (like Gitpod) do, see e.g. the architecture overview of Theia. The language server does not run in the web browser, but on the corresponding host. The Monaco setup of Lean 3 works differently.

[Gabriel Ebner]

Marc Huisinga said:

The Monaco setup of Lean 3 works differently.

lean-web-editor indeed runs a WASM version of Lean in the browser. But this has nothing to do with using Monaco as an editor. We could also run Lean on a server somewhere and connect it to Monaco via websockets or sth (just like gitpod).

[Mac]

Marc Huisinga said:

You're not misunderstanding that, that's what all these fully-fledged IDEs (like Gitpod) do, see e.g. the architecture overview of Theia. The language server does not run in the web browser, but on the corresponding host. The Monaco setup of Lean 3 works differently.

Ah, I see this is a terminology problem. When I hear web editor, I interpret that to mean the server that hosts the editor (where the language server is also running), I don't think of the web app client running in the browser. So I think of the web editor and language server as being collocated on the host without regard for the browser, hence my confusion.

[Mac]

Marc Huisinga said:

In fact, the Lean 4 extension does not work with Theia, only VSCode.

Oh! Do you (or @Gabriel Ebner) happen to know what the road block to supporting Theia is?

[Marc Huisinga]

Actually, I'd like to state that in a weaker form; Theia on Gitpod did not work together with the Lean 4 extension. I vaguely remember that this was somehow due to semantic highlighting, for which Theia has added support long ago, so maybe Gitpod was just running an older version.

[Kevin Buzzard]

How far away are we from a hopefully non-sluggish web interface to Lean 4?

[Taro Naoi]

Hello, I’m interested in running Lean 4 in a browser-based editor like Monaco. It sounds like Lean 4 is much larger than Lean 3 (original question for context: https://github.com/leanprover/lean-client-js/issues/43). Does this rule out the possibility of running Lean 4 client-side and would require hosting of Lean 4 in some kind of server and creating a client-server connection via something like websocket? I'm fine with putting in the work to make it happen, just wanted to know if this is the most viable approach before I go down the rabbit hole.

[Henrik Böving]

I would say we mostly just don't know yet? Lean does compile to C which we could probably get to compile to WASM for a web browser if we wanted to so it might be possible, might also be too big.

[Henrik Böving]

Though according to the thread @Wojciech Nawrocki seems to be the person for this

[Leonardo de Moura]

Does this rule out the possibility of running Lean 4 client-side and would require hosting of Lean 4 in some kind of server and creating a client-server connection via something like websocket?

No, it does not. @Wojciech Nawrocki already managed to compile Lean 4 into javascript using emscripten. The current Lean 4 binary is much bigger than the Lean 3 one, but this is due to an issue in our current code generator. It is too aggressive in inlining local functions. We are planning to address this issue when we rewrite the code generator in Lean.
For having Lean in the browser using Monaco, we still need the LSP client part. As @Henrik Böving pointed out , @Wojciech Nawrocki is the best person to answer this question.

[Wojciech Nawrocki]

It has been a while since I looked into this and thoughts scattered, but I can attempt to summarise the state of things.

• Having browser-based Monaco connect to a Lean 4 server hosted on a native CPU somewhere already works on various platforms, for example on Gitpod. To implement this yourself I imagine you would have to duplicate some of the work Gitpod did, but it demonstrably works.
• When we are talking about running Lean 4 itself in the browser, we have to disambiguate what we mean. There are two distinct modes of operation to get running — the batch compiler, i.e. the lean you would run on the command line, and the server, invoked with lean --server. We use the same binary (lean) to run both, but they are really quite different applications. Moreover there are at least two possible compilation targets, namely WASM with the Emscripten runtime, and WASM with a custom runtime (a bit lower-level, kind of like WASI).

In lean4#505, I got the batch compiler working with Emscripten runtime, but it has some issues.

• It is slow to load and to execute. I think this is surmountable with engineering effort, but I don't know how much effort. Here are some issues I identified:
  • Lean assumes a POSIX-like environment with blocking open/read for files which does not fit the web. On the web, you really want to load things asynchronously. This may require explicit support in the Lean runtime.
  • The Lean kernel (and maybe other parts, but mostly the kernel) relies on exceptions for control flow. At the time of my experiments, exceptions were not natively supported in WASM, and would instead work through a hack in the Emscripten compiler which jumps from WASM to JS every time an exception is raised, causing both runtime and code size overhead. But it looks like the exception extension is now supported in major browsers, so this may be easy enough to dispose of.
• WASM is currently a 32-bit platform. Consequently, WASM-Lean cannot load "standard" 64-bit .oleans compiled by a 64-bit native Lean binary. So the .oleans must be either made platform independent (this is not great since the naïve implementation increases importing overhead on 64-bit platforms, whereas a more complex implementation would be, well, more complex), or they must be built by a 32-bit Lean (e.g. by WASM-Lean running in Node.js). The 64-bit WASM extension is not widely supported as of now.

Then supposing we wanted compile the server for Emscripten (in order to have purely browser-based LSP support), there are additional things to do:

• The server heavily relies on threads to carry out concurrent processing. This also has changed since the lean4#505 experiments, since back then we had to rely on the Emscripten runtime, whereas now it looks like WASM threads are widely supported. But their execution semantics are specific to the web and would also need special support in the Lean runtime.
• Besides threads, the server uses POSIX processes (one "watchdog" process managing a "worker" process for each open file). One option suggested by Gabriel above would be not do it and only start one worker. This would limit us to a single open file (fine in games like NNG), and maybe to a static list of imports (we rely on the process restarting when the imports change; it might be possible to do away with this with some hacks when only one file is open), but might work easily enough with a modified watchdog. For full-featured support, we'd need code in the Lean runtime for launching WebWorker-based processes.

Lastly let me mention the Emscripten-less variant where we compile to WASM without Emscripten and implement our own JS runtime for things like opening files. This might improve performance as Emscripten can be heavyweight, but would be harder to get working.

So the short story is, back in 2021 WASM-Lean was not very feasible due to lack of browser support for the exceptions and threads WASM extensions. These are supported now so it seems possible, but would be a bit of work, mostly adding things to the Lean runtime.

[Matthew Ballard]

I just wanted to check in here and see if the status of a Lean 4 web editor has changed since May.

[Sebastian Ullrich]

It hasn't

[Matthew Ballard]

A possible alternative is post up a machine with the (official) VS Code Server, assuming I get access, and an install of Lean 4 . Wrap it in some auth.

[Tom]

Alternatively, VS Code has the "Remote-Container: Try a Development Container Sample...". Perhaps if there were someone that works at MSFT, they could do some convincing to have that container added to the sample repo :smirk:

[Sebastian Ullrich]

It looks like someone has managed to get an in-browser language server to work: https://www.hiro.so/blog/write-clarity-smart-contracts-with-zero-installations-how-we-built-an-in-browser-language-server-using-wasm

[Floris van Doorn]

From any GitHub repository, it’s possible to press “.” to open and edit a project in VS Code for the web.

whoa!