From 7dc1618ca532bc57ee452c9a47eafb01afa75bc3 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Wed, 4 Oct 2023 09:04:20 +0200 Subject: [PATCH] feat: Web Assembly Build (#2599) Co-authored-by: Rujia Liu --- .github/workflows/ci.yml | 24 +++++++++++++++++++-- CMakeLists.txt | 25 ++++++---------------- src/CMakeLists.txt | 37 +++++++++++++++++++-------------- src/bin/lean.in | 4 ++++ src/include/lean/lean.h | 4 ++-- src/lean.mk.in | 2 +- src/library/module.cpp | 6 +++++- src/runtime/io.cpp | 4 +++- src/runtime/stack_overflow.cpp | 6 +----- src/runtime/stackinfo.cpp | 12 +++++++++++ src/shell/CMakeLists.txt | 8 +++++-- src/stdlib.make.in | 10 ++++----- stage0/src/CMakeLists.txt | 37 +++++++++++++++++++-------------- stage0/src/library/module.cpp | 6 +++++- stage0/src/shell/CMakeLists.txt | 10 +++++++-- stage0/src/stdlib.make.in | 10 ++++----- tests/common.sh | 4 ++-- 17 files changed, 129 insertions(+), 80 deletions(-) create mode 100755 src/bin/lean.in diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index cdf7ba18dd..f686629527 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -168,6 +168,15 @@ jobs: shell: nix-shell --arg pkgsDist "import (fetchTarball \"channel:nixos-19.03\") {{ localSystem.config = \"aarch64-unknown-linux-gnu\"; }}" --run "bash -euxo pipefail {0}" llvm-url: https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst prepare-llvm: EXTRA_FLAGS=--target=aarch64-unknown-linux-gnu ../script/prepare-llvm-linux.sh lean-llvm-aarch64-* lean-llvm-x86_64-* + - name: Web Assembly + os: ubuntu-latest + # Build a native 32bit binary in stage0 and use it to compile the oleans and the wasm build + CMAKE_OPTIONS: -DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_EXECUTABLE_SUFFIX="" -DUSE_GMP=OFF -DMMAP=OFF -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DCMAKE_AR=../emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=../emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake + wasm: true + cross: true + shell: bash -euxo pipefail {0} + # Just a few selected test because wasm is slow + CTEST_OPTIONS: -R "leantest_1007\.lean|leantest_Format\.lean|leanruntest\_1037.lean|leanruntest_ac_rfl\.lean" # complete all jobs fail-fast: false name: ${{ matrix.name }} @@ -192,7 +201,7 @@ jobs: uses: cachix/install-nix-action@v18 with: install_url: https://releases.nixos.org/nix/nix-2.12.0/install - if: matrix.os == 'ubuntu-latest' + if: matrix.os == 'ubuntu-latest' && !matrix.wasm - name: Install MSYS2 uses: msys2/setup-msys2@v2 with: @@ -204,6 +213,17 @@ jobs: run: | brew install ccache tree zstd coreutils gmp if: matrix.os == 'macos-latest' + - name: Setup emsdk + uses: mymindstorm/setup-emsdk@v11 + with: + version: 3.1.44 + actions-cache-folder: emsdk + if: matrix.wasm + - name: Install 32bit c libs + run: | + sudo apt-get update + sudo apt-get install -y gcc-multilib g++-multilib ccache + if: matrix.wasm - name: Cache uses: actions/cache@v3 with: @@ -280,7 +300,7 @@ jobs: ulimit -c unlimited # coredumps # exclude nonreproducible test ctest -j4 --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null - if: ${{ !matrix.cross }} + if: matrix.wasm || !matrix.cross - name: Check Test Binary run: ${{ matrix.binary-check }} tests/compiler/534.lean.out if: ${{ !matrix.cross }} diff --git a/CMakeLists.txt b/CMakeLists.txt index 4e6c7bcc76..271ef9c4cd 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -26,23 +26,10 @@ endforeach() include(ExternalProject) project(LEAN CXX C) -if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten") - # For Emscripten, we build GMP before any of the stages and reuse it in all of them. - set(GMP_INSTALL_PREFIX ${CMAKE_BINARY_DIR}/gmp-root) - set(EMSCRIPTEN_FLAGS "-s ALLOW_MEMORY_GROWTH=1 -s MAIN_MODULE=1 -O3") - ExternalProject_Add( - gmp - URL https://gmplib.org/download/gmp/gmp-6.2.1.tar.bz2 - URL_HASH SHA256=eae9326beb4158c386e39a356818031bd28f3124cf915f8c5b1dc4c7a36b4d7c - BUILD_IN_SOURCE 1 - CONFIGURE_COMMAND emconfigure ./configure "CFLAGS=${EMSCRIPTEN_FLAGS}" --host=wasm32-unknown-emscripten --disable-assembly --prefix=${GMP_INSTALL_PREFIX} - BUILD_COMMAND emmake make -j4 - INSTALL_COMMAND emmake make install - ) - set(EXTRA_DEPENDS "gmp") - list(APPEND CL_ARGS "-DGMP_INSTALL_PREFIX=${GMP_INSTALL_PREFIX}") - list(APPEND PLATFORM_ARGS "-DGMP_INSTALL_PREFIX=${GMP_INSTALL_PREFIX}") +if(NOT (DEFINED STAGE0_CMAKE_EXECUTABLE_SUFFIX)) + set(STAGE0_CMAKE_EXECUTABLE_SUFFIX "${CMAKE_EXECUTABLE_SUFFIX}") endif() + ExternalProject_add(stage0 SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0" SOURCE_SUBDIR src @@ -57,7 +44,7 @@ ExternalProject_add(stage1 SOURCE_DIR "${LEAN_SOURCE_DIR}" SOURCE_SUBDIR src BINARY_DIR stage1 - CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 ${CL_ARGS} + CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS} BUILD_ALWAYS ON INSTALL_COMMAND "" DEPENDS stage0 @@ -66,7 +53,7 @@ ExternalProject_add(stage2 SOURCE_DIR "${LEAN_SOURCE_DIR}" SOURCE_SUBDIR src BINARY_DIR stage2 - CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 ${CL_ARGS} + CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS} BUILD_ALWAYS ON INSTALL_COMMAND "" DEPENDS stage1 @@ -76,7 +63,7 @@ ExternalProject_add(stage3 SOURCE_DIR "${LEAN_SOURCE_DIR}" SOURCE_SUBDIR src BINARY_DIR stage3 - CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 ${CL_ARGS} + CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS} BUILD_ALWAYS ON INSTALL_COMMAND "" DEPENDS stage2 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index edde691518..b40444ee22 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -57,6 +57,7 @@ option(CUSTOM_ALLOCATORS "CUSTOM_ALLOCATORS" ON) option(SAVE_SNAPSHOT "SAVE_SNAPSHOT" ON) option(SAVE_INFO "SAVE_INFO" ON) option(SMALL_ALLOCATOR "SMALL_ALLOCATOR" ON) +option(MMAP "MMAP" ON) option(LAZY_RC "LAZY_RC" OFF) option(RUNTIME_STATS "RUNTIME_STATS" OFF) option(BSYMBOLIC "Link with -Bsymbolic to reduce call overhead in shared libraries (Linux)" ON) @@ -84,6 +85,10 @@ else() set(NumBits 32) endif() +if ("${MMAP}" MATCHES "ON") + string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_MMAP") +endif() + if ("${RUNTIME_STATS}" MATCHES "ON") string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_RUNTIME_STATS") endif() @@ -93,29 +98,19 @@ if (NOT("${CHECK_OLEAN_VERSION}" MATCHES "ON")) endif() if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten") - set(MULTI_THREAD OFF) # TODO(WN): code size/performance tradeoffs # - we're using -O3; it's /okay/ - # - -flto crashes at runtime # - -Oz produces quite slow code # - system libraries such as OpenGL are included in the JS but shouldn't be # - we need EMSCRIPTEN_KEEPALIVE annotations on exports to run meta-dce (-s MAIN_MODULE=2) - # - -fexceptions is a slow JS blob, remove when more runtimes support the WASM exceptions spec # From https://emscripten.org/docs/compiling/WebAssembly.html#backends: # > The simple and safe thing is to pass all -s flags at both compile and link time. - set(EMSCRIPTEN_SETTINGS "-s ALLOW_MEMORY_GROWTH=1 -s DISABLE_EXCEPTION_CATCHING=0 -s MAIN_MODULE=1 -fexceptions") + set(EMSCRIPTEN_SETTINGS "-s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto") + string(APPEND LEANC_EXTRA_FLAGS " -pthread") string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_EMSCRIPTEN ${EMSCRIPTEN_SETTINGS}") string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${EMSCRIPTEN_SETTINGS}") endif() -if (CMAKE_CROSSCOMPILING_EMULATOR) - # emscripten likes to quote "node" - string(REPLACE "\"" "" CMAKE_CROSSCOMPILING_EMULATOR ${CMAKE_CROSSCOMPILING_EMULATOR}) - # HACK(WN): lazy compilation makes Node.js startup time a bad but tolerable ~4s - string(APPEND CMAKE_CROSSCOMPILING_EMULATOR " --wasm-lazy-compilation") -else() - set(CMAKE_CROSSCOMPILING_EMULATOR) -endif() # Added for CTest include(CTest) @@ -339,7 +334,7 @@ endif() # get rid of unused parts of C++ stdlib if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-dead_strip") -else() +elseif(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten") string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--gc-sections") endif() @@ -355,18 +350,28 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec") string(APPEND LEANC_EXTRA_FLAGS " -fPIC") string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") - string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean") + string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean") elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec") string(APPEND LEANSHARED_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib") - string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean") + string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean") +elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten") + string(APPEND CMAKE_CXX_FLAGS " -fPIC") + string(APPEND LEANC_EXTRA_FLAGS " -fPIC") + # We do not use dynamic linking via leanshared for Emscripten to keep things + # simple. (And we are not interested in `Lake` anyway.) To use dynamic + # linking, we would probably have to set MAIN_MODULE=2 on `leanshared`, + # SIDE_MODULE=2 on `lean`, and set CMAKE_SHARED_LIBRARY_SUFFIX to ".js". + string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,--whole-archive -lInit -lLean -lleancpp -lleanrt ${EMSCRIPTEN_SETTINGS} -lnodefs.js -s EXIT_RUNTIME=1 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1") +elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows") + string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared") endif() if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") string(APPEND LEAN_EXTRA_LINKER_FLAGS " -ldl") endif() -if(NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows")) +if(NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows") AND NOT(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")) # export symbols for the interpreter (done via `LEAN_EXPORT` for Windows) string(APPEND LEAN_DYN_EXE_LINKER_FLAGS " -rdynamic") string(APPEND CMAKE_EXE_LINKER_FLAGS " -rdynamic") diff --git a/src/bin/lean.in b/src/bin/lean.in new file mode 100755 index 0000000000..044b4cef36 --- /dev/null +++ b/src/bin/lean.in @@ -0,0 +1,4 @@ +#!/usr/bin/env bash +# ONLY FOR WEB ASSEMBLY BUILD +node --stack-size=8192 ${CMAKE_BINARY_DIR}/bin/lean.js $@ + diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index 45a4bd0abd..d7fc1ee579 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -1312,8 +1312,8 @@ LEAN_SHARED lean_obj_res lean_nat_log2(b_lean_obj_arg a); /* Integers */ -#define LEAN_MAX_SMALL_INT (sizeof(void*) == 8 ? INT_MAX : (1 << 30)) -#define LEAN_MIN_SMALL_INT (sizeof(void*) == 8 ? INT_MIN : -(1 << 30)) +#define LEAN_MAX_SMALL_INT (sizeof(void*) == 8 ? INT_MAX : (INT_MAX >> 1)) +#define LEAN_MIN_SMALL_INT (sizeof(void*) == 8 ? INT_MIN : (INT_MIN >> 1)) LEAN_SHARED lean_object * lean_int_big_neg(lean_object * a); LEAN_SHARED lean_object * lean_int_big_add(lean_object * a1, lean_object * a2); LEAN_SHARED lean_object * lean_int_big_sub(lean_object * a1, lean_object * a2); diff --git a/src/lean.mk.in b/src/lean.mk.in index eb3fb1ad57..90db2de6e9 100644 --- a/src/lean.mk.in +++ b/src/lean.mk.in @@ -12,7 +12,7 @@ endif LEAN = lean LEANC = leanc -LEAN_AR = ar +LEAN_AR = @CMAKE_AR@ OUT = build OLEAN_OUT = $(OUT) TEMP_OUT = $(OUT)/temp diff --git a/src/library/module.cpp b/src/library/module.cpp index bb41bbe318..7d93ca857c 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -155,7 +155,9 @@ extern "C" LEAN_EXPORT object * lean_read_module_data(object * fname, object *) if (fd == -1) { return io_result_mk_error((sstream() << "failed to open '" << olean_fn << "': " << strerror(errno)).str()); } +#ifdef LEAN_MMAP buffer = static_cast(mmap(base_addr, size, PROT_READ, MAP_PRIVATE, fd, 0)); +#endif close(fd); free_data = [=]() { if (buffer != MAP_FAILED) { @@ -163,11 +165,13 @@ extern "C" LEAN_EXPORT object * lean_read_module_data(object * fname, object *) } }; #endif - if (buffer == base_addr) { + if (buffer && buffer == base_addr) { buffer += header_size; is_mmap = true; } else { +#ifdef LEAN_MMAP free_data(); +#endif buffer = static_cast(malloc(size - header_size)); free_data = [=]() { free(buffer); diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index c923a12a38..86c206024e 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -20,8 +20,10 @@ Authors: Leonardo de Moura, Sebastian Ullrich // Linux include files #include // NOLINT #include +#ifndef LEAN_EMSCRIPTEN #include #endif +#endif #ifndef LEAN_WINDOWS #include #endif @@ -433,7 +435,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_get_random_bytes (size_t nbytes, obj_arg #else #if defined(LEAN_EMSCRIPTEN) // `Crypto.getRandomValues` documents `dest` should be at most 65536 bytes. - size_t read_sz = std::min(remain, 65536); + size_t read_sz = std::min(remain, static_cast(65536)); #else size_t read_sz = remain; #endif diff --git a/src/runtime/stack_overflow.cpp b/src/runtime/stack_overflow.cpp index 0e5656d61b..f1a81f0a00 100644 --- a/src/runtime/stack_overflow.cpp +++ b/src/runtime/stack_overflow.cpp @@ -42,10 +42,6 @@ stack_guard::stack_guard() { SetThreadStackGuarantee(&sz); } -stack_guard::~stack_guard() {} -#elif defined(LEAN_EMSCRIPTEN) -stack_guard::stack_guard() {} - stack_guard::~stack_guard() {} #else // Install a segfault signal handler and abort with custom message if address is within stack guard. @@ -105,7 +101,7 @@ void initialize_stack_overflow() { g_stack_guard = new stack_guard(); #ifdef LEAN_WINDOWS AddVectoredExceptionHandler(0, stack_overflow_handler); -#elif !defined(LEAN_EMSCRIPTEN) +#else struct sigaction action; memset(&action, 0, sizeof(struct sigaction)); action.sa_flags = SA_SIGINFO | SA_ONSTACK; diff --git a/src/runtime/stackinfo.cpp b/src/runtime/stackinfo.cpp index 0e7c6ea52a..48f4c7a394 100644 --- a/src/runtime/stackinfo.cpp +++ b/src/runtime/stackinfo.cpp @@ -19,6 +19,10 @@ Author: Leonardo de Moura #include // NOLINT #endif +#if defined(LEAN_EMSCRIPTEN) +#include +#endif + namespace lean { void throw_get_stack_size_failed() { throw exception("failed to retrieve thread stack size"); @@ -45,6 +49,14 @@ size_t get_stack_size(int main) { return lthread::get_thread_stack_size(); } } +#elif defined(LEAN_EMSCRIPTEN) +size_t get_stack_size(int main) { + if (main) { + return emscripten_stack_get_end() - emscripten_stack_get_base(); + } else { + return lthread::get_thread_stack_size(); + } +} #else size_t get_stack_size(int main) { if (main) { diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 389bfca006..7329b1a772 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -46,8 +46,12 @@ add_test(lean_ghash2 "${CMAKE_BINARY_DIR}/bin/lean" --githash) add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "-z") add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "boofoo.lean") -# LEANC_OPTS is necessary for macOS c++ to find its headers -set(TEST_VARS "PATH=${LEAN_BIN}:$PATH ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}'") +if(${EMSCRIPTEN}) + configure_file("${LEAN_SOURCE_DIR}/bin/lean.in" "${CMAKE_BINARY_DIR}/bin/lean") +endif() + +# LEANC_OPTS in CXX is necessary for macOS c++ to find its headers +set(TEST_VARS "PATH=${LEAN_BIN}:$PATH ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'") # LEAN TESTS file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") diff --git a/src/stdlib.make.in b/src/stdlib.make.in index e8c876b8ad..5d192f9ec6 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -12,7 +12,7 @@ export LEAN_ABORT_ON_PANIC=1 # LEAN_OPTS: don't use native code (except for primitives) since it is from the previous stage # MORE_DEPS: rebuild the stdlib whenever the compiler has changed LEANMAKE_OPTS=\ - LEAN="${CMAKE_CROSSCOMPILING_EMULATOR} ${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\ + LEAN="${PREV_STAGE}/bin/lean${PREV_STAGE_CMAKE_EXECUTABLE_SUFFIX}"\ LEANC="${CMAKE_BINARY_DIR}/leanc.sh"\ OUT="${LIB}"\ LIB_OUT="${LIB}/lean"\ @@ -21,7 +21,7 @@ LEANMAKE_OPTS=\ LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -DwarningAsError=true"\ LEANC_OPTS+="${LEANC_OPTS}"\ LEAN_AR="${CMAKE_AR}"\ - MORE_DEPS+="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\ + MORE_DEPS+="${PREV_STAGE}/bin/lean${PREV_STAGE_CMAKE_EXECUTABLE_SUFFIX}"\ ${EXTRA_LEANMAKE_OPTS}\ CMAKE_LIKE_OUTPUT=1 @@ -52,15 +52,15 @@ leanshared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRAR Lake: # lake is in its own subdirectory, so must adjust relative paths... - +"${LEAN_BIN}/leanmake" -C lake bin lib PKG=Lake BIN_NAME=lake${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='-lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="../${LIB}" LIB_OUT="../${LIB}/lean" OLEAN_OUT="../${LIB}/lean" + +"${LEAN_BIN}/leanmake" -C lake bin lib PKG=Lake BIN_NAME=lake${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="../${LIB}" LIB_OUT="../${LIB}/lean" OLEAN_OUT="../${LIB}/lean" ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} $(LEAN_SHELL) @echo "[ ] Building $@" # on Windows, must remove file before writing a new one (since the old one may be in use) @rm -f $@ - "${CMAKE_BINARY_DIR}/leanc.sh" $(LEAN_SHELL) -lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@ + "${CMAKE_BINARY_DIR}/leanc.sh" $(LEAN_SHELL) ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@ lean: ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX} Leanc: - +"${LEAN_BIN}/leanmake" bin PKG=Leanc BIN_NAME=leanc${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='-lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="${CMAKE_BINARY_DIR}" OLEAN_OUT="${CMAKE_BINARY_DIR}" + +"${LEAN_BIN}/leanmake" bin PKG=Leanc BIN_NAME=leanc${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="${CMAKE_BINARY_DIR}" OLEAN_OUT="${CMAKE_BINARY_DIR}" diff --git a/stage0/src/CMakeLists.txt b/stage0/src/CMakeLists.txt index 2c2425da5f..6e735d8450 100644 --- a/stage0/src/CMakeLists.txt +++ b/stage0/src/CMakeLists.txt @@ -57,6 +57,7 @@ option(CUSTOM_ALLOCATORS "CUSTOM_ALLOCATORS" ON) option(SAVE_SNAPSHOT "SAVE_SNAPSHOT" ON) option(SAVE_INFO "SAVE_INFO" ON) option(SMALL_ALLOCATOR "SMALL_ALLOCATOR" ON) +option(MMAP "MMAP" ON) option(LAZY_RC "LAZY_RC" OFF) option(RUNTIME_STATS "RUNTIME_STATS" OFF) option(BSYMBOLIC "Link with -Bsymbolic to reduce call overhead in shared libraries (Linux)" ON) @@ -84,6 +85,10 @@ else() set(NumBits 32) endif() +if ("${MMAP}" MATCHES "ON") + string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_MMAP") +endif() + if ("${RUNTIME_STATS}" MATCHES "ON") string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_RUNTIME_STATS") endif() @@ -93,29 +98,19 @@ if (NOT("${CHECK_OLEAN_VERSION}" MATCHES "ON")) endif() if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten") - set(MULTI_THREAD OFF) # TODO(WN): code size/performance tradeoffs # - we're using -O3; it's /okay/ - # - -flto crashes at runtime # - -Oz produces quite slow code # - system libraries such as OpenGL are included in the JS but shouldn't be # - we need EMSCRIPTEN_KEEPALIVE annotations on exports to run meta-dce (-s MAIN_MODULE=2) - # - -fexceptions is a slow JS blob, remove when more runtimes support the WASM exceptions spec # From https://emscripten.org/docs/compiling/WebAssembly.html#backends: # > The simple and safe thing is to pass all -s flags at both compile and link time. - set(EMSCRIPTEN_SETTINGS "-s ALLOW_MEMORY_GROWTH=1 -s DISABLE_EXCEPTION_CATCHING=0 -s MAIN_MODULE=1 -fexceptions") + set(EMSCRIPTEN_SETTINGS "-s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto") + string(APPEND LEANC_EXTRA_FLAGS " -pthread") string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_EMSCRIPTEN ${EMSCRIPTEN_SETTINGS}") string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${EMSCRIPTEN_SETTINGS}") endif() -if (CMAKE_CROSSCOMPILING_EMULATOR) - # emscripten likes to quote "node" - string(REPLACE "\"" "" CMAKE_CROSSCOMPILING_EMULATOR ${CMAKE_CROSSCOMPILING_EMULATOR}) - # HACK(WN): lazy compilation makes Node.js startup time a bad but tolerable ~4s - string(APPEND CMAKE_CROSSCOMPILING_EMULATOR " --wasm-lazy-compilation") -else() - set(CMAKE_CROSSCOMPILING_EMULATOR) -endif() # Added for CTest include(CTest) @@ -339,7 +334,7 @@ endif() # get rid of unused parts of C++ stdlib if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-dead_strip") -else() +elseif(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten") string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--gc-sections") endif() @@ -355,18 +350,28 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec") string(APPEND LEANC_EXTRA_FLAGS " -fPIC") string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") - string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean") + string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean") elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec") string(APPEND LEANSHARED_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib") - string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean") + string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean") +elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten") + string(APPEND CMAKE_CXX_FLAGS " -fPIC") + string(APPEND LEANC_EXTRA_FLAGS " -fPIC") + # We do not use dynamic linking via leanshared for Emscripten to keep things + # simple. (And we are not interested in `Lake` anyway.) To use dynamic + # linking, we would probably have to set MAIN_MODULE=2 on `leanshared`, + # SIDE_MODULE=2 on `lean`, and set CMAKE_SHARED_LIBRARY_SUFFIX to ".js". + string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,--whole-archive -lInit -lLean -lleancpp -lleanrt ${EMSCRIPTEN_SETTINGS} -lnodefs.js -s EXIT_RUNTIME=1 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1") +elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows") + string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared") endif() if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") string(APPEND LEAN_EXTRA_LINKER_FLAGS " -ldl") endif() -if(NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows")) +if(NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows") AND NOT(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")) # export symbols for the interpreter (done via `LEAN_EXPORT` for Windows) string(APPEND LEAN_DYN_EXE_LINKER_FLAGS " -rdynamic") string(APPEND CMAKE_EXE_LINKER_FLAGS " -rdynamic") diff --git a/stage0/src/library/module.cpp b/stage0/src/library/module.cpp index bb41bbe318..7d93ca857c 100644 --- a/stage0/src/library/module.cpp +++ b/stage0/src/library/module.cpp @@ -155,7 +155,9 @@ extern "C" LEAN_EXPORT object * lean_read_module_data(object * fname, object *) if (fd == -1) { return io_result_mk_error((sstream() << "failed to open '" << olean_fn << "': " << strerror(errno)).str()); } +#ifdef LEAN_MMAP buffer = static_cast(mmap(base_addr, size, PROT_READ, MAP_PRIVATE, fd, 0)); +#endif close(fd); free_data = [=]() { if (buffer != MAP_FAILED) { @@ -163,11 +165,13 @@ extern "C" LEAN_EXPORT object * lean_read_module_data(object * fname, object *) } }; #endif - if (buffer == base_addr) { + if (buffer && buffer == base_addr) { buffer += header_size; is_mmap = true; } else { +#ifdef LEAN_MMAP free_data(); +#endif buffer = static_cast(malloc(size - header_size)); free_data = [=]() { free(buffer); diff --git a/stage0/src/shell/CMakeLists.txt b/stage0/src/shell/CMakeLists.txt index 389bfca006..bda271ca3d 100644 --- a/stage0/src/shell/CMakeLists.txt +++ b/stage0/src/shell/CMakeLists.txt @@ -46,8 +46,14 @@ add_test(lean_ghash2 "${CMAKE_BINARY_DIR}/bin/lean" --githash) add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "-z") add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "boofoo.lean") -# LEANC_OPTS is necessary for macOS c++ to find its headers -set(TEST_VARS "PATH=${LEAN_BIN}:$PATH ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}'") +if(${EMSCRIPTEN}) + set(LEAN_EXE "node --stack-size=8192 ${CMAKE_BINARY_DIR}/bin/lean") +else() + set(LEAN_EXE "lean") +endif() + +# LEANC_OPTS in CXX is necessary for macOS c++ to find its headers +set(TEST_VARS "PATH=${LEAN_BIN}:$PATH ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}' LEAN_EXE='${LEAN_EXE}'") # LEAN TESTS file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") diff --git a/stage0/src/stdlib.make.in b/stage0/src/stdlib.make.in index e8c876b8ad..5d192f9ec6 100644 --- a/stage0/src/stdlib.make.in +++ b/stage0/src/stdlib.make.in @@ -12,7 +12,7 @@ export LEAN_ABORT_ON_PANIC=1 # LEAN_OPTS: don't use native code (except for primitives) since it is from the previous stage # MORE_DEPS: rebuild the stdlib whenever the compiler has changed LEANMAKE_OPTS=\ - LEAN="${CMAKE_CROSSCOMPILING_EMULATOR} ${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\ + LEAN="${PREV_STAGE}/bin/lean${PREV_STAGE_CMAKE_EXECUTABLE_SUFFIX}"\ LEANC="${CMAKE_BINARY_DIR}/leanc.sh"\ OUT="${LIB}"\ LIB_OUT="${LIB}/lean"\ @@ -21,7 +21,7 @@ LEANMAKE_OPTS=\ LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -DwarningAsError=true"\ LEANC_OPTS+="${LEANC_OPTS}"\ LEAN_AR="${CMAKE_AR}"\ - MORE_DEPS+="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\ + MORE_DEPS+="${PREV_STAGE}/bin/lean${PREV_STAGE_CMAKE_EXECUTABLE_SUFFIX}"\ ${EXTRA_LEANMAKE_OPTS}\ CMAKE_LIKE_OUTPUT=1 @@ -52,15 +52,15 @@ leanshared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRAR Lake: # lake is in its own subdirectory, so must adjust relative paths... - +"${LEAN_BIN}/leanmake" -C lake bin lib PKG=Lake BIN_NAME=lake${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='-lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="../${LIB}" LIB_OUT="../${LIB}/lean" OLEAN_OUT="../${LIB}/lean" + +"${LEAN_BIN}/leanmake" -C lake bin lib PKG=Lake BIN_NAME=lake${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="../${LIB}" LIB_OUT="../${LIB}/lean" OLEAN_OUT="../${LIB}/lean" ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} $(LEAN_SHELL) @echo "[ ] Building $@" # on Windows, must remove file before writing a new one (since the old one may be in use) @rm -f $@ - "${CMAKE_BINARY_DIR}/leanc.sh" $(LEAN_SHELL) -lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@ + "${CMAKE_BINARY_DIR}/leanc.sh" $(LEAN_SHELL) ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@ lean: ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX} Leanc: - +"${LEAN_BIN}/leanmake" bin PKG=Leanc BIN_NAME=leanc${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='-lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="${CMAKE_BINARY_DIR}" OLEAN_OUT="${CMAKE_BINARY_DIR}" + +"${LEAN_BIN}/leanmake" bin PKG=Leanc BIN_NAME=leanc${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="${CMAKE_BINARY_DIR}" OLEAN_OUT="${CMAKE_BINARY_DIR}" diff --git a/tests/common.sh b/tests/common.sh index c9fc2fdee9..a64e1a39a3 100644 --- a/tests/common.sh +++ b/tests/common.sh @@ -26,7 +26,7 @@ function lean_has_llvm_support { function compile_lean_c_backend { lean --c="$f.c" "$f" || fail "Failed to compile $f into C file" - leanc -O3 -DNDEBUG -o "$f.out" "$@" "$f.c" || fail "Failed to compile C file $f.c" + leanc ${LEANC_OPTS-} -O3 -DNDEBUG -o "$f.out" "$@" "$f.c" || fail "Failed to compile C file $f.c" } function compile_lean_llvm_backend { @@ -35,7 +35,7 @@ function compile_lean_llvm_backend { rm "*.bc" || true # remove bitcode files rm "*.o" || true # remove object files lean --bc="$f.linked.bc" "$f" || fail "Failed to compile $f into bitcode file" - leanc -o "$f.out" "$@" "$f.linked.bc.o" || fail "Failed to link object file '$f.linked.bc.o'" + leanc ${LEANC_OPTS-} -o "$f.out" "$@" "$f.linked.bc.o" || fail "Failed to link object file '$f.linked.bc.o'" set +o xtrace }