From 88f3de7a44f58a003cd279e9574e6579e1593f7a Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 18 Aug 2021 09:30:59 +0200
Subject: [PATCH] chore: link leanshared using leanc after all

---
 nix/bootstrap.nix  | 4 ++--
 src/bin/leanc.in   | 4 ++--
 src/stdlib.make.in | 3 +--
 3 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix
index 91b0b968e7..e7ea4084be 100644
--- a/nix/bootstrap.nix
+++ b/nix/bootstrap.nix
@@ -85,8 +85,8 @@ rec {
       stdlibLinkFlags = "-L${gmp}/lib -L${Init.staticLib} -L${Std.staticLib} -L${Lean.staticLib} -L${leancpp}/lib/lean";
       leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; } ''
         mkdir $out
-        c++ -fPIC -shared ${lib.optionalString stdenv.isLinux "-Bsymbolic-functions"} \
-          ${if stdenv.isDarwin then "-Wl,-force_load,${Init.staticLib}/* -Wl,-force_load,${Std.staticLib}/* -Wl,-force_load,${Lean.staticLib}/* -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a -Wl,-force_load,${leancpp}/lib/libleanrt_initial-exec.a"
+        LEAN_CXX=${stdenv.cc}/bin/c++ ${lean-bin-tools-unwrapped}/bin/leanc -x none -shared ${lib.optionalString stdenv.isLinux "-Bsymbolic-functions"} \
+          ${if stdenv.isDarwin then "-Wl,-force_load,${Init.staticLib}/* -Wl,-force_load,${Std.staticLib}/* -Wl,-force_load,${Lean.staticLib}/* -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a"
             else "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive"} ${stdlibLinkFlags} \
           -o $out/libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}
       '';
diff --git a/src/bin/leanc.in b/src/bin/leanc.in
index ed51f1b4ff..a3f2df9dcb 100755
--- a/src/bin/leanc.in
+++ b/src/bin/leanc.in
@@ -23,8 +23,8 @@ args=("$@")
 for arg in "$@"; do
     # passed -shared ~> switch to shared linker flags
     [[ $arg == "-shared" ]] && ldflags_ext=(@LEANC_SHARED_LINKER_FLAGS@) && args=("-x" "c" "$@" "-x" "none")
-    # linking against libleanshared explicitly ~> do not link against static stdlib
-    [[ $arg == "-lleanshared" ]] && ldflags_ext=()
+    # linking against libleanshared explicitly (or linking libleanshared itself) ~> do not link against static stdlib
+    [[ $arg == "-lleanshared" || $arg == *libleanshared.* ]] && ldflags_ext=()
     # Note the `-x c` for treating all input as C code
     [[ $arg == "-c" ]] && ldflags=() && ldflags_ext=() && args=("-x" "c" "$@" "-x" "none")
     [[ $arg == "--print-cflags" ]] && echo "${cflags[@]}" && exit
diff --git a/src/stdlib.make.in b/src/stdlib.make.in
index 4b4e36fc9b..8ff577b5ad 100644
--- a/src/stdlib.make.in
+++ b/src/stdlib.make.in
@@ -33,8 +33,7 @@ Lean: Init Std
 
 leanshared: Init Std Lean
 	@mkdir -p "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}" || true
-# can't use leanc here since it would try to link against leanshared
-	${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} -shared -o "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}" ${LEANSHARED_LINKER_FLAGS} -lgmp ${LEANC_EXTRA_FLAGS} -L${LIB}/lean
+	"${LEAN_BIN}/leanc" -x none -shared -o "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}" ${LEANSHARED_LINKER_FLAGS} ${LEANC_OPTS}
 
 Leanpkg: Init Std Lean leanshared
 	+"${LEAN_BIN}/leanmake" bin PKG=Leanpkg BIN_NAME=leanpkg${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='-lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE}'