From 4a9bc88a4e82b554f9efdd8c2e8b2a56133d5178 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 26 Mar 2022 10:01:03 +0100 Subject: [PATCH] chore: fix USE_GMP=OFF by removing GMP linking customization --- nix/bootstrap.nix | 8 ++++---- script/prepare-llvm-macos.sh | 1 - src/CMakeLists.txt | 5 +++-- src/Lean/Compiler/FFI.lean | 4 ++-- src/Leanc.lean | 6 ++---- src/bin/leanc.in | 2 +- src/shell/CMakeLists.txt | 2 +- src/stdlib.make.in | 1 - stage0/src/CMakeLists.txt | 34 ++++++---------------------------- stage0/src/bin/leanc.in | 2 +- 10 files changed, 20 insertions(+), 45 deletions(-) diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index 93745dc947..26c84eff78 100644 --- a/nix/bootstrap.nix +++ b/nix/bootstrap.nix @@ -25,10 +25,10 @@ rec { lean-bin-tools-unwrapped = buildCMake { name = "lean-bin-tools"; outputs = [ "out" "leanc_src" ]; - realSrc = lib.sourceByRegex ../src [ "CMakeLists\.txt" "bin.*" "include.*" ".*\.in" "Leanc\.lean" ]; + realSrc = lib.sourceByRegex ../src [ "CMakeLists\.txt" "cmake.*" "bin.*" "include.*" ".*\.in" "Leanc\.lean" ]; preConfigure = '' touch empty.cpp - sed -i 's/find_package.*//;s/add_subdirectory.*//;s/set(LEAN_OBJS.*/set(LEAN_OBJS empty.cpp)/' CMakeLists.txt + sed -i 's/add_subdirectory.*//;s/set(LEAN_OBJS.*/set(LEAN_OBJS empty.cpp)/' CMakeLists.txt ''; dontBuild = true; installPhase = '' @@ -105,8 +105,8 @@ rec { stdlib = [ Init Std Lean ]; iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; }; extlib = stdlib; # TODO: add Lake - Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; linkFlags = ["-L${gmp}/lib -L${leanshared}"]; }; - stdlibLinkFlags = "-L${gmp}/lib -L${Init.staticLib} -L${Std.staticLib} -L${Lean.staticLib} -L${leancpp}/lib/lean"; + Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; linkFlags = ["-L${leanshared}"]; }; + stdlibLinkFlags = "-L${Init.staticLib} -L${Std.staticLib} -L${Lean.staticLib} -L${leancpp}/lib/lean"; leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } '' mkdir $out LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Bsymbolic"} \ diff --git a/script/prepare-llvm-macos.sh b/script/prepare-llvm-macos.sh index 050d2564fe..d724d8ae9d 100755 --- a/script/prepare-llvm-macos.sh +++ b/script/prepare-llvm-macos.sh @@ -48,7 +48,6 @@ else echo -n " -DCMAKE_C_COMPILER=$PWD/llvm-host/bin/clang -DLEANC_OPTS='--sysroot $PWD/stage1 -resource-dir $PWD/stage1/lib/clang/14.0.0 ${EXTRA_FLAGS:-}'" echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/libc -fuse-ld=lld'" fi -echo -n " -DGMP_LIBRARIES=lib/libgmp.a -DGMP_INCLUDE_DIR=$GMP/include" echo -n " -DLEANC_INTERNAL_FLAGS='-nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang" # do not set `LEAN_CC` for tests echo -n " -DLEAN_TEST_VARS=''" diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 51cdad5b94..e285ddf0da 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -237,8 +237,9 @@ if("${USE_GMP}" MATCHES "ON") # GMP find_package(GMP 5.0.5 REQUIRED) include_directories(${GMP_INCLUDE_DIR}) - # dlopen - set(EXTRA_LIBS ${EXTRA_LIBS} ${CMAKE_DL_LIBS}) + endif() + if(NOT LEAN_STANDALONE) + string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${GMP_LIBRARIES}") endif() endif() diff --git a/src/Lean/Compiler/FFI.lean b/src/Lean/Compiler/FFI.lean index d1f4bc5255..a74815ffda 100644 --- a/src/Lean/Compiler/FFI.lean +++ b/src/Lean/Compiler/FFI.lean @@ -19,7 +19,7 @@ def getCFlags (leanSysroot : FilePath) : Array String := private constant getBuiltinLinkerFlags (linkStatic : Bool) : String /-- Return linker flags for linking against Lean's libraries. -/ -def getLinkerFlags (leanSysroot : FilePath) (linkStatic := true) (gmp := "-lgmp") : Array String := - #["-L", (leanSysroot / "lib" / "lean").toString] ++ (getBuiltinLinkerFlags linkStatic).trim.splitOn ++ [gmp] +def getLinkerFlags (leanSysroot : FilePath) (linkStatic := true) : Array String := + #["-L", (leanSysroot / "lib" / "lean").toString] ++ (getBuiltinLinkerFlags linkStatic).trim.splitOn end Lean.Compiler.FFI diff --git a/src/Leanc.lean b/src/Leanc.lean index 976d764dee..365a933e19 100644 --- a/src/Leanc.lean +++ b/src/Leanc.lean @@ -12,9 +12,7 @@ as-is to the wrapped compiler. Interesting options: * `--print-cflags`: print C compiler flags necessary for building against the Lean runtime and exit -* `--print-ldlags`: print C compiler flags necessary for statically linking against the Lean library and exit -* Set the `LEANC_GMP` environment variable to a path to `libgmp.a` (or `-l:libgmp.a` on Linux) to link GMP statically. -Beware of the licensing consequences since GMP is LGPL." +* `--print-ldlags`: print C compiler flags necessary for statically linking against the Lean library and exit" return 1 let root ← match (← IO.getEnv "LEAN_SYSROOT") with @@ -29,7 +27,7 @@ Beware of the licensing consequences since GMP is LGPL." let cflags := getCFlags root let mut cflagsInternal := "@LEANC_INTERNAL_FLAGS@".trim.splitOn let mut ldflagsInternal := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn - let ldflags := getLinkerFlags root linkStatic ((← IO.getEnv "LEANC_GMP").getD "-lgmp") + let ldflags := getLinkerFlags root linkStatic for arg in args do match arg with diff --git a/src/bin/leanc.in b/src/bin/leanc.in index 60ae824f77..11fe5cdbf6 100755 --- a/src/bin/leanc.in +++ b/src/bin/leanc.in @@ -1,7 +1,7 @@ #!/usr/bin/env bash # used only for building Lean itself root=$(dirname $0) -ldflags=(@LEANC_INTERNAL_LINKER_FLAGS@ "-L$root/lib/lean" "${LEANC_GMP:--lgmp}" @LEAN_EXTRA_LINKER_FLAGS@) +ldflags=(@LEANC_INTERNAL_LINKER_FLAGS@ "-L$root/lib/lean" @LEAN_EXTRA_LINKER_FLAGS@) for arg in "$@"; do # ccache doesn't like linker flags being passed here [[ "$arg" = "-c" ]] && ldflags=() diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index b9b815ff77..d570dd7950 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -93,7 +93,7 @@ ENDFOREACH(T) add_test(NAME leancomptest_foreign WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler/foreign" - COMMAND bash -c "LEANC_GMP=${GMP_LIBRARIES} ${LEAN_BIN}/leanmake --always-make") + COMMAND bash -c "${LEAN_BIN}/leanmake --always-make") add_test(NAME leancomptest_doc_example WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples/compiler" COMMAND bash -c "export ${TEST_VARS}; leanmake --always-make bin && ./build/bin/test hello world") diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 72f0278e7a..841ad8695c 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -3,7 +3,6 @@ SHELL := /usr/bin/env bash -euo pipefail # any absolute path to the stdlib breaks the Makefile export LEAN_PATH= export LEAN_CC=${CMAKE_C_COMPILER_LAUNCHER} ${CMAKE_C_COMPILER} -export LEANC_GMP=${GMP_LIBRARIES} # LEAN_OPTS: don't use native code (except for primitives) since it is from the previous stage # MORE_DEPS: rebuild the stdlib whenever the compiler has changed diff --git a/stage0/src/CMakeLists.txt b/stage0/src/CMakeLists.txt index 2437fc711a..e285ddf0da 100644 --- a/stage0/src/CMakeLists.txt +++ b/stage0/src/CMakeLists.txt @@ -237,8 +237,9 @@ if("${USE_GMP}" MATCHES "ON") # GMP find_package(GMP 5.0.5 REQUIRED) include_directories(${GMP_INCLUDE_DIR}) - # dlopen - set(EXTRA_LIBS ${EXTRA_LIBS} ${CMAKE_DL_LIBS}) + endif() + if(NOT LEAN_STANDALONE) + string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${GMP_LIBRARIES}") endif() endif() @@ -535,32 +536,9 @@ endif() file(COPY ${CMAKE_SOURCE_DIR}/include/lean DESTINATION ${CMAKE_BINARY_DIR}/include FILES_MATCHING PATTERN "*.h") -# CPack -set(CPACK_PACKAGE_NAME lean) -set(CPACK_PACKAGE_CONTACT "Leonardo de Moura ") -string(TOLOWER ${CMAKE_SYSTEM_NAME} LOWER_SYSTEM_NAME) -string(TIMESTAMP COMPILE_DATETIME "%Y%m%d%H%M%S") -set(CPACK_PACKAGE_VERSION "${LEAN_VERSION_STRING}.${COMPILE_DATETIME}") -if(NOT (${GIT_SHA1} MATCHES "")) - string(APPEND CPACK_PACKAGE_VERSION ".git${GIT_SHA1}") -endif() -if (${CMAKE_SYSTEM_PROCESSOR} MATCHES "x86_64|AMD64") - # for compatibility with elan/previous releases - set(ARCH_SUFFIX "") -else() - set(ARCH_SUFFIX "_${CMAKE_SYSTEM_PROCESSOR}") -endif() -set(CPACK_PACKAGE_FILE_NAME "lean-${LEAN_VERSION_STRING}-${LOWER_SYSTEM_NAME}${ARCH_SUFFIX}") -if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") - SET(CPACK_GENERATOR TGZ) -else() - SET(CPACK_GENERATOR ZIP) -endif() - set(LEAN_INSTALL_PREFIX "" CACHE STRING "If set, set CMAKE_INSTALL_PREFIX to this value + version name") if(LEAN_INSTALL_PREFIX) - set(CMAKE_INSTALL_PREFIX "${LEAN_INSTALL_PREFIX}/${CPACK_PACKAGE_FILE_NAME}") + string(TOLOWER ${CMAKE_SYSTEM_NAME} LOWER_SYSTEM_NAME) + set(LEAN_INSTALL_SUFFIX "-${LOWER_SYSTEM_NAME}" CACHE STRING "If LEAN_INSTALL_PREFIX is set, append this value to CMAKE_INSTALL_PREFIX") + set(CMAKE_INSTALL_PREFIX "${LEAN_INSTALL_PREFIX}/lean-${LEAN_VERSION_STRING}${LEAN_INSTALL_SUFFIX}") endif() - -# NOTE: modifies `CPACK_PACKAGE_FILE_NAME`(??) -include(CPack) diff --git a/stage0/src/bin/leanc.in b/stage0/src/bin/leanc.in index 60ae824f77..11fe5cdbf6 100755 --- a/stage0/src/bin/leanc.in +++ b/stage0/src/bin/leanc.in @@ -1,7 +1,7 @@ #!/usr/bin/env bash # used only for building Lean itself root=$(dirname $0) -ldflags=(@LEANC_INTERNAL_LINKER_FLAGS@ "-L$root/lib/lean" "${LEANC_GMP:--lgmp}" @LEAN_EXTRA_LINKER_FLAGS@) +ldflags=(@LEANC_INTERNAL_LINKER_FLAGS@ "-L$root/lib/lean" @LEAN_EXTRA_LINKER_FLAGS@) for arg in "$@"; do # ccache doesn't like linker flags being passed here [[ "$arg" = "-c" ]] && ldflags=()