what is lean.js

Stream: general

[TongKe Xue]

Can someone please tell me what https://github.com/leanprover/lean4/blob/master/doc/make/emscripten.md is meant for ?

1. I have followed the (regular) build instructions via

nix develop
21613  cmake --preset release
21614  make -C build/release -j56
21615  make -C build/release -j200

and everything went fine

2. I am under the impression that lean4 does not compile to wasm32 yet (i.e. this is why the lean4web / lean game server uses a x86_64 server instead of running all in Chrome/wasm32)

question: what is this lean.js, and what are the emscriptsen build instrs for?

Thanks!

[Markus Himmel]

Lean had a wasm32 build until v4.15.0 (see for example the list of assets at https://github.com/leanprover/lean4/releases/tag/v4.15.0), but we ran into an Emscripten limitation which would have taken a lot of engineering effort to overcome, and we decided to drop the WebAssembly target for the time being. So the current status is that the WebAssembly target is still in the code, but in a broken state. Whether it will come back depends on whether there is a use case for a WebAssembly target that is important enough to justify the significant investment to bring it back and keep it running (this is a very high bar).

[TongKe Xue]

Thank you for the informative historical insight. Could you expand a bit more on

but we ran into an Emscripten limitation which would have taken a lot of engineering effort to overcome, and we decided to drop the WebAssembly target for the time being

My background is: (1) I just recently got the lean4 github code to build locally (on x86_64), (2) I I have some familiar with wasm32, not via emscriptsen, but Rust.

I'm curious is the issue: 4GB memory limit ? This appears to be resolved in https://spidermonkey.dev/blog/2025/01/15/is-memory64-actually-worth-using.html (never tested this myself).

Digging around github issues, I found https://github.com/leanprover/lean4/pull/2599 , where the claim seems to be "wasm32 makes CI tests really slow"

I'm curious if you could share what the Emscriptsen limitation is (or point me to the github issue). Thanks!

[Markus Himmel]

The problem was that the build used EXPORT_ALL and we exceeded the limit of 10000 exported symbols (not sure whether this is an emscripten or wasm-ld limitation)

[TongKe Xue]

1. I currently reproduce the "10,000 export limit error yet"

doc/make/emscripten.md says:
mkdir -p build/emscripten
cd build/emscripten
emconfigure cmake ../../src -DCMAKE_BUILD_TYPE=Emscripten
make lean_js_js lean_js_wasm

however, running the emconfigure cmakeline, I get

emconfigure cmake ../../src -DCMAKE_BUILD_TYPE=Emscripten
error: use `emcmake` rather then `emconfigure` for cmake projects

changing to emcmake, I get

emcmake cmake ../../src -DCMAKE_BUILD_TYPE=Emscripten
configure: cmake ../../src -DCMAKE_BUILD_TYPE=Emscripten -DCMAKE_TOOLCHAIN_FILE=/nix/store/202rpslcjhwax183ahrf54xf46kvp1li-emscripten-4.0.10/share/emscripten/cmake/Modules/Platform/Emscripten.cmake -DCMAKE_CROSSCOMPILING_EMULATOR=/nix/store/ijsy113yzy0mpcr1sf0773nz9v0r7hff-nodejs-22.17.1/bin/node
CMake Error at CMakeLists.txt:8 (message):
  STAGE must be set; use the CMakeLists.txt in the root folder

changing to

emcmake cmake ../../src -DCMAKE_BUILD_TYPE=Emscripten  -DSTAGE=0

I get an error about not finding mimalloc.h (still sorting this out)

Setting aside those issues: do we actually need export_all ? Intuitively, I feel there is a very small number of lean4 wasm fns we need to expose to js. The exported fns need to be able to call non-exported fns, but it is not clear to me at all why we need to export all fns.

This shows my lack of understanding of lean4 internals: could you enlighten me on why we need to export all lean4 fns? Intuitively, it seems we only need to export a few for repl, type checker, lsp, ...

Thanks!

[Markus Himmel]

Well, a Lean program can do import Lean and then it has access to literally the entire Lean codebase, so all of that needs to be available.

But like I said, this problem isn't insurmountable. It's just not that high on the priority list.

[Max Nowak 🐉]

A naive solution would be to only export the necessary symbols, right? Do you have links at hand to prior discussion on those limitations? If not, I'll find it myself. I might spend a weekend playing around with this.

[TongKe Xue]

Again, this is due to my lack of understanding of Lean internals/fundamentals:

Markus Himmel said:

Well, a Lean program can do import Lean and then it has access to literally the entire Lean codebase, so all of that needs to be available.

But like I said, this problem isn't insurmountable. It's just not that high on the priority list.

My understanding is that import Lean needs to expose those symbols to the Lean REPL/Editor. It is not clear to me why this implies the same symbols need to be exposed to the Wasm/JS FFI Boundary.

My current mental model (which is probably wrong -- and I would appreciate knowing where I'm wrong) would be this analogy: Suppose we wanted to get Emacs + ELisp to run in Chrome/wasm32:

1. We need to export a few emacs/elisp fns to Wasm/JS boundary.
2. We do not need to expose every elisp fn to to the Wasm/JS boundary.
3. And being able to call a elisp fn inside a scratch buffer does NOT imply we can also call the elisp fn directly from js.

My (current) mental model is that this argument would also apply to the import Lean case above: being able to refer to a theorem / fun / def in the Lean editor/repl does NOT imply that we need to expose it to the wasm/js FFI boundary.

Could you let me know where I'm wrong (or point me at the docs I can read up on this) -- it's clear I'm misunderstanding something about the way Lean Editor/Repl <-> wasm32 interaction works, but it's not clear to me where my understanding is.

Thanks!

[Markus Himmel]

I guess I was thinking about what would happen if you #eval something, i.e., how the interpreter finds the native implementation of a function defined in core. But the truth is that I don't know the details of how this works, both on the "traditional" platforms and on WebAssembly, so it's very possible that there isn't any problem.

It would definitely be great to see a working build of a recent Lean that doesn't need the export_all.

[Sebastian Ullrich]

The interpreter will use exported symbols to jump into native code. It doesn't need an exported symbol for every single Lean function if you don't call it or can live with the interpretation overhead, but now you're in the business of designing a new heuristic for what to export to it and what not.

[TongKe Xue]

The interpreter will use exported symbols to jump into native code.

I'm clearly misunderstanding something here. Let's see what I'm doing wrong. So my background is that I have a Rust/wasm32 app running in Chrome. It's about 100k loc of Rust, and I think I expose a total of 2 functions. func1 = after wasm is loaded, it calls an init fn; func2 = sometimes from the JS dev console, I want to send the Rust code a msg. Literally 2 functions exposed from wasm to JS. (No exposed fns for keyboard/mouse/postmessage callbacks; Rust creates an anon closure on the fly and registers it with JS land).

So now let's talk about something like https://live.lean-lang.org/ . Right now, it has a websocket to some x86_64 server running "lake serve bunch of options" from https://github.com/leanprover-community/lean4web/blob/main/server/bubblewrap.sh#L45

Now, let's imagine an alternative world, where instead of

1. "lean4web client" <-> websocket <-> "x86_64 server: lake serve", we did
2. "lean4web client" <-> postmessage <-> "chrome webweworker: lean4/wasm" ; post msg here referring to https://developer.mozilla.org/en-US/docs/Web/API/Window/postMessage

Intuitively to me, it seems the "lean4/wasm in Chrome webworker" needs to expose the same number of fns as the "x86_64 server: lake serve" -- i.e. a single fn for processing window.postMessage instead of websocket msgs.

Now, clearly, I'm misunderstanding something. What am I getting wrong? :-)

[TongKe Xue]

In short, ignoring lots of low level details:

Naively, if we tried

1. started with "lake serve --"
2. replaced websocket w/ handling window.postmessage
3. only exposed the fn for handling window.postmessage
4. what breaks down?

Context: I just realized. I never stated my XY problem. I'm trying to build something in Rust + http://egui.rs (running in Chrome) that talks to lean4 (running in a Chrome webworker), as a potential alternative to the standard lean4web client UI.

[Eric Wieser]

My guess is that we need to export the functions via webassembly, because this happens to export them in a way that emscripten's implementation of dlsym (which the Lean interpreter uses) can load

[Eric Wieser]

As far as I can tell 10000 symbols was an old chrome limitation, but perhaps the bottleneck is somewhere else, or Markus Himmel elided a zero

[TongKe Xue]

I repeated "10k" somewhere up there. Turns out, the limit appears to be 100k: (unless bottleneck elsewhere).

https://www.w3.org/TR/wasm-js-api-1/#:~:text=The%20maximum%20number%20of%20exports%20declared%20in%20a%20module%20is%20100000.

[Snir Broshi]

AFAICT Chrome's limit is 1M exports, and it was never 10k
https://chromium.googlesource.com/v8/v8/+/fd3b8616dbc6115c8e0536d5adbeb2c8863c8bca/src/wasm/wasm-limits.h#33

[Markus Himmel]

Sorry, that was a typo on my end. It's 100k. Here is an excerpt from one of the error messages we observed:

1/5 Test #1070: leanruntest_ac_rfl.lean ..........***Failed    1.95 sec
failed to asynchronously prepare wasm: CompileError: WebAssembly.instantiate(): exports count of 100019 exceeds internal limit of 100000 @+279585
Aborted(CompileError: WebAssembly.instantiate(): exports count of 100019 exceeds internal limit of 100000 @+279585)
/home/runner/work/lean4/lean4/build/stage1/bin/lean.js:1

[TongKe Xue]

This shows my utter lack of emscriptsen knowledge (though I've done quite a bit of Rust + wasm32; involving webworkers + postmessage).

Why can't we stuff lake serve -- in a webworker, have it use window.postMessage instead of tcp/websockets, and thus on the wasm side, only have to "expose 1 function" ?

I apologize for my ignorance here -- why do we need to expose 100k fns? (I think the previous argument was "so the repl can make fn calls"); but if we just stuff all of lake serve -- as a single binary blob, it seems if we change the tcp/websocket to use postmessage (and run in a separate webworker), JS would not need to have access to all 100k exported fns.

[TongKe Xue]

PS: I'm not in anyway suggesting the above is easy. I'm trying to debug my ignorance of why we need to export 100k fns, instead of just the fn lake serve -- needs to support its tcp/websocket. Naively, this lake serve -- network protocol seems like the perfect place to draw the wasm/js ffi boundary (for the sake of having a web lean4 repl).

[Henrik Böving]

A lean server process can be coerced to call any of those 100k+ functions through #eval so they need to be exposed

[Markus Himmel]

To spell it out a bit more: the problem isn't at the boundary between lake serve and the repl, the problem is what lake serve needs to do to answer the requests it receives from the repl. lake serve needs to be able to execute arbitrary Lean programs, which may call arbitrary library functions.

[TongKe Xue]

Clearly I am misunderstanding something very fundamental/basic, but I still don't understand this.

1. I have Rust projects that are 100,000+ loc, running wasm32. I only need to expose < 10 Rust fns to js. Rust fns calling rust fns do not require them to be exposed to js.

2. I can embed Python (https://crates.io/crates/rustpython) or lua (https://crates.io/crates/piccolo) interpreter in them -- and again, I only need to expose a websocket/postMessage

3. I feel like I'm missing something very very basic here. Why is it, for a Lean4 repl, it does not suffice to just expose a bidirectional json msg port of sorts? Why is it that these Lean4 fns must be exposed from wasm to JS ?

Again, I'm sorry for such a stupid question. I feel like I'm misunderstanding something very very basic here. I don't understand why "lean repl needs to be able to call X" implies "X has to be exposed from wasm to js".

[Markus Himmel]

The special thing about Lean is that is has this slightly unique model where it is both a compiled and an interpreted language. When you send #eval someFunction to the Lean server it calls the interpreter on someFunction. The interpreter will check if it finds a compiled version of someFunction. If it finds it, it will jump into that native code. Otherwise, it will interpret someFunction, which in turn might call more functions, for which it will then again do the same thing of first looking for a compiled version and otherwise interpreting.

The "using the native version if available" step is the problem. It will only work if the native code is available as an exported symbol.

[TongKe Xue]

1. I was definitely ignorant of this dual compiled-code/interpreter structure. Thank you for clarifying that. Is there documentation I can read up on this ?

2. On x86_64 Desktop, when I am editing in VSCode, is the Lean4 server doing dynamic code generation? Either via JIT or building a .so and doing dlopen?

3. To the best of my knowledge (which is not very strongly held beliefs), wasm neither (1) supports JIT nor (2) supports dlopen. AFAIK, wasm blobs communicate via postmessage or sharedarraybuffer. Does this mean that technically, for the wasm build, we know, at compile time which fns have "native version", and which fns not? So in very wild theory hypothetical world for wasm32 builds, we could just hard code the jumps at compile time, and not have to export the fns. If this is true, is it also the case we're not doing this because it would heavily complicate / almost "fork" parts of the codebase, as the x86_64 and wasm32 would behave very differently for building/linking/calling fns?

4. Purely out of curiosity, if we just went "all interpreter, no native code" how bad would the performance hit be? (10x? 100x?) I think the most common "lean4 in Chrome" use case is a basic editor + some toy problems (probably not even loading up all of Mathlib) for educational / demo purposes.

Thank you for taking your time to clear up my incorrect assumptions. I appreciate it. :-)

[Markus Himmel]

I'm not aware of any documentation beyond the module doc at https://github.com/leanprover/lean4/blob/0173444d24df9253d7947cfe82519e4a6caffd3a/src/library/ir_interpreter.cpp#L7.

[Henrik Böving]

Purely out of curiosity, if we just went "all interpreter, no native code" how bad would the performance hit be? (10x? 100x?) I think the most common "lean4 in Chrome" use case is a basic editor + some toy problems (probably not even loading up all of Mathlib) for educational / demo purposes.

usually 10x

[TongKe Xue]

Different question (but perhaps it hits same limitation).

Instead of compiling the LeanREPL into wasm32, I have a program written in Lean (say InsertSort), and I want to compile this lean program to wasm32. Is this possible, or would this also hit the 100k export limit?

My intuition is:

1. lean will emit InsertSort.c
2. we need to use emscriptsen and somehow link vs (1) Lean cpp runtime and (2) libraries the cpp runtime depends on (big number libraries + ...)

Is there a tutorial for doing this somewhere? I want to do:
input: InsertSort.lean
output: some wasm module I can run in Chrome32 and call via JS

Thanks!

PS: If bundling lean runtime itself does not hit 100k limit, what hits the 100k limit in the LeanREPL case? Something like MathLib or something else ?

[Snir Broshi]

Markus Himmel said:

Sorry, that was a typo on my end. It's 100k. Here is an excerpt from one of the error messages we observed:

1/5 Test #1070: leanruntest_ac_rfl.lean ..........***Failed    1.95 sec
failed to asynchronously prepare wasm: CompileError: WebAssembly.instantiate(): exports count of 100019 exceeds internal limit of 100000 @+279585
Aborted(CompileError: WebAssembly.instantiate(): exports count of 100019 exceeds internal limit of 100000 @+279585)
/home/runner/work/lean4/lean4/build/stage1/bin/lean.js:1

Well in that case it was 100k previously, and a year ago it was bumped up to 1M
https://chromium.googlesource.com/v8/v8/+/285bfe195f7918f623ee6d0f138774ec003f2262%5E%21/#F0

Does that mean wasm Lean is viable right now? (at least until Lean bypasses that increased limit)