diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 856f89b866..435a3dbfb5 100644 --- 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 diff --git a/doc/make/index.md b/doc/make/index.md index 8772bdb431..1bf663760c 100644 --- 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 ----------------------- diff --git a/doc/make/msys2.md b/doc/make/msys2.md index fa3d28dfde..952db856d7 100644 --- 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: diff --git a/doc/make/osx-10.9.md b/doc/make/osx-10.9.md index 0563aa6bbf..ca63b47230 100644 --- 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 -``` \ No newline at end of file +``` diff --git a/doc/make/ubuntu.md b/doc/make/ubuntu.md index 15a19145f4..abeb1a127f 100644 --- 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 ``` diff --git a/flake.nix b/flake.nix index cceb1de454..3319db4c45 100644 --- 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; diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index 8a4c6db00e..033ee7cd28 100644 --- 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 ''; diff --git a/script/prepare-llvm-linux.sh b/script/prepare-llvm-linux.sh index 429725b82a..40c9889788 100755 --- 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//' and 'llvm/include//' # 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=''" diff --git a/script/prepare-llvm-macos.sh b/script/prepare-llvm-macos.sh index ab81c210ff..d3cdc61b3f 100755 --- 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'" diff --git a/script/prepare-llvm-mingw.sh b/script/prepare-llvm-mingw.sh index b30bcd6488..749fc9d9fa 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 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=''" diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4a503b3590..c8dc6a277d 100644 --- 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) diff --git a/src/Lean/Runtime.lean b/src/Lean/Runtime.lean index 4cac6f1379..f789697858 100644 --- 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 diff --git a/src/cmake/Modules/FindLibUV.cmake b/src/cmake/Modules/FindLibUV.cmake new file mode 100644 index 0000000000..259b08cd93 --- /dev/null +++ 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) diff --git a/src/include/lean/lean_libuv.h b/src/include/lean/lean_libuv.h new file mode 100644 index 0000000000..e69de29bb2 diff --git a/src/runtime/CMakeLists.txt b/src/runtime/CMakeLists.txt index f696108531..367c7c2980 100644 --- 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}) diff --git a/src/runtime/libuv.cpp b/src/runtime/libuv.cpp new file mode 100644 index 0000000000..627eb848d3 --- /dev/null +++ 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 + +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 diff --git a/src/runtime/libuv.h b/src/runtime/libuv.h new file mode 100644 index 0000000000..4c53786a59 --- /dev/null +++ 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 + +extern "C" LEAN_EXPORT lean_obj_res lean_libuv_version(lean_obj_arg); diff --git a/tests/lean/run/libuv.lean b/tests/lean/run/libuv.lean new file mode 100644 index 0000000000..0bad76a4aa --- /dev/null +++ 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