Zulip Chat Archive

Stream: general

Topic: lean-web-editor not compiling?


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Scott Morrison (Apr 03 2018 at 00:00):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Apr 03 2018 at 08:35):

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

view this post on Zulip Sebastian Ullrich (Apr 03 2018 at 09:01):

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


Last updated: May 16 2021 at 20:13 UTC