Any plans for supporting wasm-compiled Lean 4 servers?

[tnaoi]

Just wondering if there are any current efforts to enable interfacing with a wasm-compiled lean 4 server.

[gebner]

Note that this library is for Lean 3. Most of the code here deals with the Lean 3 server protocol and has nothing to do with webassembly. (And so any potential Lean 4 webassembly wrapper won't be here so I will close this issue as it is out-of-scope.)

There has been some work on compiling Lean 4 to webassembly, see leanprover/lean4#398 and leanprover/lean4#505 Please come to https://leanprover.zulipchat.com/#narrow/stream/270676-lean4 for further discussion.

I'm not sure if we can ever use webassembly to run Lean 4 in the browser though. The native build of Lean 4 is already several hundred megabytes large, this is pretty infeasible to ship over the web.