lean-web-editor not compiling?

Stream: general

[Scott Morrison]

@Gabriel Ebner, I'm trying to build the lean-web-editor from scratch, and running into a problem.

[Scott Morrison]

When I try

mkdir -p build/release
pushd build/release
emconfigure cmake ../../src/ -DCMAKE_BUILD_TYPE=Emscripten
make

[Scott Morrison]

I get the following error: https://gist.github.com/semorrison/5145439a8e501380dd102edf50ea67c8

[Gabriel Ebner]

I don't think anyone has ever tried building the emscripten version on macOS. We even hardcode Linux on x86_64 as the host platform: https://github.com/leanprover/lean/blob/96c932ab210ac4e71ad3439d128fb4f75b314e1e/src/CMakeLists.txt#L290

[Gabriel Ebner]

You can try to look at the config.log file, which should show the exact error message.

[Gabriel Ebner]

But I'd suggest to do the emscripten build in docker or a VM instead.

[Sebastian Ullrich]

And feel free to set up a Travis script :smile: