lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

Emscripten support

Open leodemoura opened this issue 4 years ago • 3 comments

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.

leodemoura avatar Apr 13 '21 23:04 leodemoura

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.

Kha avatar Apr 14 '21 07:04 Kha

Initial build support, but no editor integration yet: https://github.com/leanprover/lean4/pull/505

Kha avatar Jun 12 '21 15:06 Kha

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

Anderssorby avatar Jan 05 '22 23:01 Anderssorby