From 485f8ea2d0c699edc90e6705073ab3c95401207f Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 1 Jun 2021 21:02:56 -0400 Subject: [PATCH] feat: setup Emscripten file paths --- CMakeLists.txt | 2 +- src/CMakeLists.txt | 3 ++- src/Init/System/IO.lean | 2 +- src/Lean/Util/Path.lean | 2 -- src/runtime/io.cpp | 26 +++++++++++++++++++++++--- src/shell/CMakeLists.txt | 2 +- src/shell/lean.cpp | 26 ++++++++++---------------- 7 files changed, 38 insertions(+), 25 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index b512d3f081..793c566468 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -19,7 +19,7 @@ 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_SETTINGS "-s ALLOW_MEMORY_GROWTH=1") + set(EMSCRIPTEN_SETTINGS "-s ALLOW_MEMORY_GROWTH=1 -s MAIN_MODULE=1") ExternalProject_Add( gmp URL https://gmplib.org/download/gmp/gmp-6.2.1.tar.bz2 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 39b2d2e478..3cde0c9394 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -122,9 +122,10 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten") set(MULTI_THREAD OFF) # 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 -fexceptions") + set(EMSCRIPTEN_SETTINGS "-s ALLOW_MEMORY_GROWTH=1 -s DISABLE_EXCEPTION_CATCHING=0 -s MAIN_MODULE=1 -fexceptions") set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_EMSCRIPTEN ${EMSCRIPTEN_SETTINGS}") set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} ${EMSCRIPTEN_SETTINGS}") + set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${EMSCRIPTEN_SETTINGS}") endif() if (CMAKE_CROSSCOMPILING_EMULATOR) # emscripten likes to quote "node" diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index d69c2f4beb..b0ba5ee948 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -193,7 +193,7 @@ def fopenFlags (m : FS.Mode) (b : Bool) : String := @[extern "lean_io_getenv"] constant getEnv (var : @& String) : IO (Option String) @[extern "lean_io_realpath"] constant realPath (fname : FilePath) : IO FilePath @[extern "lean_io_remove_file"] constant removeFile (fname : @& FilePath) : IO Unit -@[extern "lean_io_app_dir"] constant appPath : IO FilePath +@[extern "lean_io_app_path"] constant appPath : IO FilePath @[extern "lean_io_current_dir"] constant currentDir : IO FilePath end Prim diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean index 12d637439d..7be0af5257 100644 --- a/src/Lean/Util/Path.lean +++ b/src/Lean/Util/Path.lean @@ -45,8 +45,6 @@ builtin_initialize searchPathRef : IO.Ref SearchPath ← IO.mkRef {} private constant isStage0 (u : Unit) : Bool def getBuiltinSearchPath : IO SearchPath := do - if System.Platform.isEmscripten then - return ["/lib/lean"] let appDir ← IO.appDir let mut buildDir := appDir / ".." -- use stage1 stdlib with stage0 executable (which should never be distributed outside of the build directory) diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index db8dd06dc4..c512e0544d 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -11,6 +11,9 @@ Authors: Leonardo de Moura, Sebastian Ullrich #include #include #else +#if defined(LEAN_EMSCRIPTEN) +#include +#endif // Linux include files #include // NOLINT #include @@ -556,7 +559,7 @@ extern "C" obj_res lean_io_remove_file(b_obj_arg fname, obj_arg) { } } -extern "C" obj_res lean_io_app_dir(obj_arg) { +extern "C" obj_res lean_io_app_path(obj_arg) { #if defined(LEAN_WINDOWS) HMODULE hModule = GetModuleHandleW(NULL); WCHAR path[MAX_PATH]; @@ -579,7 +582,24 @@ extern "C" obj_res lean_io_app_dir(obj_arg) { return io_result_mk_error("failed to resolve symbolic links when locating application"); return io_result_mk_ok(mk_string(buf2)); #elif defined(LEAN_EMSCRIPTEN) - return io_result_mk_error("no app directory exists on Emscripten"); + // See https://emscripten.org/docs/api_reference/emscripten.h.html#c.EM_ASM_INT + char* appPath = reinterpret_cast(EM_ASM_INT({ + if ((typeof process === "undefined") || (process.release.name !== "node")) { + return 0; + } + + var lengthBytes = lengthBytesUTF8(__filename)+1; + var pathOnWasmHeap = _malloc(lengthBytes); + stringToUTF8(__filename, pathOnWasmHeap, lengthBytes); + return pathOnWasmHeap; + })); + if (appPath == nullptr) { + return io_result_mk_error("no Lean executable file exists in WASM outside of Node.js"); + } + + object * appPathLean = mk_string(appPath); + free(appPath); + return io_result_mk_ok(appPathLean); #else // Linux version char path[PATH_MAX]; @@ -816,7 +836,7 @@ void initialize_io() { mark_persistent(g_stream_stderr); g_stream_stdin = lean_stream_of_handle(io_wrap_handle(stdin)); mark_persistent(g_stream_stdin); -#ifndef LEAN_WINDOWS +#if !defined(LEAN_WINDOWS) && !defined(LEAN_EMSCRIPTEN) // We want to handle SIGPIPE ourselves lean_always_assert(signal(SIGPIPE, SIG_IGN) != SIG_ERR); #endif diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 1ca538137c..aeee171b97 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -2,7 +2,7 @@ if (${CMAKE_SYSTEM_NAME} MATCHES "Emscripten") add_executable(lean lean.cpp) set_target_properties(lean PROPERTIES RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/bin/") - target_link_libraries(lean Init Std Lean leancpp "${GMP_INSTALL_PREFIX}/lib/libgmp.a") + target_link_libraries(lean Init Std Lean leancpp "${GMP_INSTALL_PREFIX}/lib/libgmp.a" "-lnodefs.js") else () add_library(shell OBJECT lean.cpp) add_custom_command(OUTPUT ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX} diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 881006a4cf..fe8ad8d814 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -381,24 +381,18 @@ void check_optarg(char const * option_name) { int main(int argc, char ** argv) { #ifdef LEAN_EMSCRIPTEN - // TODO(WN): Node.js stuff - /*EM_ASM( - var lean_path = process.env['LEAN_PATH']; - if (lean_path) { - ENV['LEAN_PATH'] = lean_path; + // When running in command-line mode under Node.js, we make system directories available in the virtual filesystem. + // This mode is used to compile 32-bit oleans. + EM_ASM( + if ((typeof process === "undefined") || (process.release.name !== "node")) { + throw new Error("The Lean command-line driver can only run under Node.js. For the embeddable WASM library, see lean_wasm.cpp."); } - try { - // emscripten cannot mount all of / in the vfs, - // we can only mount subdirectories... - FS.mount(NODEFS, { root: '/home' }, '/home'); - FS.mkdir('/root'); - FS.mount(NODEFS, { root: '/root' }, '/root'); - - FS.chdir(process.cwd()); - } catch (e) { - console.log(e); - });*/ + // We cannot mount /, see https://github.com/emscripten-core/emscripten/issues/2040 + FS.mount(NODEFS, { root: "/home" }, "/home"); + FS.mount(NODEFS, { root: "/tmp" }, "/tmp"); + FS.chdir(process.cwd()); + ); #elif defined(LEAN_WINDOWS) // "best practice" according to https://docs.microsoft.com/en-us/windows/win32/api/errhandlingapi/nf-errhandlingapi-seterrormode SetErrorMode(SEM_FAILCRITICALERRORS);