Today I was thinking about how easy it is to include Lean into a website.
Since it compiles via an intermediate C layer, it shouldn't be _that_ hard to do this via Emscripten, but apparently it's harder than that: Since there's `#eval`, every function of the language needs to be exported per default (only then it's really a full Lean compiler), and that apparently hit a limit for the number of imports and exports a WASM program(?, module?) allows.
That has been increased since then, but now there's other issues.
Wild.
# Notes
# Links
- Lean 4 | wasm build | Zulip team chat
- Lean 4 | lean.js | Zulip team chat
- GitHub - T-Brick/lean2wasm: Tool for compiling Lean to WASM · GitHub (shouldn't work right now, if the lean.js thread is right)
Today, I had a short research spree on the state of Lean->Wasm compilation. Pretty interesting!
#Lean #Wasm