diff --git a/bin/linja.in b/bin/linja.in index 191f0f5bba..7c5eeb2448 100755 --- a/bin/linja.in +++ b/bin/linja.in @@ -463,7 +463,7 @@ def make_build_ninja(args): print("""rule LEAN""", file=f) print(""" depfile = ${DLEAN_FILE}""", file=f) - print(""" command = "%s" %s $in -o "${OLEAN_FILE}" """ \ + print(""" command = "%s" %s -o ${OLEAN_FILE} $in""" \ % (g_lean_path, " ".join(args.lean_options)), file=f) print("build all: phony", end=' ', file=f) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 69734f9df5..1884de39bc 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -4,6 +4,19 @@ set(LEAN_VERSION_MAJOR 0) set(LEAN_VERSION_MINOR 3) set(LEAN_VERSION_PATCH 0) +set(LEAN_EXTRA_LINKER_FLAGS "") +set(LEAN_EXTRA_CXX_FLAGS "") + +if("${CMAKE_C_COMPILER}" MATCHES "emcc") + set(EMSCRIPTEN ON) + set(CROSS_COMPILE ON) + set(IGNORE_SORRY ON) + set(MULTI_THREAD OFF) + set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_EMSCRIPTEN") + set(LEAN_JS_LIBRARY "${CMAKE_CURRENT_SOURCE_DIR}/../library" CACHE STRING + "location of olean files for lean.js") +endif() + if (NOT CMAKE_BUILD_TYPE) message(STATUS "No build type selected, default to Release") set(CMAKE_BUILD_TYPE "Release") @@ -63,9 +76,6 @@ include(CTest) configure_file("${LEAN_SOURCE_DIR}/CTestCustom.cmake.in" "${LEAN_BINARY_DIR}/CTestCustom.cmake" @ONLY) -set(LEAN_EXTRA_LINKER_FLAGS "") -set(LEAN_EXTRA_CXX_FLAGS "") - # Windows does not support ulimit -s unlimited. So, we reserve a lot of stack space: 100Mb if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows")) message(STATUS "Windows detected") @@ -112,12 +122,6 @@ if(STATIC) set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -static") endif() -if("${CMAKE_C_COMPILER}" MATCHES "emcc") - set(EMSCRIPTEN ON) - set(CROSS_COMPILE ON) - set(IGNORE_SORRY ON) -endif() - # Set Module Path set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules") @@ -128,7 +132,7 @@ set(CMAKE_CXX_FLAGS_MINSIZEREL "-Os -DNDEBUG") set(CMAKE_CXX_FLAGS_RELEASE "-O3 -DNDEBUG") set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g") set(CMAKE_CXX_FLAGS_GPROF "-O2 -g -pg") -set(CMAKE_CXX_FLAGS_EMSCRIPTEN "-Oz -O3 -s ALLOW_MEMORY_GROWTH=1 --llvm-lto 1 -s DISABLE_EXCEPTION_CATCHING=0 -D LEAN_EMSCRIPTEN -Wno-warn-absolute-paths --bind") +set(CMAKE_CXX_FLAGS_EMSCRIPTEN "-Oz -O3 -s ALLOW_MEMORY_GROWTH=1 --llvm-lto 1 -s DISABLE_EXCEPTION_CATCHING=0 -Wno-warn-absolute-paths") # OSX .dmg generation (this is working in progress) set(CPACK_DMG_BACKGROUND_IMAGE "${LEAN_SOURCE_DIR}/../images/lean.png") @@ -209,15 +213,47 @@ if (BOOST AND MULTI_THREAD) endif() endif() -# MPFR -find_package(MPFR 3.1.0 REQUIRED) -include_directories(${MPFR_INCLUDES}) -set(EXTRA_LIBS ${EXTRA_LIBS} ${MPFR_LIBRARIES}) +if (${EMSCRIPTEN}) + include(ExternalProject) + set(gmp_install_prefix ${CMAKE_CURRENT_BINARY_DIR}/gmp-root) + # The plethory of configure arguments only makes sure that gmp thinks sizeof(mp_limb_t) == sizeof(long) == 4 + ExternalProject_Add( + gmp + URL https://leanprover.github.io/lean.js/gmp-5.1.1.tar.bz2 + URL_HASH SHA256=9a30128284cb710cdc0d71866ed582bc0c97cff3a077ff70739f1d979c76279e + BUILD_IN_SOURCE 1 + CONFIGURE_COMMAND emconfigure ./configure CFLAGS=-m32\ -DPIC --build=i686-pc-linux-gnu --disable-assembly --prefix=${gmp_install_prefix} + BUILD_COMMAND emmake make -j4 + INSTALL_COMMAND make install + ) + set(mpfr_install_prefix ${CMAKE_CURRENT_BINARY_DIR}/mpfr-root) + ExternalProject_Add( + mpfr + DEPENDS gmp + URL https://leanprover.github.io/lean.js/mpfr-3.1.1.tar.bz2 + URL_HASH SHA256=7b66c3f13dc8385f08264c805853f3e1a8eedab8071d582f3e661971c9acd5fd + BUILD_IN_SOURCE 1 + CONFIGURE_COMMAND emconfigure ./configure --prefix=${mpfr_install_prefix} --with-gmp-include=${gmp_install_prefix}/include --with-gmp-lib=${gmp_install_prefix}/lib + BUILD_COMMAND emmake make -j4 + INSTALL_COMMAND make install + ) -# GMP -find_package(GMP 5.0.5 REQUIRED) -include_directories(${GMP_INCLUDE_DIR}) -set(EXTRA_LIBS ${EXTRA_LIBS} ${GMP_LIBRARIES}) + add_library(lean_external_deps INTERFACE) + target_link_libraries(lean_external_deps INTERFACE ${gmp_install_prefix}/lib/libgmp.a ${mpfr_install_prefix}/lib/libmpfr.a) + include_directories(lean_external_deps INTERFACE ${gmp_install_prefix}/include ${mpfr_install_prefix}/include) + add_dependencies(lean_external_deps gmp mpfr) + set(EXTRA_LIBS lean_external_deps) +else() + # MPFR + find_package(MPFR 3.1.0 REQUIRED) + include_directories(${MPFR_INCLUDES}) + set(EXTRA_LIBS ${EXTRA_LIBS} ${MPFR_LIBRARIES}) + + # GMP + find_package(GMP 5.0.5 REQUIRED) + include_directories(${GMP_INCLUDE_DIR}) + set(EXTRA_LIBS ${EXTRA_LIBS} ${GMP_LIBRARIES}) +endif() # TRACK_MEMORY_USAGE if(TRACK_MEMORY_USAGE) @@ -362,9 +398,13 @@ if(MULTI_THREAD AND (NOT ("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")) AND (NOT BOO set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread") endif() set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage") -if(NOT EMSCRIPTEN) - add_library(leanstatic ${LEAN_OBJS}) +if(EMSCRIPTEN) + set(LEAN_LIBRARY_TYPE SHARED) +else() + set(LEAN_LIBRARY_TYPE STATIC) endif() +add_library(leanstatic ${LEAN_LIBRARY_TYPE} ${LEAN_OBJS}) +target_link_libraries(leanstatic ${EXTRA_LIBS}) if ((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows")) set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -Wl,--export-all") endif() @@ -416,30 +456,6 @@ add_style_check_target(style "${LEAN_SOURCES}") add_test(NAME style_check COMMAND "${PYTHON_EXECUTABLE}" "${LEAN_SOURCE_DIR}/cmake/Modules/cpplint.py" ${LEAN_SOURCES}) endif() -# Set PROCESSOR_COUNT -if(NOT DEFINED PROCESSOR_COUNT) - # Unknown: - set(PROCESSOR_COUNT 1) - - # Linux: - set(cpuinfo_file "/proc/cpuinfo") - if(EXISTS "${cpuinfo_file}") - file(STRINGS "${cpuinfo_file}" procs REGEX "^processor.: [0-9]+$") - list(LENGTH procs PROCESSOR_COUNT) - endif() - - # Mac: - if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") - execute_process(COMMAND "sysctl" "hw.ncpu" OUTPUT_VARIABLE info) - string(REGEX REPLACE "^hw.ncpu: ([0-9]+).*$" "\\1" PROCESSOR_COUNT "${info}") - endif() - - # Windows: - if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") - set(PROCESSOR_COUNT "$ENV{NUMBER_OF_PROCESSORS}") - endif() -endif() - if("${CROSS_COMPILE}" MATCHES "ON" OR "${CMAKE_C_COMPILER}" MATCHES "emcc") message(STATUS "Lean standard library will not be compiled when using cross-compilation.") else() diff --git a/src/library/module.cpp b/src/library/module.cpp index a1729a3c40..022c56e7ef 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -344,7 +344,6 @@ struct import_modules_fn { } module_info_ptr load_module_file(std::string const & base, module_name const & mname) { - std::string fname_lean = find_lean_file(base, mname); std::string fname = find_olean_file(base, mname); auto it = m_module_info.find(fname); if (it) @@ -357,8 +356,11 @@ struct import_modules_fn { try { module_metadata metadata; metadata.m_mname = mname; - metadata.m_lean_mod_time = get_mtime(fname_lean); - metadata.m_olean_mod_time = get_mtime(fname); + try { + std::string fname_lean = find_lean_file(base, mname); + metadata.m_lean_mod_time = get_mtime(fname_lean); + } catch (...) {} + try { metadata.m_olean_mod_time = get_mtime(fname); } catch (...) {} m_imported.insert(fname, metadata); unsigned major, minor, patch, claimed_hash; @@ -500,7 +502,7 @@ struct import_modules_fn { object_readers & readers = get_object_readers(); auto it = readers.find(k); if (it == readers.end()) - throw exception(sstream() << "file '" << r->m_fname << "' has been corrupted, unknown object"); + throw exception(sstream() << "file '" << r->m_fname << "' has been corrupted, unknown object: " << k); it->second(d, m_senv, add_asynch_update, add_delayed_update); } obj_counter++; diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 3c86962292..b2377d6683 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -1,19 +1,49 @@ +add_executable(lean lean.cpp json.cpp server.cpp) +target_link_libraries(lean leanstatic) +install(TARGETS lean DESTINATION bin) + +add_executable(lean_js lean_js.cpp) +target_link_libraries(lean_js leanstatic) + if(${EMSCRIPTEN}) - add_executable(lean.js lean.cpp emscripten.cpp ${LEAN_OBJS}) - target_link_libraries(lean.js ${EXTRA_LIBS} "--embed-file library --memory-init-file 0") + target_link_libraries(lean "--memory-init-file 0") + + file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/run_lean_js + "#!/bin/sh\nLEAN_PATH=${CMAKE_CURRENT_SOURCE_DIR}/../../library node ${CMAKE_CURRENT_BINARY_DIR}/lean.js \"$@\"\n") + execute_process(COMMAND chmod +x ${CMAKE_CURRENT_BINARY_DIR}/run_lean_js) + + # FIXME(gabriel): we rebuild the library using lean.js because the serialization is different + file(READ ${CMAKE_CURRENT_SOURCE_DIR}/../../bin/linja.in linja_code) + string(REGEX REPLACE "\ng_lean_path[^\n]* = [^\n]*" "\ng_lean_path = '${CMAKE_CURRENT_BINARY_DIR}/run_lean_js'" linja_js_code ${linja_code}) + string(REGEX REPLACE "ninja_option = \\[\\]" "ninja_option = ['-j1']" linja_js_code ${linja_js_code}) + string(REGEX REPLACE " make_deps_all_files\\(args\\)" " #" linja_js_code ${linja_js_code}) + file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/linja_js ${linja_js_code}) + execute_process(COMMAND chmod +x ${CMAKE_CURRENT_BINARY_DIR}/linja_js) + add_custom_target(build_lean_js_library + COMMAND find -name \\*.olean -exec rm '{}' \\\; + COMMAND ${CMAKE_CURRENT_BINARY_DIR}/linja_js + WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/../../library) + + # copy olean files from the library into build/emscripten/shell/library/... + add_custom_target(lean_js_library + COMMAND rm -rf ${CMAKE_CURRENT_BINARY_DIR}/library + COMMAND mkdir -p ${CMAKE_CURRENT_BINARY_DIR}/library + COMMAND bash -c "(cd ${LEAN_JS_LIBRARY}; tar c `find -name '*.olean'`) | (cd ${CMAKE_CURRENT_BINARY_DIR}/library; tar x)" + VERBATIM) + + file(COPY ${CMAKE_CURRENT_SOURCE_DIR}/lean_js.html DESTINATION ${CMAKE_CURRENT_BINARY_DIR}) + + target_link_libraries(lean_js "--embed-file library --memory-init-file 0 --bind") + add_dependencies(lean_js lean_js_library) + set_target_properties(lean_js PROPERTIES COMPILE_FLAGS --bind -s NO_EXIT_RUNTIME=1) else() - add_executable(lean lean.cpp emscripten.cpp json.cpp server.cpp) - target_link_libraries(lean leanstatic ${EXTRA_LIBS}) ADD_CUSTOM_COMMAND(TARGET lean POST_BUILD COMMAND "${CMAKE_COMMAND}" -E make_directory "${LEAN_SOURCE_DIR}/../bin" COMMAND "${CMAKE_COMMAND}" -E copy "${CMAKE_CURRENT_BINARY_DIR}/lean${CMAKE_EXECUTABLE_SUFFIX}" "${LEAN_SOURCE_DIR}/../bin/" ) - install(TARGETS lean DESTINATION bin) endif() -add_library(shell OBJECT emscripten.cpp) - # add_test(example1_stdin1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../tests/lean/single.lean") # add_test(lean_export ${CMAKE_CURRENT_BINARY_DIR}/lean "-o simple.olean" "${LEAN_SOURCE_DIR}/../tests/lean/run/simple.lean") add_test(lean_help1 "${CMAKE_CURRENT_BINARY_DIR}/lean" --help) diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 3f7e87aed8..dcb44d3b29 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -37,12 +37,14 @@ Author: Leonardo de Moura #include "frontends/lean/opt_cmd.h" #include "frontends/smt2/parser.h" #include "init/init.h" -#include "shell/emscripten.h" #include "shell/simple_pos_info_provider.h" #include "shell/json.h" #if defined(LEAN_SERVER) #include "shell/server.h" #endif +#if defined(LEAN_EMSCRIPTEN) +#include +#endif #include "version.h" #include "githash.h" // NOLINT @@ -210,15 +212,6 @@ options set_config_option(options const & opts, char const * in) { } } -#if defined(LEAN_EMSCRIPTEN) -#include -EMSCRIPTEN_BINDINGS(LEAN_JS) { - emscripten::function("lean_init", &initialize_emscripten); - emscripten::function("lean_import_module", &emscripten_import_module); - emscripten::function("lean_process_file", &emscripten_process_file); -} -int main() { return 0; } -#else class initializer { private: lean::initializer m_init; @@ -236,6 +229,26 @@ public: }; int main(int argc, char ** argv) { +#if defined(LEAN_EMSCRIPTEN) + EM_ASM( + var lean_path = process.env['LEAN_PATH']; + if (lean_path) { + ENV['LEAN_PATH'] = lean_path; + } + + 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); + } + ); +#endif initializer init; bool export_objects = false; unsigned trust_lvl = LEAN_BELIEVER_TRUST_LEVEL+1; @@ -449,4 +462,3 @@ int main(int argc, char ** argv) { } return 1; } -#endif diff --git a/src/shell/lean_js.cpp b/src/shell/lean_js.cpp new file mode 100644 index 0000000000..c8b5c54bec --- /dev/null +++ b/src/shell/lean_js.cpp @@ -0,0 +1,103 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "library/flycheck.h" +#include "library/module.h" +#include "library/standard_kernel.h" +#include "library/type_context.h" +#include "frontends/lean/pp.h" +#include "frontends/lean/parser.h" +#include "init/init.h" +#include "shell/simple_pos_info_provider.h" + +namespace lean { +class emscripten_shell { +private: + unsigned trust_lvl; + unsigned num_threads; + options opts; + environment env; + io_state ios; + +public: + emscripten_shell() : trust_lvl(LEAN_BELIEVER_TRUST_LEVEL+1), num_threads(1), + env(mk_environment(trust_lvl)), ios(opts, lean::mk_pretty_formatter_factory()) { + ios.set_message_channel(std::make_shared(std::cout)); + } + + int import_module(std::string mname) { + try { + module_name mod(mname); + std::string base = "."; + bool num_threads = 1; + // FIXME(gabriel): discarding proofs fails at the moment with "invalid equation lemma, unexpected form" + bool keep_proofs = true; + env = import_modules(env, base, 1, &mod, num_threads, keep_proofs, ios); + } catch (lean::exception & ex) { + lean::message_builder(env, ios, "import_module", lean::pos_info(1, 1), lean::ERROR).set_exception(ex).report(); + return 1; + } + return 0; + } + + int process_file(std::string input_filename) { + bool ok = true; + try { + environment temp_env(env); + io_state temp_ios(ios); + if (!parse_commands(temp_env, temp_ios, input_filename.c_str(), optional(), false, num_threads)) { + ok = false; + } + } catch (lean::exception & ex) { + lean::message_builder(env, ios, input_filename, lean::pos_info(1, 1), lean::ERROR).set_exception(ex).report(); + ok = false; + } + return ok ? 0 : 1; + } +}; +} + +static lean::initializer * g_init = nullptr; +static lean::emscripten_shell * g_shell = nullptr; + +void initialize_emscripten() { + g_init = new lean::initializer(); + g_shell = new lean::emscripten_shell(); +} + +void finalize_emscripten() { + delete g_shell; + delete g_init; +} + +int emscripten_import_module(std::string mname) { + return g_shell->import_module(mname); +} + +int emscripten_process_file(std::string input_filename) { + return g_shell->process_file(input_filename); +} + +#if defined(LEAN_EMSCRIPTEN) + +#include +EMSCRIPTEN_BINDINGS(LEAN_JS) { + emscripten::function("lean_init", &initialize_emscripten); + emscripten::function("lean_import_module", &emscripten_import_module); + emscripten::function("lean_process_file", &emscripten_process_file); +} + +int main() { return 0; } + +#else + +int main(int, char **) { + initialize_emscripten(); + emscripten_import_module("standard"); +} + +#endif diff --git a/src/shell/emscripten.h b/src/shell/lean_js.h similarity index 100% rename from src/shell/emscripten.h rename to src/shell/lean_js.h diff --git a/src/shell/lean_js.html b/src/shell/lean_js.html new file mode 100644 index 0000000000..be9938eee8 --- /dev/null +++ b/src/shell/lean_js.html @@ -0,0 +1,81 @@ + + + lean.js minimal working example + + + + +

Small example of using lean.js

+ +

+
+
+
+
+
+
+
+
+
diff --git a/src/shell/server.cpp b/src/shell/server.cpp
index 40643d0dd3..05e11e5407 100644
--- a/src/shell/server.cpp
+++ b/src/shell/server.cpp
@@ -56,7 +56,9 @@ void server::run() {
     /* Leo: we use std::setlocale to make sure decimal period is displayed as ".".
        We added this hack because the json library code used for ensuring this property
        was crashing when compiling Lean on Windows with mingw. */
+#if !defined(LEAN_EMSCRIPTEN)
     std::setlocale(LC_NUMERIC, "C");
+#endif
     while (true) {
         try {
             std::string req_string;
diff --git a/src/tests/shell/CMakeLists.txt b/src/tests/shell/CMakeLists.txt
index e402feeebb..f41ef2bb3c 100644
--- a/src/tests/shell/CMakeLists.txt
+++ b/src/tests/shell/CMakeLists.txt
@@ -1,4 +1,4 @@
-add_executable(shell_test shell.cpp ${LEAN_OBJS} $)
+add_executable(shell_test shell.cpp ${LEAN_OBJS})
 target_link_libraries(shell_test ${EXTRA_LIBS})
 
 # TODO(Leo): add after stdlib is activated again
diff --git a/src/tests/shell/shell.cpp b/src/tests/shell/shell.cpp
index 30db9992d9..08235f3df9 100644
--- a/src/tests/shell/shell.cpp
+++ b/src/tests/shell/shell.cpp
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #include 
 #include "util/test.h"
-#include "shell/emscripten.h"
+#include "shell/lean_js.h"
 using namespace lean;
 
 int main() {
diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp
index 973b580532..7632b038f1 100644
--- a/src/util/lean_path.cpp
+++ b/src/util/lean_path.cpp
@@ -40,7 +40,13 @@ bool is_directory(char const * pathname) {
     return info.st_mode & S_IFDIR;
 }
 
-#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+#if defined(LEAN_EMSCRIPTEN)
+// emscripten version
+static char g_path_sep     = ':';
+static char g_sep          = '/';
+static char g_bad_sep      = '\\';
+bool is_path_sep(char c) { return c == g_path_sep; }
+#elif defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
 // Windows version
 static char g_path_sep     = ';';
 static char g_path_alt_sep = ':';
@@ -118,19 +124,19 @@ std::string get_path(std::string f) {
 }
 
 void init_lean_path() {
-#if defined(LEAN_EMSCRIPTEN)
-    *g_lean_path = "/library";
-    g_lean_path_vector->push_back(*g_lean_path);
-#else
     char * r = nullptr;
     r = getenv("LEAN_PATH");
     if (r == nullptr) {
+#ifdef LEAN_EMSCRIPTEN
+        *g_lean_path = "/library";
+#else
         std::string exe_path = get_path(get_exe_location());
         *g_lean_path  = exe_path + g_sep + ".." + g_sep + "library";
         *g_lean_path += g_path_sep;
         *g_lean_path += exe_path + g_sep + ".." + g_sep + "lib" + g_sep + "lean" + g_sep + "library";
         *g_lean_path += g_path_sep;
         *g_lean_path += ".";
+#endif
     } else {
         *g_lean_path = r;
     }
@@ -148,7 +154,6 @@ void init_lean_path() {
     }
     if (j > i)
         g_lean_path_vector->push_back(g_lean_path->substr(i, j - i));
-#endif
 }
 
 static char g_sep_str[2];
diff --git a/src/util/name.cpp b/src/util/name.cpp
index fff8184e7c..16e8736877 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -85,10 +85,8 @@ name::name(name const & prefix, char const * name) {
     m_ptr      = new (mem) imp(true, prefix.m_ptr);
     std::memcpy(mem + sizeof(imp), name, sz + 1);
     m_ptr->m_str       = mem + sizeof(imp);
-    if (m_ptr->m_prefix)
-        m_ptr->m_hash = hash_str(sz, name, m_ptr->m_prefix->m_hash);
-    else
-        m_ptr->m_hash = hash_str(sz, name, 0);
+    // Emscripten easily breaks with small changes here.  The main fix seems to be to use m_ptr->m_str instead of name.
+    m_ptr->m_hash = hash_str(static_cast(sz), m_ptr->m_str, prefix.hash());
 }
 
 name::name(name const & prefix, unsigned k, bool) {
diff --git a/src/util/realpath.cpp b/src/util/realpath.cpp
index 320f18dbcb..5770f8d333 100644
--- a/src/util/realpath.cpp
+++ b/src/util/realpath.cpp
@@ -21,7 +21,9 @@ Author: Leonardo de Moura
 
 namespace lean {
 std::string lrealpath(char const * fname) {
-#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+#if defined(LEAN_EMSCRIPTEN)
+    return fname;
+#elif defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
     constexpr unsigned BufferSize = 8192;
     char buffer[BufferSize];
     DWORD retval = GetFullPathName(fname, BufferSize, buffer, nullptr);