feat: use libuv for tempfiles

.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

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;

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=''"

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=''"

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} $<TARGET_OBJECTS:util>)
@@ -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

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

src/runtime/io.cpp

@@ -39,6 +39,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 #include <cstdlib>
 #include <cctype>
 #include <sys/stat.h>
+#include <uv.h>
 #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());
     }
 }

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