chore: lake: bootstrap Lean include directory (#7967)

This PR adds a `bootstrap` option to Lake which is used to identify the
core Lean package. This enables Lake to use the current stage's include
directory rather than the Lean toolchains when compiling Lean with Lean
in core.

**Breaking change:** The Lean library directory is no longer part of
`getLeanLinkSharedFlags`. FFI users should provide this option
separately when linking to Lean (e.g.. via `s!"-L{(←
getLeanLibDir).toString}"`). See the FFI example for a demonstration.

CMakeLists.txt

@@ -108,6 +108,7 @@ ExternalProject_add(stage2
   INSTALL_COMMAND ""
   DEPENDS stage1
   EXCLUDE_FROM_ALL ON
+  STEP_TARGETS configure
 )
 ExternalProject_add(stage3
   SOURCE_DIR "${LEAN_SOURCE_DIR}"

src/Lean/Compiler/FFI.lean

@@ -17,9 +17,16 @@ private opaque getLeancExtraFlags : Unit → String
 private def flagsStringToArray (s : String) : Array String :=
   s.splitOn.toArray |>.filter (· ≠ "")
 
+/--
+Return C compiler flags for including Lean's headers.
+Unlike `getCFlags`, this does not contain the Lean include directory.
+-/
+def getCFlags' : Array String :=
+  flagsStringToArray (getLeancExtraFlags ())
+
 /-- Return C compiler flags for including Lean's headers. -/
 def getCFlags (leanSysroot : FilePath) : Array String :=
-  #["-I", (leanSysroot / "include").toString] ++ flagsStringToArray (getLeancExtraFlags ())
+  #["-I", (leanSysroot / "include").toString] ++ getCFlags'
 
 @[extern "lean_get_leanc_internal_flags"]
 private opaque getLeancInternalFlags : Unit → String
@@ -31,9 +38,16 @@ def getInternalCFlags (leanSysroot : FilePath) : Array String :=
 @[extern "lean_get_linker_flags"]
 private opaque getBuiltinLinkerFlags (linkStatic : Bool) : String
 
+/--
+Return linker flags for linking against Lean's libraries.
+Unlike `getLinkerFlags`, this does not contain the Lean library directory.
+-/
+def getLinkerFlags' (linkStatic := true) : Array String :=
+  flagsStringToArray (getBuiltinLinkerFlags linkStatic)
+
 /-- Return linker flags for linking against Lean's libraries. -/
 def getLinkerFlags (leanSysroot : FilePath) (linkStatic := true) : Array String :=
-  #["-L", (leanSysroot / "lib" / "lean").toString] ++ flagsStringToArray (getBuiltinLinkerFlags linkStatic)
+  #["-L", (leanSysroot / "lib" / "lean").toString] ++ getLinkerFlags' linkStatic
 
 @[extern "lean_get_internal_linker_flags"]
 private opaque getBuiltinInternalLinkerFlags : Unit → String

src/lake/Lake/Build/Common.lean

@@ -377,12 +377,13 @@ which will be computed in the resulting `Job` before building.
     return oFile
 
 /--
-Build an object file from a source fie job (i.e, a `lean -c` output)=
+Build an object file from a source fie job (i.e, a `lean -c` output)
 using the Lean toolchain's C compiler.
 -/
 def buildLeanO
   (oFile : FilePath) (srcJob : Job FilePath)
   (weakArgs traceArgs : Array String := #[])
+  (leanIncludeDir? : Option FilePath := none)
 : SpawnM (Job FilePath) :=
   srcJob.mapM fun srcFile => do
     addLeanTrace
@@ -390,7 +391,9 @@ def buildLeanO
     addPlatformTrace -- object files are platform-dependent artifacts
     buildFileUnlessUpToDate' oFile do
       let lean ← getLeanInstall
-      compileO oFile srcFile (lean.ccFlags ++ weakArgs ++ traceArgs) lean.cc
+      let includeDir := leanIncludeDir?.getD lean.includeDir
+      let args := #["-I", includeDir.toString] ++ lean.ccFlags ++ weakArgs ++ traceArgs
+      compileO oFile srcFile args lean.cc
     return oFile
 
 /-- Build a static library from object file jobs using the Lean toolchain's `ar`. -/
@@ -477,8 +480,8 @@ def buildLeanSharedLib
     buildFileUnlessUpToDate' libFile do
       let lean ← getLeanInstall
       let libs ← if linkDeps then mkLinkOrder libs else pure #[]
-      let args := mkLinkObjArgs objs libs ++
-        weakArgs ++ traceArgs ++ lean.ccLinkSharedFlags
+      let args := mkLinkObjArgs objs libs ++ weakArgs ++ traceArgs ++
+        #["-L", lean.leanLibDir.toString] ++ lean.ccLinkSharedFlags
       compileSharedLib libFile args lean.cc
     return {name := libName, path := libFile, deps := libs, plugin}
 
@@ -499,7 +502,7 @@ def buildLeanExe
     buildFileUnlessUpToDate' exeFile do
       let lean ← getLeanInstall
       let libs ← mkLinkOrder libs
-      let args := mkLinkObjArgs objs libs ++
-        weakArgs ++ traceArgs ++ lean.ccLinkFlags sharedLean
+      let args := mkLinkObjArgs objs libs ++ weakArgs ++ traceArgs ++
+        #["-L", lean.leanLibDir.toString] ++ lean.ccLinkFlags sharedLean
       compileExe exeFile args lean.cc
     return exeFile

src/lake/Lake/Build/Module.lean

@@ -343,7 +343,7 @@ def Module.recBuildLeanCToOExport (self : Module) : FetchM (Job FilePath) := do
   withRegisterJob s!"{self.name}:c.o{suffix}" do
   -- TODO: add option to pass a target triplet for cross compilation
   let leancArgs := self.leancArgs ++ #["-DLEAN_EXPORTING"]
-  buildLeanO self.coExportFile (← self.c.fetch) self.weakLeancArgs leancArgs
+  buildLeanO self.coExportFile (← self.c.fetch) self.weakLeancArgs leancArgs self.leanIncludeDir?
 
 /-- The `ModuleFacetConfig` for the builtin `coExportFacet`. -/
 def Module.coExportFacetConfig : ModuleFacetConfig coExportFacet :=
@@ -357,7 +357,7 @@ def Module.recBuildLeanCToONoExport (self : Module) : FetchM (Job FilePath) := d
   let suffix := if (← getIsVerbose) then " (without exports)" else ""
   withRegisterJob s!"{self.name}:c.o{suffix}" do
   -- TODO: add option to pass a target triplet for cross compilation
-  buildLeanO self.coNoExportFile (← self.c.fetch) self.weakLeancArgs self.leancArgs
+  buildLeanO self.coNoExportFile (← self.c.fetch) self.weakLeancArgs self.leancArgs self.leanIncludeDir?
 
 /-- The `ModuleFacetConfig` for the builtin `coNoExportFacet`. -/
 def Module.coNoExportFacetConfig : ModuleFacetConfig coNoExportFacet :=

src/lake/Lake/Config/InstallPath.lean

@@ -77,9 +77,9 @@ structure LeanInstall where
   ar : FilePath := "ar"
   cc : FilePath := "cc"
   customCc : Bool := true
-  cFlags := getCFlags sysroot |>.push "-Wno-unused-command-line-argument"
-  linkStaticFlags := getLinkerFlags sysroot (linkStatic := true)
-  linkSharedFlags := getLinkerFlags sysroot (linkStatic := false)
+  cFlags := getCFlags'.push "-Wno-unused-command-line-argument"
+  linkStaticFlags := getLinkerFlags' (linkStatic := true)
+  linkSharedFlags := getLinkerFlags' (linkStatic := false)
   ccFlags := cFlags
   ccLinkStaticFlags := linkStaticFlags
   ccLinkSharedFlags := linkSharedFlags

src/lake/Lake/Config/Module.lean

@@ -163,6 +163,9 @@ def dynlibSuffix := "-1"
 @[inline] def weakLinkArgs (self : Module) : Array String :=
   self.lib.weakLinkArgs
 
+@[inline] def leanIncludeDir? (self : Module) : Option FilePath :=
+  if self.pkg.bootstrap then some <| self.pkg.buildDir / "include" else none
+
 @[inline] def platformIndependent (self : Module) : Option Bool :=
   self.lib.platformIndependent
 

src/lake/Lake/Config/Package.lean

@@ -31,6 +31,9 @@ namespace Lake
 set_option linter.unusedVariables false in
 /-- A `Package`'s declarative configuration. -/
 configuration PackageConfig (name : Name) extends WorkspaceConfig, LeanConfig where
+  /-- **For internal use.** Whether this package is Lean itself. -/
+  bootstrap : Bool := false
+
   /--
   **This field is deprecated.**
 
@@ -393,6 +396,10 @@ structure PostUpdateHookDecl where
 
 namespace Package
 
+/-- **For internal use.** Whether this package is Lean itself.  -/
+@[inline] def bootstrap (self : Package) : Bool  :=
+  self.config.bootstrap
+
 /-- The package version. -/
 @[inline] def version (self : Package) : LeanVer  :=
   self.config.version

src/lake/examples/ffi/lib/lakefile.lean

@@ -44,9 +44,10 @@ target ffi_shared.o pkg : FilePath := do
 target libleanffi_shared pkg : Dynlib := do
   let libName := "leanffi"
   let ffiO ← ffi_shared.o.fetch
+  let weakArgs := #["-L", (← getLeanLibDir).toString]
   let leanArgs ← getLeanLinkSharedFlags
   buildSharedLib libName (pkg.sharedLibDir / nameToSharedLib libName)
-    #[ffiO] #[] #[] leanArgs "c++" getLeanTrace
+    #[ffiO] #[] weakArgs leanArgs "c++" getLeanTrace
 
 lean_lib FFI.Shared where
   moreLinkLibs := #[libleanffi_shared]

src/lakefile.toml.in

@@ -6,6 +6,7 @@
 # them, please consult the instructions in doc/dev/index.md.
 
 name = "lean4"
+bootstrap = true
 
 defaultTargets = ["Init", "Std", "Lean", "Lake", "LakeMain"]
 
@@ -24,11 +25,6 @@ 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"