Zulip Chat Archive

Stream: general

Topic: Has Lean 3 emscripten builds tested on emscripten ≥ 2?

Ryan Lahfa (Aug 20 2021 at 14:11):

I'm trying to reproduce Lean 3 emscripten builds with emscripten ≥ 2 toolchain, but I am having a lot of difficulties (mainly because emscripten has very difficult constraints on LLVM / Binaryen versions).

I wanted to understand if Lean 3 WASM builds were built under which version, reading the CI code leads to this Docker image: https://hub.docker.com/r/trzeci/emscripten with the tag sdk-incoming-64bits, so I suppose this host an emscripten 1.X.Y toolchain?

Is anyone able to compile the builds using a recent emscripten? Thanks!

Ryan Lahfa (Aug 20 2021 at 14:15):

Precisely: CC="/emsdk_portable/emscripten/tag-1.38.43/emcc"

Ryan Lahfa (Aug 20 2021 at 20:31):

FWIW, I have setup'd some code to build emscripten bundles from Nix: https://github.com/RaitoBezarius/nixexprs/blob/master/pkgs/science/lean/emscripten.nix but unfortunately, the emscripten toolchain seems to be broken on nixpkgs for now, so I cannot get any bundle :-).

Ryan Lahfa (Aug 20 2021 at 20:32):

(but with this, once it's fixed, it should be possible to produce any JavaScript WASM/JS files for any version of Lean, put it in a CI and cache it, then produce any kind of Lean 3 game, put it in a CI, then cache it :>)

Last updated: Aug 03 2023 at 10:10 UTC