Zulip Chat Archive

Stream: general

Topic: lean-web-editor not compiling?


Scott Morrison (Apr 02 2018 at 23:59):

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

Scott Morrison (Apr 03 2018 at 00:00):

When I try

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

Scott Morrison (Apr 03 2018 at 00:00):

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

Gabriel Ebner (Apr 03 2018 at 08:34):

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 (Apr 03 2018 at 08:35):

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

Gabriel Ebner (Apr 03 2018 at 08:35):

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

Sebastian Ullrich (Apr 03 2018 at 09:01):

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


Last updated: Dec 20 2023 at 11:08 UTC