feat: setup Emscripten file paths

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

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"

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

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)

src/runtime/io.cpp

@@ -11,6 +11,9 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 #include <mach-o/dyld.h>
 #include <unistd.h>
 #else
+#if defined(LEAN_EMSCRIPTEN)
+#include <emscripten.h>
+#endif
 // Linux include files
 #include <unistd.h> // NOLINT
 #include <sys/mman.h>
@@ -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<char*>(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

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}

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);