Some changes to revive WebAssembly support

[rujialiu]

• Put an X in this bracket to confirm you have read the
  External Contribution Guidelines.

• Please put the link to your RFC or bug issue here.
  PRs missing this link will be marked as missing RFC.

• If that issue does not already have approval from a developer,
  please be sure to open this PR in "Draft" mode.

• Please make sure the PR has excellent documentation and tests.
  If we label it missing documentation or missing tests then it needs fixing!

• You can manage the awaiting-review, awaiting-author, and WIP labels
  yourself, by writing a comment containing one of these labels on its own line.

[github-actions]

Thanks for your contribution! Please make sure to follow our Commit Convention.

[rujialiu]

Here is the commands used to build:

cd /src/lean4/build/release
rm -rf *
emcmake cmake ../.. -DUSE_GMP=OFF -DSTAGE0_CMAKE_AR=/emsdk_portable/upstream/emscripten/emar -DSTAGE0_CMAKE_TOOLCHAIN_FILE=/emsdk_portable/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake -DDSTAGE0_CMAKE_CROSSCOMPILING_EMULATOR="/emsdk_portable/node/12.9.1_64bit/bin/node"
VERBOSE=1 emmake make -j4 stage0
"/src/lean4/build/release/stage0/leanc.sh" /src/lean4/build/release/stage0/shell/CMakeFiles/shell.dir/lean.cpp.o -Wl,--whole-archive -lInit -lLean -lleancpp -lleanrt -rdynamic -o /src/lean4/build/release/stage0/bin/lean -s ERROR_ON_UNDEFINED_SYMBOLS=0 -s ASSERTIONS=1 -s WASM=1 -fexceptions -lnodefs.js -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1 -s LLD_REPORT_UNDEFINED=1
cp -a /src/lean4/build/release/stage0 /home
cd /home/stage0/bin
LEAN_PATH=/home/stage0/bin node --stack-size=8192 lean --run Main.lean

Note that I didn't bother changing the final command to build the wasm, so I added a followup command after make. The next command is to copy everything into a directory insode /home because the current code only mounted /home and /tmp. The last command is try to run a Hello World program (or whatever else).

The local paths used in the command was reported by executing emcmake alone first.

[eric-wieser]

I'm puzzled by this; it look like the original code should work just fine, given it runs:

https://github.com/emscripten-core/emscripten/blob/0be5b609412d5b07f8157528df8e5088dae84858/system/lib/libc/dynlink.c#L664-L668

which shouldn't care whether you first run dlopen:

https://github.com/emscripten-core/emscripten/blob/0be5b609412d5b07f8157528df8e5088dae84858/system/lib/libc/dynlink.c#L543C1-L548C4

[eric-wieser]

It looks to me like this is no longer necessary after emscripten-core/emscripten@c4f7a55; what version of empscripten are we targeting?

[rujialiu]

Oops. It looks like I'm using a rather old docker image (https://hub.docker.com/r/trzeci/emscripten). I think that was recommended by the official doc but apparently it's already outdated. So I think you're right: it's not neccesary for recent emscripten versions. PS: I'm setting up this PR for easier discussion and further experiment in zulip topic "wasm build" with other people. You can also help us there. Thank you! @eric-wieser

[rujialiu]

superseded by #2599