reproducing lean4 wasm32 build of 100k export error

Stream: general

[TongKe Xue]

Currently, I can not even reproduce the lean4 wasm32 100k export error. Here are my build attempts

1. x86_64 build of lean4 from git works fine. Proof: https://www.youtube.com/watch?v=y3jyCaoru-A

   

2. following doc/make/emscripten.md for wasm32 build fails much earlier than 100k export issue (first it complains about STAGE not being set; after setting it, it looks for mimalloc in wrong loc; perhaps the CMakefile is out of date?). Proof: https://www.youtube.com/watch?v=WWs3F2ToU6c

   

If anyone could offer insight on this, it would be great. Between (1) #general > what is lean.js @ 💬 showing it is barely over 100k and #general > what is lean.js @ 💬 showing the new limit is 1M, I am hoping this can be made to work with a little linux/emscripten hacking.

Thanks!

[TongKe Xue]

I hope this does not come off as entitled -- the most helpful response would be if someone has

1. a 5-10 line bash script
2. to be run from .../lean4, after the x86_64 lean4 stage1 build
3. and will get me to the point where it complains about the 100k wasm export error

[TongKe Xue]

The "reason" I'm being so stubborn on this is that

1. after #general > what is lean.js @ 💬 's link to https://chromium.googlesource.com/v8/v8/+/285bfe195f7918f623ee6d0f138774ec003f2262%5E%21/#F0 ; I'm quite convinced Chrome itself supports 1M.
2. Which means the only issue is the "intermediate tooling" (which can probably be patched in 2-3 lines).
3. And from #general > what is lean.js , I'm not aware of any other "blockers"

So it seems like if we just push through this one obstacle, we can restore lean4 on wasm32 again.

[Kim Morrison]

You may have to do the archaeology yourself here, e.g. bisecting in the git history to find where things changed and/or identifying points in time when the non-wasm build changed (and the wasm build want updated because it was turned off!)

[TongKe Xue]

I'm not familiar with the Lean4 codebase yet, but sounds reasonable.

1. If we had to guess, https://github.com/leanprover/lean4/commits/master/src/CMakeLists.txt -- somewhere between 4.14.0 and 4.26.0-rc2 is probably where things got broken right ?

2. Would a reasonable first step be trying to get the wasm build to work on git tag 4.14.0 ? To binary search for this, I need a working state and a failure state. I know 4.26.0-rc2 fails; and 4.14.0 is supposedly the last working state ?

[TongKe Xue]

Even on 4.14.0(supposed to work, since 4.15 is when wasm was dropped), I can't get a working emscripten/wasm build.

1. Proof 4.14 x86_64 builds fine: https://www.youtube.com/watch?v=LSvOZClvuaI
   
2. Proof 4.14 emscripten/wasm build fails: https://www.youtube.com/watch?v=d3Auop5nXo4
   

At this point, it is pretty clear I am mis-interpreting doc/make/emscripten.md -- appears to be same instrs on 4.26.0-rc2 and 4.14.0 -- and I'm getting what appears to be same error in both cases.

It's not obvious to me how to do a emscripten/wasm build on 4.14.0. Are there CI wasm scripts somewhere I can copy/paste from for 4.14.0 ?

[TongKe Xue]

#lean4 > wasm build @ 💬 is interesting

wget -P toolchains https://github.com/leanprover/lean4/releases/download/v$LEAN_VERSION/lean-$LEAN_VERSION-linux_wasm32.tar.zst

^-- especially this line here. How / where in the CI is this file built ?

[TongKe Xue]

make
[  1%] Performing update step for 'libuv'
[  2%] Performing patch step for 'libuv'
HEAD is now at e9f29cb9 2024.02.07, Version 1.48.0 (Stable)
[  2%] Performing configure step for 'libuv'
-- summary of build options:
    Install prefix:  /nix/store/202rpslcjhwax183ahrf54xf46kvp1li-emscripten-4.0.10/share/emscripten/cache/sysroot
    Target system:   Emscripten
    Compiler:
      C compiler:    /nix/store/202rpslcjhwax183ahrf54xf46kvp1li-emscripten-4.0.10/share/emscripten/emcc (Clang)
      CFLAGS:         -s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto

-- Configuring done (1.2s)
-- Generating done (0.0s)
-- Build files have been written to: /home/y/tst/lean4/build/emscripten/libuv/src/libuv
[  3%] Performing build step for 'libuv'
[100%] Built target uv_a
[  4%] No install step for 'libuv'
[  5%] Completed 'libuv'
[  6%] Built target libuv
[  7%] Built target initialize
[  7%] Built target leaninitialize
[  9%] Built target leanshell
[ 26%] Built target compiler
[ 37%] Built target util
[ 48%] Built target kernel
[ 59%] Built target library
[ 62%] Built target constructions
[ 63%] Linking CXX static library lib/temp/libleancpp_1.a
[ 63%] Built target leancpp_1
[ 64%] Linking CXX static library lib/lean/libleancpp.a
[ 64%] Built target leancpp
bash: line 1: cd: /home/y/tst/lean4/src/../stdlib/: No such file or directory
bash: line 1: cd: /home/y/tst/lean4/src/../stdlib/: No such file or directory
make[4]: *** No rule to make target '../build/emscripten/lib/lean/Init/Simproc.olean', needed by 'objs'.  Stop.
make[3]: *** [/home/y/tst/lean4/build/emscripten/stdlib.make:37: Init] Error 2
make[2]: *** [CMakeFiles/make_stdlib.dir/build.make:70: CMakeFiles/make_stdlib] Error 2
make[1]: *** [CMakeFiles/Makefile2:1145: CMakeFiles/make_stdlib.dir/all] Error 2
make: *** [Makefile:146: all] Error 2

(building emscripten lean4 on 4.14.0)

I think this is closer; but I can't figure out wtf stdlib is supposed to be. C stdlib? C++ stdlib? Some lean stdlib?

[TongKe Xue]

4.14.0 wasm build is making progress. But I can't figure out wtf this Simproc.olean is:

error:

make
[  1%] Performing update step for 'libuv'
[  2%] Performing patch step for 'libuv'
HEAD is now at e9f29cb9 2024.02.07, Version 1.48.0 (Stable)
[  2%] Performing configure step for 'libuv'
-- summary of build options:
    Install prefix:  /nix/store/202rpslcjhwax183ahrf54xf46kvp1li-emscripten-4.0.10/share/emscripten/cache/sysroot
    Target system:   Emscripten
    Compiler:
      C compiler:    /nix/store/202rpslcjhwax183ahrf54xf46kvp1li-emscripten-4.0.10/share/emscripten/emcc (Clang)
      CFLAGS:         -s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto

-- Configuring done (1.4s)
-- Generating done (0.0s)
-- Build files have been written to: /home/y/tst/lean4/build/emscripten/libuv/src/libuv
[  3%] Performing build step for 'libuv'
[100%] Built target uv_a
[  4%] No install step for 'libuv'
[  5%] Completed 'libuv'
[  6%] Built target libuv
[  7%] Built target initialize
[  7%] Built target leaninitialize
[  9%] Built target leanshell
[ 26%] Built target compiler
[ 37%] Built target util
[ 48%] Built target kernel
[ 59%] Built target library
[ 62%] Built target constructions
[ 63%] Built target leancpp_1
[ 64%] Built target leancpp
make[4]: *** No rule to make target '../build/emscripten/lib/lean/Init/Simproc.olean', needed by 'objs'.  Stop.
make[3]: *** [/home/y/tst/lean4/build/emscripten/stdlib.make:37: Init] Error 2
make[2]: *** [CMakeFiles/make_stdlib.dir/build.make:70: CMakeFiles/make_stdlib] Error 2
make[1]: *** [CMakeFiles/Makefile2:1145: CMakeFiles/make_stdlib.dir/all] Error 2
make: *** [Makefile:146: all] Error 2

I don't understand where this Simproc is referenced:

[y@c240:~/tst/lean4/build/emscripten]$ rg Simproc ../../CMakeLists.txt ../../src/CMakeLists.txt

[y@c240:~/tst/lean4/build/emscripten]$ rg Simproc .
./shell/CTestTestfile.cmake
427:add_test([=[leantest_builtinSimprocTrace.lean]=] "bash" "-c" "PATH=/home/y/tst/lean4/build/emscripten/bin:\$PATH LEAN_CC=/nix/store/202rpslcjhwax183ahrf54xf46kvp1li-emscripten-4.0.10/share/emscripten/emcc CXX='/nix/store/202rpslcjhwax183ahrf54xf46kvp1li-emscripten-4.0.10/share/emscripten/em++  ' LEANC_OPTS=' ' ./test_single.sh builtinSimprocTrace.lean")
428:set_tests_properties([=[leantest_builtinSimprocTrace.lean]=] PROPERTIES  WORKING_DIRECTORY "/home/y/tst/lean4/src/../tests/lean" _BACKTRACE_TRIPLES "/home/y/tst/lean4/src/shell/CMakeLists.txt;67;add_test;/home/y/tst/lean4/src/shell/CMakeLists.txt;0;")

[Kevin Buzzard]

I'm not sure you're going to get too much support here trying to build 4.14 unfortunately

[TongKe Xue]

Sorry for not being clear:

1. My goal is not to build 4.14.
2. My goal is to get 4.26.0-rc2 to get to a point I can replicate the 100k wasm-export limit error.
3. I can't get 4.26.0-rc2 to replicate that error, I suspect something in the CMakeList.txt or build process has bit-rotted after wasm was turned off in 4.15.0
4. So I'm trying to get a version where lean4 compiles to wasm, then bisect through the commits to get to a point where 4.26.0-rc2 tries to do the wasm32 build (and fails at the 100k wasm-export limit).

If this sounds convoluted -- it's because I'm not familiar with the codebase and have no other attack.

Again, my goal is NOT to build 4.14.0 to use in wasm. My goal is to get 4.26.0-rc2 to get to the point where I can replicate the 100k wasm-export issue. But I can't do that right now, as it appears the lean4/4.26.0-rc2/doc/make/emscripten.md may have bit rotted.

[TongKe Xue]

I'm trying to build 4.14 because

1. I read somewhere in 4.15.0, wasm support was dropped
2. So I'm trying to get the latest still-working-wasm-build to run, just to see what the Makefile / CMake is supposed to look for a successful/working wasm build.

[TongKe Xue]

Phrased another way:

1. I believe 4.26.0-rc2 fails to build on wasm32 for two reasons: (a) 100k export limit, (b) wasm32 build scripts have bit rotted.

2. I am trying to build 4.14, not because I want to use the 4.14-wasm in Chrome; but because I am trying to find what a successful "(b)" -- working wasm32 build script -- is supposed to look like, so I can "un-bit-rot" the 4.26.0-rc2 to the point I can replicate the 100k wasm-export limit.

[Kevin Buzzard]

Thanks for your clear answers. I shouldn't really be contributing here at all, I understand nothing of all this, I just wanted to warn you that often when people come along saying "I am trying to get this old version working" people's instincts are usually "just get a new version working". But this case does seem to be different to the usual one.