Emscripten support
Lean 3 can run on the web browser. The code is compiled into javascript using emscripten https://emscripten.org/ We need this feature in Lean 4 to be able to have interactive documentation again.
A note for people stumbling upon this issue: for our Lean 4 course at KIT, we have had good experience (so far) with using Gitpod in effectively the same manner. But since this is using somebody else's infrastructure using limited accounts, it is not a proper solution.
Initial build support, but no editor integration yet: https://github.com/leanprover/lean4/pull/505
What is the status of this? I'm guessing this is not supported in the nix build and removed from the CI? I'm interested in getting this to work (in nix). Is it enough to run:
emcmake cmake ../..
emmake make -jN