From d991f5efe0217ecadbe77a020a1516778fe32547 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 19 Jul 2023 13:03:21 +0200
Subject: [PATCH] fix: ship libLake.a

---
 nix/bootstrap.nix                          | 2 +-
 src/CMakeLists.txt                         | 1 +
 src/stdlib.make.in                         | 2 +-
 tests/compiler/link_lake.lean              | 5 +++++
 tests/compiler/link_lake.lean.expected.out | 0
 5 files changed, 8 insertions(+), 2 deletions(-)
 create mode 100644 tests/compiler/link_lake.lean
 create mode 100644 tests/compiler/link_lake.lean.expected.out

diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix
index 0581acad40..f43678e24b 100644
--- a/nix/bootstrap.nix
+++ b/nix/bootstrap.nix
@@ -119,7 +119,7 @@ rec {
       depRoots = symlinkJoin { name = "depRoots"; paths = map (l: l.depRoots) stdlib; };
       iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
       Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
-      stdlibLinkFlags = "-L${Init.staticLib} -L${Lean.staticLib} -L${leancpp}/lib/lean";
+      stdlibLinkFlags = "-L${Init.staticLib} -L${Lean.staticLib} -L${Lake.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 "-Wl,-Bsymbolic"} \
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 3ceb103c83..403e447dcd 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -301,6 +301,7 @@ elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
 else()
   string(APPEND LEANC_STATIC_LINKER_FLAGS " -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lleanrt -Wl,--end-group")
 endif()
+string(APPEND LEANC_STATIC_LINKER_FLAGS " -lLake")
 
 set(LEAN_CXX_STDLIB "-lstdc++" CACHE STRING "C++ stdlib linker flags")
 
diff --git a/src/stdlib.make.in b/src/stdlib.make.in
index 53a75888fd..92383e8a8b 100644
--- a/src/stdlib.make.in
+++ b/src/stdlib.make.in
@@ -45,7 +45,7 @@ leanshared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRAR
 
 Lake:
 # must put lake in its own directory because of submodule, so must adjust relative paths...
-	+"${LEAN_BIN}/leanmake" -C lake bin PKG=Lake BIN_NAME=lake${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='-lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="../${LIB}" LIB_OUT="../${LIB}/lean" OLEAN_OUT="../${LIB}/lean"
+	+"${LEAN_BIN}/leanmake" -C lake bin lib PKG=Lake BIN_NAME=lake${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='-lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="../${LIB}" LIB_OUT="../${LIB}/lean" OLEAN_OUT="../${LIB}/lean"
 
 ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} $(LEAN_SHELL)
 	@echo "[    ] Building $@"
diff --git a/tests/compiler/link_lake.lean b/tests/compiler/link_lake.lean
new file mode 100644
index 0000000000..66000bd2ac
--- /dev/null
+++ b/tests/compiler/link_lake.lean
@@ -0,0 +1,5 @@
+-- this should be sufficient to trigger linking against Lake's initializer symbols
+import Lake
+
+def main : IO Unit :=
+  return
diff --git a/tests/compiler/link_lake.lean.expected.out b/tests/compiler/link_lake.lean.expected.out
new file mode 100644
index 0000000000..e69de29bb2