diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d457cd6ae8a1..b80da01759d9 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -257,7 +257,7 @@ jobs: "cross": true, "shell": "bash -euxo pipefail {0}", // Just a few selected tests because wasm is slow - "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean|leanruntest_libuv\\.lean\"" + "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean|leanruntest_tempfile.lean\\.|leanruntest_libuv\\.lean\"" } ]; console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`) @@ -452,7 +452,7 @@ jobs: run: ccache -s # This job collects results from all the matrix jobs - # This can be made the “required” job, instead of listing each + # This can be made the "required" job, instead of listing each # matrix job separately all-done: name: Build matrix complete diff --git a/flake.nix b/flake.nix index af0139b5c668..abe17a33b856 100644 --- a/flake.nix +++ b/flake.nix @@ -39,7 +39,19 @@ CTEST_OUTPUT_ON_FAILURE = 1; } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux { GMP = pkgsDist.gmp.override { withStatic = true; }; - LIBUV = pkgsDist.libuv.overrideAttrs (attrs: { configureFlags = ["--enable-static"]; }); + LIBUV = pkgsDist.libuv.overrideAttrs (attrs: { + configureFlags = ["--enable-static"]; + hardeningDisable = [ "stackprotector" ]; + # Sync version with CMakeLists.txt + version = "1.48.0"; + src = pkgs.fetchFromGitHub { + owner = "libuv"; + repo = "libuv"; + rev = "v1.48.0"; + sha256 = "100nj16fg8922qg4m2hdjh62zv4p32wyrllsvqr659hdhjc03bsk"; + }; + doCheck = false; + }); GLIBC = pkgsDist.glibc; GLIBC_DEV = pkgsDist.glibc.dev; GCC_LIB = pkgsDist.gcc.cc.lib; diff --git a/script/prepare-llvm-linux.sh b/script/prepare-llvm-linux.sh index 40c9889788af..f1a872a8eff2 100755 --- a/script/prepare-llvm-linux.sh +++ b/script/prepare-llvm-linux.sh @@ -48,6 +48,7 @@ $CP llvm-host/lib/*/lib{c++,c++abi,unwind}.* llvm-host/lib/ $CP -r llvm/include/*-*-* llvm-host/include/ # glibc: use for linking (so Lean programs don't embed newer symbol versions), but not for running (because libc.so, librt.so, and ld.so must be compatible)! $CP $GLIBC/lib/libc_nonshared.a stage1/lib/glibc +$CP $GLIBC/lib/libpthread_nonshared.a stage1/lib/glibc for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done OPTIONS=() echo -n " -DLEAN_STANDALONE=ON" @@ -62,8 +63,8 @@ fi # use `-nostdinc` to make sure headers are not visible by default (in particular, not to `#include_next` in the clang headers), # but do not change sysroot so users can still link against system libs echo -n " -DLEANC_INTERNAL_FLAGS='-nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang" -echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'" +echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a ROOT/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -lpthread -ldl -lrt -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'" # when not using the above flags, link GMP dynamically/as usual -echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -Wl,--no-as-needed'" +echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed'" # do not set `LEAN_CC` for tests echo -n " -DLEAN_TEST_VARS=''" diff --git a/script/prepare-llvm-mingw.sh b/script/prepare-llvm-mingw.sh index 749fc9d9fac4..4d32632197c0 100644 --- a/script/prepare-llvm-mingw.sh +++ b/script/prepare-llvm-mingw.sh @@ -31,15 +31,15 @@ cp /clang64/lib/{crtbegin,crtend,crt2,dllcrt2}.o stage1/lib/ # runtime (cd llvm; cp --parents lib/clang/*/lib/*/libclang_rt.builtins* ../stage1) # further dependencies -cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase}.* /clang64/lib/libgmp.a /clang64/lib/libuv.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/ +cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase,psapi,iphlpapi,userenv,ws2_32,dbghelp,ole32}.* /clang64/lib/libgmp.a /clang64/lib/libuv.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/ echo -n " -DLEAN_STANDALONE=ON" echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang.exe -DCMAKE_C_COMPILER_WORKS=1 -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++.exe -DCMAKE_CXX_COMPILER_WORKS=1 -DLEAN_CXX_STDLIB='-lc++ -lc++abi'" echo -n " -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_CXX_COMPILER=clang++" echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter /clang64/include/'" echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang.exe" -echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -static-libgcc -Wl,-Bstatic -lgmp -luv -lunwind -Wl,-Bdynamic -fuse-ld=lld'" +echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -static-libgcc -Wl,-Bstatic -lgmp $(pkg-config --static --libs libuv) -lunwind -Wl,-Bdynamic -fuse-ld=lld'" # when not using the above flags, link GMP dynamically/as usual -echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv -lucrtbase'" +echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp $(pkg-config --libs libuv) -lucrtbase'" # do not set `LEAN_CC` for tests echo -n " -DAUTO_THREAD_FINALIZATION=OFF -DSTAGE0_AUTO_THREAD_FINALIZATION=OFF" echo -n " -DLEAN_TEST_VARS=''" diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 825c3ec998c6..37ed6ba754b5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -243,11 +243,56 @@ if("${USE_GMP}" MATCHES "ON") endif() endif() -if(NOT "${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten") - # LibUV +# LibUV +if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten") + # Only on WebAssembly we compile LibUV ourselves + set(LIBUV_EMSCRIPTEN_FLAGS "${EMSCRIPTEN_SETTINGS}") + + # LibUV does not compile on WebAssembly without modifications because + # building LibUV on a platform requires including stub implementations + # for features not present on the target platform. This patch includes + # the minimum amount of stub implementations needed for successfully + # running Lean on WebAssembly and using LibUV's temporary file support. + # It still leaves several symbols completely undefined: uv__fs_event_close, + # uv__hrtime, uv__io_check_fd, uv__io_fork, uv__io_poll, uv__platform_invalidate_fd + # uv__platform_loop_delete, uv__platform_loop_init. Making additional + # LibUV features available on WebAssembly might require adapting the + # patch to include additional LibUV source files. + set(LIBUV_PATCH_IN " +diff --git a/CMakeLists.txt b/CMakeLists.txt +index 5e8e0166..f3b29134 100644 +--- a/CMakeLists.txt ++++ b/CMakeLists.txt +@@ -317,6 +317,11 @@ if(CMAKE_SYSTEM_NAME STREQUAL \"GNU\") + src/unix/hurd.c) + endif() + ++if(CMAKE_SYSTEM_NAME STREQUAL \"Emscripten\") ++ list(APPEND uv_sources ++ src/unix/no-proctitle.c) ++endif() ++ + if(CMAKE_SYSTEM_NAME STREQUAL \"Linux\") + list(APPEND uv_defines _GNU_SOURCE _POSIX_C_SOURCE=200112) + list(APPEND uv_libraries dl rt) +") + string(REPLACE "\n" "\\n" LIBUV_PATCH ${LIBUV_PATCH_IN}) + + ExternalProject_add(libuv + PREFIX libuv + GIT_REPOSITORY https://github.com/libuv/libuv + # Sync version with flake.nix + GIT_TAG v1.48.0 + CMAKE_ARGS -DCMAKE_BUILD_TYPE=Release -DLIBUV_BUILD_TESTS=OFF -DLIBUV_BUILD_SHARED=OFF -DCMAKE_AR=${CMAKE_AR} -DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DCMAKE_C_FLAGS=${LIBUV_EMSCRIPTEN_FLAGS} + PATCH_COMMAND git reset --hard HEAD && printf "${LIBUV_PATCH}" > patch.diff && git apply patch.diff + BUILD_IN_SOURCE ON + INSTALL_COMMAND "") + set(LIBUV_INCLUDE_DIR "${CMAKE_BINARY_DIR}/libuv/src/libuv/include") + set(LIBUV_LIBRARIES "${CMAKE_BINARY_DIR}/libuv/src/libuv/libuv.a") +else() find_package(LibUV 1.0.0 REQUIRED) - include_directories(${LIBUV_INCLUDE_DIR}) endif() +include_directories(${LIBUV_INCLUDE_DIR}) if(NOT LEAN_STANDALONE) string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${LIBUV_LIBRARIES}") endif() @@ -513,6 +558,10 @@ if(${STAGE} GREATER 1) endif() else() add_subdirectory(runtime) + if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten") + add_dependencies(leanrt libuv) + add_dependencies(leanrt_initial-exec libuv) + endif() add_subdirectory(util) set(LEAN_OBJS ${LEAN_OBJS} $) @@ -553,7 +602,7 @@ if (${CMAKE_SYSTEM_NAME} MATCHES "Emscripten") # 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 LEAN_EXE_LINKER_FLAGS " ${LIB}/temp/libleanshell.a ${TOOLCHAIN_STATIC_LINKER_FLAGS} ${EMSCRIPTEN_SETTINGS} -lnodefs.js -s EXIT_RUNTIME=1 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1") + string(APPEND LEAN_EXE_LINKER_FLAGS " ${LIB}/temp/libleanshell.a ${TOOLCHAIN_STATIC_LINKER_FLAGS} ${EMSCRIPTEN_SETTINGS} -lnodefs.js -s EXIT_RUNTIME=1 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1 -s ERROR_ON_UNDEFINED_SYMBOLS=0") endif() # Build the compiler using the bootstrapped C sources for stage0, and use diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index e2f704a80d49..cfaf8be2d57a 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -1916,6 +1916,7 @@ LEAN_EXPORT lean_object * lean_dbg_trace_if_shared(lean_obj_arg s, lean_obj_arg /* IO Helper functions */ LEAN_EXPORT lean_obj_res lean_decode_io_error(int errnum, b_lean_obj_arg fname); +LEAN_EXPORT lean_obj_res lean_decode_uv_error(int errnum, b_lean_obj_arg fname); static inline lean_obj_res lean_io_mk_world() { return lean_box(0); } static inline bool lean_io_result_is_ok(b_lean_obj_arg r) { return lean_ptr_tag(r) == 0; } diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index db628b207d7f..afeea75c92ff 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -39,6 +39,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich #include #include #include +#include #include "util/io.h" #include "runtime/alloc.h" #include "runtime/io.h" @@ -157,6 +158,7 @@ static FILE * io_get_handle(lean_object * hfile) { extern "C" LEAN_EXPORT obj_res lean_decode_io_error(int errnum, b_obj_arg fname) { object * details = mk_string(strerror(errnum)); + // Keep in sync with lean_decode_uv_error below switch (errnum) { case EINTR: lean_assert(fname != nullptr); @@ -251,6 +253,113 @@ extern "C" LEAN_EXPORT obj_res lean_decode_io_error(int errnum, b_obj_arg fname) } } +extern "C" LEAN_EXPORT obj_res lean_decode_uv_error(int errnum, b_obj_arg fname) { + object * details = mk_string(uv_strerror(errnum)); + // Keep in sync with lean_decode_io_error above + switch (errnum) { + case UV_EINTR: + lean_assert(fname != nullptr); + inc_ref(fname); + return lean_mk_io_error_interrupted(fname, errnum, details); + /* LibUV does not map EDOM, ENOEXEC and ENOSTR as of version 1.48.0 */ + case UV_ELOOP: case UV_ENAMETOOLONG: case UV_EDESTADDRREQ: + case UV_EBADF: case UV_EINVAL: case UV_EILSEQ: + case UV_ENOTCONN: case UV_ENOTSOCK: + if (fname == nullptr) { + return lean_mk_io_error_invalid_argument(errnum, details); + } else { + inc_ref(fname); + return lean_mk_io_error_invalid_argument_file(fname, errnum, details); + } + case UV_ENOENT: + lean_assert(fname != nullptr); + inc_ref(fname); + return lean_mk_io_error_no_file_or_directory(fname, errnum, details); + case UV_EACCES: case UV_EROFS: case UV_ECONNABORTED: case UV_EFBIG: + case UV_EPERM: + if (fname == nullptr) { + return lean_mk_io_error_permission_denied(errnum, details); + } else { + inc_ref(fname); + return lean_mk_io_error_permission_denied_file(fname, errnum, details); + } + /* LibUV does not map ENOLCK and ENOSR as of version 1.48.0 */ + case UV_EMFILE: case UV_ENFILE: case UV_ENOSPC: + case UV_E2BIG: case UV_EAGAIN: case UV_EMLINK: + case UV_EMSGSIZE: case UV_ENOBUFS: + case UV_ENOMEM: + if (fname == nullptr) { + return lean_mk_io_error_resource_exhausted(errnum, details); + } else { + inc_ref(fname); + return lean_mk_io_error_resource_exhausted_file(fname, errnum, details); + } + /* LibUV does not map EBADMSG as of version 1.48.0 */ + case UV_EISDIR: case UV_ENOTDIR: + if (fname == nullptr) { + return lean_mk_io_error_inappropriate_type(errnum, details); + } else { + inc_ref(fname); + return lean_mk_io_error_inappropriate_type_file(fname, errnum, details); + } + /* LibUV does not map ECHILD as of version 1.48.0 */ + case UV_ENXIO: case UV_EHOSTUNREACH: case UV_ENETUNREACH: + case UV_ECONNREFUSED: +#if UV_VERSION_HEX >= 0x014500 + case UV_ENODATA: +#endif + case UV_ESRCH: + if (fname == nullptr) { + return lean_mk_io_error_no_such_thing(errnum, details); + } else { + inc_ref(fname); + return lean_mk_io_error_no_such_thing_file(fname, errnum, details); + } + /* LibUV does not map EINPROGRESS as of version 1.48.0 */ + case UV_EEXIST: case UV_EISCONN: + if (fname == nullptr) { + return lean_mk_io_error_already_exists(errnum, details); + } else { + inc_ref(fname); + return lean_mk_io_error_already_exists_file(fname, errnum, details); + } + case UV_EIO: + lean_assert(fname == nullptr); + return lean_mk_io_error_hardware_fault(errnum, details); + case UV_ENOTEMPTY: + lean_assert(fname == nullptr); + return lean_mk_io_error_unsatisfied_constraints(errnum, details); + case UV_ENOTTY: + lean_assert(fname == nullptr); + return lean_mk_io_error_illegal_operation(errnum, details); + /* LibUV does not map EIDRM, ENETRESET and ENOLINK as of version 1.48.0 */ + case UV_ECONNRESET: case UV_ENETDOWN: + case UV_EPIPE: + lean_assert(fname == nullptr); + return lean_mk_io_error_resource_vanished(errnum, details); + case UV_EPROTO: case UV_EPROTONOSUPPORT: case UV_EPROTOTYPE: + lean_assert(fname == nullptr); + return lean_mk_io_error_protocol_error(errnum, details); + /* LibUV does not map ETIME as of version 1.48.0 */ + case UV_ETIMEDOUT: + lean_assert(fname == nullptr); + return lean_mk_io_error_time_expired(errnum, details); + /* LibUV does not map EDEADLK as of version 1.48.0 */ + case UV_EADDRINUSE: case UV_EBUSY: case UV_ETXTBSY: + lean_assert(fname == nullptr); + return lean_mk_io_error_resource_busy(errnum, details); + case UV_EADDRNOTAVAIL: case UV_EAFNOSUPPORT: case UV_ENODEV: + case UV_ENOPROTOOPT: case UV_ENOSYS: case UV_ENOTSUP: + case UV_ERANGE: case UV_ESPIPE: case UV_EXDEV: + lean_assert(fname == nullptr); + return lean_mk_io_error_unsupported_operation(errnum, details); + case UV_EFAULT: + default: + lean_assert(fname == nullptr); + return lean_mk_io_error_other_error(errnum, details); + } +} + /* IO.setAccessRights (filename : @& String) (mode : UInt32) : IO Handle */ extern "C" LEAN_EXPORT obj_res lean_chmod (b_obj_arg filename, uint32_t mode, obj_arg /* w */) { if (!chmod(lean_string_cstr(filename), mode)) { @@ -831,50 +940,42 @@ extern "C" LEAN_EXPORT obj_res lean_io_rename(b_obj_arg from, b_obj_arg to, lean /* createTempFile : IO (Handle × FilePath) */ extern "C" LEAN_EXPORT obj_res lean_io_create_tempfile(lean_object * /* w */) { char path[PATH_MAX]; - const char* file_pattern = "tmp.XXXXXXXX"; - const int file_pattern_size = strlen(file_pattern); + size_t base_len = PATH_MAX; + int ret = uv_os_tmpdir(path, &base_len); + if (ret < 0) { + return io_result_mk_error(decode_uv_error(ret, nullptr)); + } else if (base_len == 0) { + return lean_io_result_mk_error(decode_uv_error(UV_ENOENT, mk_string(""))); + } + #if defined(LEAN_WINDOWS) + // On Windows `GetTempPathW` always returns a path ending in \, but libuv removes it. // https://learn.microsoft.com/en-us/windows/win32/fileio/creating-and-using-a-temporary-file - DWORD retval = GetTempPath(MAX_PATH, path); - if (retval > MAX_PATH || (retval == 0)) { - return io_result_mk_error((sstream() << GetLastError()).str()); + if (path[base_len - 1] != '\\') { + lean_always_assert(PATH_MAX >= base_len + 1 + 1); + strcat(path, "\\"); } - // On Windows we have a guarantee that GetTempPath ends on a \. - // If the temp dir is so long that we can't put files into it something is seriously wrong. - lean_always_assert(PATH_MAX >= strlen(path) + file_pattern_size + 1); - strcat(path, file_pattern); #else - char* tmpdir = getenv("TMPDIR"); - if (tmpdir == NULL) { - const char* path_template = "/tmp/tmp.XXXXXXXX"; - strcpy(path, path_template); - } else { - strcpy(path, tmpdir); - int base_len = strlen(path); - if (base_len == 0) { - lean_io_result_mk_error(lean_decode_io_error(ENOENT, mk_string(""))); - } - // No guarantee that we have a trailing / in TMPDIR. - if (path[base_len - 1] != '/') { - // If the temp dir is so long that we can't put files into it something is seriously wrong. - lean_always_assert(PATH_MAX >= strlen(path) + 1 + file_pattern_size + 1); - strcat(path, "/"); - strcat(path, file_pattern); - } else { - // If the temp dir is so long that we can't put files into it something is seriously wrong. - lean_always_assert(PATH_MAX >= strlen(path) + file_pattern_size + 1); - strcat(path, file_pattern); - } + // No guarantee that we have a trailing / in TMPDIR. + if (path[base_len - 1] != '/') { + lean_always_assert(PATH_MAX >= base_len + 1 + 1); + strcat(path, "/"); } #endif - int fd = mkstemp(path); - if (fd == -1) { + const char* file_pattern = "tmp.XXXXXXXX"; + const size_t file_pattern_size = strlen(file_pattern); + lean_always_assert(PATH_MAX >= strlen(path) + file_pattern_size + 1); + strcat(path, file_pattern); + + uv_fs_t req; + ret = uv_fs_mkstemp(NULL, &req, path, NULL); + if (ret < 0) { // If mkstemp throws an error we cannot rely on path to contain a proper file name. - return io_result_mk_error(decode_io_error(errno, nullptr)); + return io_result_mk_error(decode_uv_error(ret, nullptr)); } else { - FILE* handle = fdopen(fd, "r+"); - object_ref pair = mk_cnstr(0, io_wrap_handle(handle), mk_string(path)); + FILE* handle = fdopen(req.result, "r+"); + object_ref pair = mk_cnstr(0, io_wrap_handle(handle), mk_string(req.path)); return lean_io_result_mk_ok(pair.steal()); } } diff --git a/src/runtime/io.h b/src/runtime/io.h index 783f2fc08bbd..ee45c6d86fd5 100644 --- a/src/runtime/io.h +++ b/src/runtime/io.h @@ -15,6 +15,7 @@ inline lean_obj_res io_result_mk_error(lean_obj_arg e) { return lean_io_result_m LEAN_EXPORT lean_obj_res io_result_mk_error(char const * msg); LEAN_EXPORT lean_obj_res io_result_mk_error(std::string const & msg); inline lean_obj_res decode_io_error(int errnum, b_lean_obj_arg fname) { return lean_decode_io_error(errnum, fname); } +inline lean_obj_res decode_uv_error(int errnum, b_lean_obj_arg fname) { return lean_decode_uv_error(errnum, fname); } LEAN_EXPORT lean_obj_res io_wrap_handle(FILE * hfile); void initialize_io(); void finalize_io();