chore: fix USE_GMP=OFF by removing GMP linking customization

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"} \

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

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

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

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

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

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")

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

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 <leodemoura@microsoft.com>")
-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)

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