lol another WASM question

Stream: lean4

[Huỳnh Trần Khanh]

ok so this is another WASM question and you might think in your head oh why does this guy love WASM so much. is Lean 4 significantly faster than Lean 3 on WASM? in the future I might package Lean 4 for use on the web because why not :joy: Lean 3 can be annoyingly slow on WASM sometimes

[Huỳnh Trần Khanh]

if Lean 4 is still slow on WASM I might need to consider other approaches, for example running Lean 4 on a server with appropriate sandboxing

[Mario Carneiro]

It will probably be faster for builtin stuff and about the same for interpreted stuff. But WASM may significantly complicate the bootstrapping/plugin situation for libraries like mathlib that depend on compiled tactics

[Wojciech Nawrocki]

@Huỳnh Trần Khanh it depends on what you mean by "Lean 4 on WASM". We recently added an Emscripten build which can run under Node.js. Precise benchmarks TBD, but it is currently slower than native. However there is lots of optimisation work specific to Emscripten to be done. What is your intended use-case for "Lean4 on the web"? A build that will be usable in the browser as a library is WIP. But there are no immediate plans for running the LSP server in browsers (although it would be cool). Also we require the Emscripten runtime. A standalone/WASI build is not planned.

[Wojciech Nawrocki]

WASM may significantly complicate the bootstrapping/plugin situation for libraries like mathlib that depend on compiled tactics

Amazingly enough, the Emscripten people implemented a (admittedly simple, but good enough) dynamic linker, so we can load dylibs/plugins.

[Ryan Lahfa]

Wojciech Nawrocki said:

Huỳnh Trần Khanh it depends on what you mean by "Lean 4 on WASM". We recently added an Emscripten build which can run under Node.js. Precise benchmarks TBD, but it is currently slower than native. However there is lots of optimisation work specific to Emscripten to be done. What is your intended use-case for "Lean4 on the web"? A build that will be usable in the browser as a library is WIP. But there are no immediate plans for running the LSP server in browsers (although it would be cool). Also we require the Emscripten runtime. A standalone/WASI build is not planned.

Is this public? I'm interested, I was planning to tackle the WASM Lean 4 issue but didn't had any time to fix it

[Sebastian Ullrich]

https://github.com/leanprover/lean4/pull/505

[Xubai Wang]

Wojciech Nawrocki said:

A standalone/WASI build is not planned.

Why is that? It seems Emscripten does not provide more functionality than WASI (thread is unavailable in both), and many languages prefer standalone (rust) or wasi (swiftwasm, tinygo). Also WASI is the WebAssembly standard.

[Xubai Wang]

Also in lean 3 Emscripten compiles the whole lean program into lean.js and lean.wasm. What can I do if I just want to compile a single lake project?

[Sebastian Ullrich]

It seems Emscripten does not provide more functionality than WASI

I don't think that's true, Emscripten supports C++ exceptions that Lean uses. But I don't think the stdlib implementation needs them, so building a standalone Lean 4 program against WASI might be possible.

[Xubai Wang]

Oh yes, exception for WASM is still in proposal stage :upside_down: (WASI will have hope when all C++ stuff is moved to Lean).