emscripten build

Stream: general

[Sebastian Ullrich]

I see the emscripten situation is as stellar as ever :| .
Using the official Arch Linux build:

$ pacaur -Qo $(which emconfigure)
/usr/lib/emscripten/emconfigure is owned by emscripten 1.37.36-1
 $ emconfigure cmake ../../src -DCMAKE_BUILD_TYPE=Emscripten
-- Lean library will be installed at /usr/local/lib/lean
-- Disabled multi-thread support, it will not be safe to run multiple threads in parallel
-- Using standard malloc.
-- Found PythonInterp: /usr/bin/python (found version "3.6.4")
-- git commit sha1: 17fe3decaf8ae236f0d0ff51ac8fd7f6940acdee
-- Configuring done
-- Generating done
-- Build files have been written to: /home/sebastian/projects/lean/build/emscripten
$ make
...
checking how to switch to text section... configure: error: Cannot determine text section directive
ERROR:root:Configure step failed with non-zero return code 1! Command line: ['./configure', 'CC_FOR_BUILD=gcc', 'CFLAGS=-m32 -DPIC -Oz -O3', '--host=x86_64-pc-linux-gnu', '--build=i686-pc-linux-gnu', '--disable-assembly', '--prefix=/home/sebastian/projects/lean/build/emscripten/gmp-root'] at /home/sebastian/projects/lean/build/emscripten/gmp-prefix/src/gmp
make[2]: *** [CMakeFiles/gmp.dir/build.make:109: gmp-prefix/src/gmp-stamp/gmp-configure] Error 1
make[1]: *** [CMakeFiles/Makefile2:1180: CMakeFiles/gmp.dir/all] Error 2
make: *** [Makefile:163: all] Error 2

[Sebastian Ullrich]

/cc @Gabriel Ebner @Scott Morrison @loki der quaeler

[Kevin Buzzard]

https://gitter.im/leanprover_public/lean_js

[Kevin Buzzard]

(for reference)

[Johan Commelin]

Once we have multiplayer lean on cocalc we can forget about these headaches :video_game:

[Kevin Buzzard]

no because I want people who are idly reading my blog with no cocalc account to be able to see modern lean and mathlib doing stuff at the click of a button.

[Kevin Buzzard]

so we have one 3.4.1 headache

[Kevin Buzzard]

but then that's it

[Kevin Buzzard]

[assuming Mario can get mathlib working with 3.4.1]

[Kevin Buzzard]

[or else the number of headaches goes up again]

[Johan Commelin]

Ok, fair enough

[Gabriel Ebner]

try this:

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 863f6a66d..6163d9b32 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -287,7 +287,7 @@ if (EMSCRIPTEN)
             URL https://gmplib.org/download/gmp/gmp-6.1.1.tar.bz2
             URL_HASH SHA256=a8109865f2893f1373b0a8ed5ff7429de8db696fc451b1036bd7bdf95bbeffd6
             BUILD_IN_SOURCE 1
-            CONFIGURE_COMMAND emconfigure ./configure "CC_FOR_BUILD=gcc" "CFLAGS=-m32 -DPIC ${CFLAGS_EMSCRIPTEN}" --host=x86_64-pc-linux-gnu --build=i686-pc-linux-gnu --disable-assembly --prefix=${gmp_install_prefix}
+           CONFIGURE_COMMAND emconfigure ./configure "CC_FOR_BUILD=gcc" "CCAS=gcc -c" "CFLAGS=-m32 -DPIC ${CFLAGS_EMSCRIPTEN}" --host=x86_64-pc-linux-gnu --build=i686-pc-linux-gnu --disable-assembly --prefix=${gmp_install_prefix}
             BUILD_COMMAND emmake make -j4
             INSTALL_COMMAND make install
     )

[Sebastian Ullrich]

@Gabriel Ebner Seems to work, thanks!

[Bryan Gin-ge Chen]

@Sebastian Ullrich @Gabriel Ebner I've been digging into the emscripten build for lean and am trying to figure out how to get a reasonable test setup working in the community fork (see this PR). I'd appreciate any advice or suggestions if you've got time.

Here's where I'm at: I've managed to build the js and wasm files that are used by lean-web-editor, but I am having trouble with the other build outputs. ctest seems to rely on a shell script lean which runs lean.js and lean.wasm using node. This fails for me with the following error (and I get similar errors for leanchecker):

{ Error
    at new ErrnoError (.../lean/build/emscripten/shell/lean.js:1:72345)
    at Object.getMode (.../lean/build/emscripten/shell/lean.js:1:40486)
    at Object.mount (.../lean/build/emscripten/shell/lean.js:1:40042)
    at Object.mount (.../lean/build/emscripten/shell/lean.js:1:56062)
    at Array.ASM_CONSTS (.../lean/build/emscripten/shell/lean.js:1:15742)
    at _emscripten_asm_const_i (.../lean/build/emscripten/shell/lean.js:1:15892)
    at wasm-function[11542]:20
    at Object.Module._main (.../lean/build/emscripten/shell/lean.js:1:123255)
    at Object.callMain (.../lean/build/emscripten/shell/lean.js:1:128352)
    at doRun (.../lean/build/emscripten/shell/lean.js:1:129028)
  node: undefined,
  setErrno: [Function],
  errno: 2,
  message: 'FS error' }

Any ideas on how to get it running again?

I tried adding:

    set_target_properties(lean PROPERTIES LINK_FLAGS "-s WASM=0 ${LEAN_JS_OPTS}")

in src/shell/CMakeLists.txt since LEAN_JS_OPTS contains "-s 'EXTRA_EXPORTED_RUNTIME_METHODS=[\"FS\"]'" but it didn't seem to do anything. (-s WASM=1 didn't work either) (Actually, that option doesn't matter.)

[Bryan Gin-ge Chen]

OK, I've gotten past this error now. There were some hardcoded paths in src/shell/lean.cpp that I had to change.