Has Lean 3 emscripten builds tested on emscripten ≥ 2?

Stream: general

[Ryan Lahfa]

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]

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

[Ryan Lahfa]

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]

(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 :>)