feat: link LibUV (#4963)

2024-08-12 14:33:24 +02:00 · 2024-08-12 14:33:24 +02:00 · c237c1f9fb
commit c237c1f9fb
parent dd4e26f247
18 changed files with 100 additions and 25 deletions
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@ -226,21 +226,19 @@ jobs:
              },
              {
                "name": "Linux aarch64",
-                "os": "ubuntu-latest",
+                "os": "nscloud-ubuntu-22.04-arm64-4x8",
                "CMAKE_OPTIONS": "-DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-linux_aarch64",
                "release": true,
                "check-level": 2,
-                "cross": true,
-                "cross_target": "aarch64-unknown-linux-gnu",
                "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst",
-                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm-aarch64-* lean-llvm-x86_64-*"
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst",
+                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*"
              },
              {
                "name": "Linux 32bit",
                "os": "ubuntu-latest",
                // Use 32bit on stage0 and stage1 to keep oleans compatible
-                "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86",
+                "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/",
                "cmultilib": true,
                "release": true,
                "check-level": 2,
@ -259,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\""
+                "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean|leanruntest_libuv\\.lean\""
              }
            ];
            console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`)
@ -299,11 +297,11 @@ jobs:
        with:
          msystem: clang64
          # `:` means do not prefix with msystem
-          pacboy: "make: python: cmake clang ccache gmp git: zip: unzip: diffutils: binutils: tree: zstd tar:"
+          pacboy: "make: python: cmake clang ccache gmp libuv git: zip: unzip: diffutils: binutils: tree: zstd tar:"
        if: runner.os == 'Windows'
      - name: Install Brew Packages
        run: |
-          brew install ccache tree zstd coreutils gmp
+          brew install ccache tree zstd coreutils gmp libuv
        if: runner.os == 'macOS'
      - name: Checkout
        uses: actions/checkout@v4
@ -327,8 +325,9 @@ jobs:
        if: matrix.wasm
      - name: Install 32bit c libs
        run: |
+          sudo dpkg --add-architecture i386
          sudo apt-get update
-          sudo apt-get install -y gcc-multilib g++-multilib ccache
+          sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386
        if: matrix.cmultilib
      - name: Cache
        uses: actions/cache@v3
--- a/doc/make/index.md
+++ b/doc/make/index.md
@ -8,6 +8,7 @@ Requirements
 - C++14 compatible compiler
 - [CMake](http://www.cmake.org)
 - [GMP (GNU multiprecision library)](http://gmplib.org/)
+- [LibUV](https://libuv.org/)

 Platform-Specific Setup
 -----------------------
--- a/doc/make/msys2.md
+++ b/doc/make/msys2.md
@ -25,7 +25,7 @@ MSYS2 has a package management system, [pacman][pacman], which is used in Arch L
 Here are the commands to install all dependencies needed to compile Lean on your machine.

 ```bash
-pacman -S make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-ccache git unzip diffutils binutils
+pacman -S make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-ccache mingw-w64-x86_64-libuv mingw-w64-x86_64-gmp git unzip diffutils binutils
 ```

 You should now be able to run these commands:
@ -64,6 +64,7 @@ they are installed in your MSYS setup:
 - libgcc_s_seh-1.dll
 - libstdc++-6.dll
 - libgmp-10.dll
+- libuv-1.dll
 - libwinpthread-1.dll

 The following linux command will do that:
--- a/doc/make/osx-10.9.md
+++ b/doc/make/osx-10.9.md
@ -37,10 +37,11 @@ cmake -DCMAKE_CXX_COMPILER=g++ ...
 ```bash
 brew install cmake
 brew install gmp
+brew install libuv
 ```

 ## Recommended Packages: CCache

 ```bash
 brew install ccache
-```
+```
--- a/doc/make/ubuntu.md
+++ b/doc/make/ubuntu.md
@ -8,5 +8,5 @@ follow the [generic build instructions](index.md).
 ## Basic packages

 ```bash
-sudo apt-get install git libgmp-dev cmake ccache clang
+sudo apt-get install git libgmp-dev libuv1-dev cmake ccache clang
 ```
--- a/flake.nix
+++ b/flake.nix
@ -21,7 +21,7 @@
          stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
        } ({
          buildInputs = with pkgs; [
-            cmake gmp ccache
+            cmake gmp libuv ccache
            lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
            gdb
            # TODO: only add when proven to not affect the flakification
@ -34,6 +34,7 @@
          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"]; });
          GLIBC = pkgsDist.glibc;
          GLIBC_DEV = pkgsDist.glibc.dev;
          GCC_LIB = pkgsDist.gcc.cc.lib;
--- a/nix/bootstrap.nix
+++ b/nix/bootstrap.nix
@ -1,5 +1,5 @@
 { src, debug ? false, stage0debug ? false, extraCMakeFlags ? [],
-  stdenv, lib, cmake, gmp, git, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
+  stdenv, lib, cmake, gmp, libuv, git, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
  ... } @ args:
 with builtins;
 lib.warn "The Nix-based build is deprecated" rec {
@ -7,7 +7,7 @@ lib.warn "The Nix-based build is deprecated" rec {
  sourceByRegex = p: rs: lib.sourceByRegex p (map (r: "(/src/)?${r}") rs);
  buildCMake = args: stdenv.mkDerivation ({
    nativeBuildInputs = [ cmake ];
-    buildInputs = [ gmp llvmPackages.llvm ];
+    buildInputs = [ gmp libuv llvmPackages.llvm ];
    # https://github.com/NixOS/nixpkgs/issues/60919
    hardeningDisable = [ "all" ];
    dontStrip = (args.debug or debug);
@ -158,7 +158,7 @@ lib.warn "The Nix-based build is deprecated" rec {
      test = buildCMake {
        name = "lean-test-${desc}";
        realSrc = lib.sourceByRegex src [ "src.*" "tests.*" ];
-        buildInputs = [ gmp perl git ];
+        buildInputs = [ gmp libuv perl git ];
        preConfigure = ''
          cd src
        '';
--- a/script/prepare-llvm-linux.sh
+++ b/script/prepare-llvm-linux.sh
@ -38,7 +38,7 @@ $CP $GLIBC/lib/*crt* llvm/lib/
 $CP $GLIBC/lib/*crt* stage1/lib/
 # runtime
 (cd llvm; $CP --parents lib/clang/*/lib/*/{clang_rt.*.o,libclang_rt.builtins*} ../stage1)
-$CP llvm/lib/*/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.a stage1/lib/
+$CP llvm/lib/*/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.a $LIBUV/lib/libuv.a stage1/lib/
 # LLVM 15 appears to ship the dependencies in 'llvm/lib/<target-triple>/' and 'llvm/include/<target-triple>/'
 # but clang-15 that we use to compile is linked against 'llvm/lib/' and 'llvm/include'
 # https://github.com/llvm/llvm-project/issues/54955
@ -62,8 +62,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 -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 -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -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 -Wl,--no-as-needed'"
+echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -Wl,--no-as-needed'"
 # do not set `LEAN_CC` for tests
 echo -n " -DLEAN_TEST_VARS=''"
--- a/script/prepare-llvm-macos.sh
+++ b/script/prepare-llvm-macos.sh
@ -9,6 +9,7 @@ set -uxo pipefail
 # use full LLVM release for compiling C++ code, but subset for compiling C code and distribution

 GMP=${GMP:-$(brew --prefix)}
+LIBUV=${LIBUV:-$(brew --prefix)}

 [[ -d llvm ]] || (mkdir llvm; gtar xf $1 --strip-components 1 --directory llvm)
 [[ -d llvm-host ]] || if [[ "$#" -gt 1 ]]; then
@ -46,8 +47,9 @@ echo -n " -DLEAN_EXTRA_CXX_FLAGS='${EXTRA_FLAGS:-}'"
 if [[ -L llvm-host ]]; then
  echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"
  gcp $GMP/lib/libgmp.a stage1/lib/
+  gcp $LIBUV/lib/libuv.a stage1/lib/
  echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/libc -fuse-ld=lld'"
-  echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp'"
+  echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv'"
 else
  echo -n " -DCMAKE_C_COMPILER=$PWD/llvm-host/bin/clang -DLEANC_OPTS='--sysroot $PWD/stage1 -resource-dir $PWD/stage1/lib/clang/15.0.1 ${EXTRA_FLAGS:-}'"
  echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/libc -fuse-ld=lld'"
--- 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 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}.* /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 -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -static-libgcc -Wl,-Bstatic -lgmp -luv -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
 # when not using the above flags, link GMP dynamically/as usual
-echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -lucrtbase'"
+echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv -lucrtbase'"
 # do not set `LEAN_CC` for tests
 echo -n " -DAUTO_THREAD_FINALIZATION=OFF -DSTAGE0_AUTO_THREAD_FINALIZATION=OFF"
 echo -n " -DLEAN_TEST_VARS=''"
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@ -243,6 +243,15 @@ if("${USE_GMP}" MATCHES "ON")
  endif()
 endif()

+if(NOT "${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
+  # LibUV
+  find_package(LibUV 1.0.0 REQUIRED)
+  include_directories(${LIBUV_INCLUDE_DIR})
+endif()
+if(NOT LEAN_STANDALONE)
+  string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${LIBUV_LIBRARIES}")
+endif()
+
 # ccache
 if(CCACHE AND NOT CMAKE_CXX_COMPILER_LAUNCHER AND NOT CMAKE_C_COMPILER_LAUNCHER)
  find_program(CCACHE_PATH ccache)
--- a/src/Lean/Runtime.lean
+++ b/src/Lean/Runtime.lean
@ -14,10 +14,16 @@ opaque closureMaxArgsFn : Unit → Nat
@[extern "lean_max_small_nat"]
 opaque maxSmallNatFn : Unit → Nat

+@[extern "lean_libuv_version"]
+opaque libUVVersionFn : Unit → Nat
+
 def closureMaxArgs : Nat :=
  closureMaxArgsFn ()

 def maxSmallNat : Nat :=
  maxSmallNatFn ()

+def libUVVersion : Nat :=
+  libUVVersionFn ()
+
 end Lean
--- a/src/cmake/Modules/FindLibUV.cmake
+++ b/src/cmake/Modules/FindLibUV.cmake
@ -0,0 +1,12 @@
+if (LIBUV_INCLUDE_DIR AND LIBUV_LIBRARIES)
+  # Already in cache, be silent
+  set(LIBUV_FIND_QUIETLY TRUE)
+endif (LIBUV_INCLUDE_DIR AND LIBUV_LIBRARIES)
+
+find_path(LIBUV_INCLUDE_DIR NAMES uv.h)
+find_library(LIBUV_LIBRARIES NAMES uv REQUIRED)
+MESSAGE(STATUS "LIBUV: " ${LIBUV_LIBRARIES})
+
+include(FindPackageHandleStandardArgs)
+FIND_PACKAGE_HANDLE_STANDARD_ARGS(LibUV DEFAULT_MSG LIBUV_INCLUDE_DIR LIBUV_LIBRARIES)
+mark_as_advanced(LIBUV_INCLUDE_DIR LIBUV_LIBRARIES)
--- a/src/include/lean/lean_libuv.h
+++ b/src/include/lean/lean_libuv.h
--- a/src/runtime/CMakeLists.txt
+++ b/src/runtime/CMakeLists.txt
@ -2,7 +2,7 @@ set(RUNTIME_OBJS debug.cpp thread.cpp mpz.cpp utf8.cpp
 object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
 stackinfo.cpp compact.cpp init_module.cpp load_dynlib.cpp io.cpp hash.cpp
 platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
-process.cpp object_ref.cpp mpn.cpp mutex.cpp)
+process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp)
 add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})
 set_target_properties(leanrt_initial-exec PROPERTIES
  ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})
--- a/src/runtime/libuv.cpp
+++ b/src/runtime/libuv.cpp
@ -0,0 +1,22 @@
+/*
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Markus Himmel
+*/
+#include "runtime/libuv.h"
+
+#ifndef LEAN_EMSCRIPTEN
+#include <uv.h>
+
+extern "C" LEAN_EXPORT lean_obj_res lean_libuv_version(lean_obj_arg o) {
+    return lean_unsigned_to_nat(uv_version());
+}
+
+#else
+
+extern "C" LEAN_EXPORT lean_obj_res lean_libuv_version(lean_obj_arg o) {
+    return lean_box(0);
+}
+
+#endif
--- a/src/runtime/libuv.h
+++ b/src/runtime/libuv.h
@ -0,0 +1,10 @@
+/*
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Markus Himmel
+*/
+#pragma once
+#include <lean/lean.h>
+
+extern "C" LEAN_EXPORT lean_obj_res lean_libuv_version(lean_obj_arg);
--- a/tests/lean/run/libuv.lean
+++ b/tests/lean/run/libuv.lean
@ -0,0 +1,11 @@
+import Lean.Runtime
+
+-- Non-emscripten build: expect the major version of LibUV
+/-- info: 1 -/
+#guard_msgs in
+#eval if !System.Platform.isEmscripten then Lean.libUVVersion >>> 16 else 1
+
+-- Emscripten build: expect 0
+/-- info: 0 -/
+#guard_msgs in
+#eval if System.Platform.isEmscripten then Lean.libUVVersion >>> 16 else 0