From 160ca476a1f369c8f937bc1c4c44d2e63c8da213 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Thu, 20 Mar 2025 02:27:22 -0400
Subject: [PATCH] chore: `USE_LAKE` touchups (#7581)

This PR adds some documentation to the Lean's `lakefile.toml` and makes
a few tweaks required to get `USE_LAKE` working properly on Windows. It
also adds a `stage1-configure` step target so the Lake configuration
files can be generated without performing a build of stage 1. This
enables one to build stage 0 and configure Lake via CMake and then use
Lake instead of CMake to build stage 1.

Partly adapted from #7505.
---
 CMakeLists.txt       |  1 +
 src/CMakeLists.txt   |  4 ++++
 src/lakefile.toml.in | 20 +++++++++++++++-----
 src/stdlib.make.in   |  6 +++++-
 4 files changed, 25 insertions(+), 6 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 8336745315..03723e9284 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -83,6 +83,7 @@ ExternalProject_add(stage1
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS stage0
+  STEP_TARGETS configure
 )
 ExternalProject_add(stage2
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 98b8c47a0c..1cc0e7a2cb 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -815,6 +815,10 @@ toml_escape("${LEAN_EXTRA_MAKE_OPTS}" LEAN_EXTRA_OPTS_TOML)
 toml_escape("${LEANC_OPTS_TOML}" LEANC_OPTS_TOML)
 toml_escape("${LINK_OPTS_TOML}" LINK_OPTS_TOML)
 
+if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+  set(LAKE_LIB_PREFIX "lib")
+endif()
+
 if(USE_LAKE AND STAGE EQUAL 1)
   configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/lakefile.toml)
   configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/../tests/lakefile.toml)
diff --git a/src/lakefile.toml.in b/src/lakefile.toml.in
index 5e694b3747..8aed37f200 100644
--- a/src/lakefile.toml.in
+++ b/src/lakefile.toml.in
@@ -7,7 +7,7 @@
 
 name = "lean4"
 
-defaultTargets = ["Init", "Lean", "Lake"]
+defaultTargets = ["Init", "Std", "Lean", "Lake", "LakeMain"]
 
 # The root of all the compiler output directories
 buildDir = "${CMAKE_BINARY_DIR}"
@@ -24,20 +24,24 @@ leanLibDir = "lib/lean"
 # Destination for static libraries
 nativeLibDir = "lib/lean"
 
+# Toolchain CLI options derived from the CMake configuration
 moreLeanArgs = [${LEAN_EXTRA_OPTS_TOML}]
 moreLeancArgs = [${LEANC_OPTS_TOML}]
 moreLinkArgs = [${LINK_OPTS_TOML}]
 
 [[lean_lib]]
 name = "Init"
+libName = "${LAKE_LIB_PREFIX}Init"
 defaultFacets = ["static", "static.export"]
 
 [[lean_lib]]
 name = "Std"
+libName = "${LAKE_LIB_PREFIX}Std"
 defaultFacets = ["static", "static.export"]
 
 [[lean_lib]]
 name = "Lean"
+libName = "${LAKE_LIB_PREFIX}Lean"
 defaultFacets = ["static", "static.export"]
 globs = [
   # Library root
@@ -51,12 +55,18 @@ globs = [
 [[lean_lib]]
 name = "Lake"
 srcDir = "lake"
-moreLeanArgs = ["--plugin=${PREV_STAGE}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}"]
+globs = [
+  # Lake API imported by configuration files
+  "Lake",
+  # API only imported by `LakeMain` and the `lake` CLI
+  "Lake.CLI",
+]
+libName = "${LAKE_LIB_PREFIX}Lake"
 defaultFacets = ["static", "static.export"]
-globs = ["Lake", "Lake.CLI"]
-moreLeanArgs = ["--plugin=${LAKE_PREV_PLUGIN}"]
+moreLeanArgs = ["--plugin=${PREV_STAGE}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}"]
 
 [[lean_lib]]
 name = "LakeMain"
 srcDir = "lake"
-defaultFacets = ["static"]
+libName = "${LAKE_LIB_PREFIX}LakeMain"
+defaultFacets = ["static.export"]
diff --git a/src/stdlib.make.in b/src/stdlib.make.in
index 0cb13b18a0..92fb020125 100644
--- a/src/stdlib.make.in
+++ b/src/stdlib.make.in
@@ -6,7 +6,11 @@ SHELL := $(LEAN_BASH) -eo pipefail
 
 # any absolute path to the stdlib breaks the Makefile
 export LEAN_PATH=
-export LEAN_CC=${CMAKE_C_COMPILER_LAUNCHER} ${CMAKE_C_COMPILER}
+ifeq "${USE_LAKE} ${STAGE}" "ON 1"
+  export LEAN_CC=${CMAKE_C_COMPILER}
+else
+  export LEAN_CC=${CMAKE_C_COMPILER_LAUNCHER} ${CMAKE_C_COMPILER}
+endif
 export LEAN_ABORT_ON_PANIC=1
 
 # LEAN_OPTS: don't use native code (except for primitives) since it is from the previous stage