feat: lake: build without leanc (#6176)

This PR changes Lake's build process to no longer use `leanc` for
compiling C files or linking shared libraries and executables. Instead,
it directly invokes the bundled compiler (or the native compiler if
none) using the necessary flags.

src/lake/Lake/Build/Actions.lean

@@ -105,6 +105,16 @@ def compileExe
   proc {
     cmd := linker.toString
     args := #["-o", binFile.toString] ++ linkFiles.map toString ++ linkArgs
+    env := ← do
+      -- It is difficult to identify the correct minor version here, leading to linking warnings like:
+      -- `ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 13.5.0, which is newer than target minimum of 13.0.0`
+      -- In order to suppress these we set the MACOSX_DEPLOYMENT_TARGET variable into the far future.
+      if System.Platform.isOSX then
+        match (← IO.getEnv "MACOSX_DEPLOYMENT_TARGET") with
+        | some _ => pure #[]
+        | none => pure #[("MACOSX_DEPLOYMENT_TARGET", some "99.0")]
+      else
+        pure #[]
   }
 
 /-- Download a file using `curl`, clobbering any existing file. -/

src/lake/Lake/Build/Common.lean

@@ -306,7 +306,8 @@ which will be computed in the resulting `BuildJob` before building.
   let extraDepTrace :=
     return (← getLeanTrace).mix <| (pureHash traceArgs).mix platformTrace
   buildFileAfterDep oFile srcJob (extraDepTrace := extraDepTrace) fun srcFile => do
-     compileO oFile srcFile (weakArgs ++ traceArgs) (← getLeanc)
+    let lean ← getLeanInstall
+    compileO oFile srcFile (lean.ccFlags ++ weakArgs ++ traceArgs) lean.cc
 
 /-- Build a static library from object file jobs using the `ar` packaged with Lean. -/
 def buildStaticLib
@@ -315,27 +316,42 @@ def buildStaticLib
   buildFileAfterDepArray libFile oFileJobs fun oFiles => do
     compileStaticLib libFile oFiles (← getLeanAr)
 
-/-- Build a shared library by linking the results of `linkJobs` using `leanc`. -/
+/--
+Build a shared library by linking the results of `linkJobs`
+using the Lean toolchain's C compiler.
+-/
 def buildLeanSharedLib
   (libFile : FilePath) (linkJobs : Array (BuildJob FilePath))
   (weakArgs traceArgs : Array String := #[])
 : SpawnM (BuildJob FilePath) :=
   let extraDepTrace :=
     return (← getLeanTrace).mix <| (pureHash traceArgs).mix platformTrace
   buildFileAfterDepArray libFile linkJobs (extraDepTrace := extraDepTrace) fun links => do
-    compileSharedLib libFile (links.map toString ++ weakArgs ++ traceArgs) (← getLeanc)
+    let lean ← getLeanInstall
+    let args := links.map toString ++ weakArgs ++ traceArgs ++ lean.ccLinkSharedFlags
+    compileSharedLib libFile args lean.cc
+
 
-/-- Build an executable by linking the results of `linkJobs` using `leanc`. -/
+/--
+Build an executable by linking the results of `linkJobs`
+using the Lean toolchain's linker.
+-/
 def buildLeanExe
   (exeFile : FilePath) (linkJobs : Array (BuildJob FilePath))
-  (weakArgs traceArgs : Array String := #[])
+  (weakArgs traceArgs : Array String := #[]) (sharedLean : Bool := false)
 : SpawnM (BuildJob FilePath) :=
   let extraDepTrace :=
-    return (← getLeanTrace).mix <| (pureHash traceArgs).mix platformTrace
+    return (← getLeanTrace).mix <|
+      (pureHash sharedLean).mix <| (pureHash traceArgs).mix platformTrace
   buildFileAfterDepArray exeFile linkJobs (extraDepTrace := extraDepTrace) fun links => do
-    compileExe exeFile links (weakArgs ++ traceArgs) (← getLeanc)
+    let lean ← getLeanInstall
+    let args := weakArgs ++ traceArgs ++ lean.ccLinkFlags sharedLean
+    compileExe exeFile links args lean.cc
 
-/-- Build a shared library from a static library using `leanc`. -/
+/--
+Build a shared library from a static library using `leanc`
+using the Lean toolchain's linker.
+-/
 def buildLeanSharedLibOfStatic
   (staticLibJob : BuildJob FilePath)
   (weakArgs traceArgs : Array String := #[])
@@ -347,11 +363,12 @@ def buildLeanSharedLibOfStatic
         #[s!"-Wl,-force_load,{staticLib}"]
       else
         #["-Wl,--whole-archive", staticLib.toString, "-Wl,--no-whole-archive"]
+    let lean ← getLeanInstall
     let depTrace := staticTrace.mix <|
       (← getLeanTrace).mix <| (pureHash traceArgs).mix <| platformTrace
-    let args := baseArgs ++ weakArgs ++ traceArgs
+    let args := baseArgs ++ weakArgs ++ traceArgs ++ lean.ccLinkSharedFlags
     let trace ← buildFileUnlessUpToDate dynlib depTrace do
-      compileSharedLib dynlib args (← getLeanc)
+      compileSharedLib dynlib args lean.cc
     return (dynlib, trace)
 
 /-- Construct a `Dynlib` object for a shared library target. -/

src/lake/Lake/Build/Executable.lean

@@ -29,4 +29,4 @@ def LeanExe.recBuildExe (self : LeanExe) : FetchM (BuildJob FilePath) :=
   let deps := (← fetch <| self.pkg.facet `deps).push self.pkg
   for dep in deps do for lib in dep.externLibs do
     linkJobs := linkJobs.push <| ← lib.static.fetch
-  buildLeanExe self.file linkJobs self.weakLinkArgs self.linkArgs
+  buildLeanExe self.file linkJobs self.weakLinkArgs self.linkArgs self.sharedLean

src/lake/Lake/Build/Trace.lean

@@ -125,6 +125,9 @@ instance : ToString Hash := ⟨Hash.toString⟩
 @[inline] def ofByteArray (bytes : ByteArray) : Hash :=
   ⟨hash bytes⟩
 
+@[inline] def ofBool (b : Bool) :=
+  mk (hash b)
+
 @[inline] protected def toJson (self : Hash) : Json :=
   toJson self.val
 
@@ -151,6 +154,7 @@ instance [ComputeHash α m] : ComputeTrace α m Hash := ⟨ComputeHash.computeHa
 @[inline] def computeHash [ComputeHash α m] [MonadLiftT m n] (a : α) : n Hash :=
   liftM <| ComputeHash.computeHash a
 
+instance : ComputeHash Bool Id := ⟨Hash.ofBool⟩
 instance : ComputeHash String Id := ⟨Hash.ofString⟩
 
 /--

src/lake/Lake/Config/InstallPath.lean

@@ -3,10 +3,12 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lean.Compiler.FFI
 import Lake.Util.NativeLib
 import Lake.Config.Defaults
 
-open System
+open System Lean.Compiler.FFI
+
 namespace Lake
 
 /-- Convert the string value of an environment variable to a boolean. -/
@@ -71,7 +73,13 @@ structure LeanInstall where
   initSharedLib := leanSharedLibDir sysroot / initSharedLib
   ar : FilePath := "ar"
   cc : FilePath := "cc"
-  customCc : Bool := false
+  customCc : Bool := true
+  cFlags := getCFlags sysroot |>.push "-Wno-unused-command-line-argument"
+  linkStaticFlags := getLinkerFlags sysroot (linkStatic := true)
+  linkSharedFlags := getLinkerFlags sysroot (linkStatic := false)
+  ccFlags := cFlags
+  ccLinkStaticFlags := linkStaticFlags
+  ccLinkSharedFlags := linkSharedFlags
   deriving Inhabited, Repr
 
 /--
@@ -88,6 +96,10 @@ def LeanInstall.sharedLibPath (self : LeanInstall) : SearchPath :=
 def LeanInstall.leanCc? (self : LeanInstall) : Option String :=
   if self.customCc then self.cc.toString else none
 
+/-- The link-time flags for the C compiler of the Lean installation. -/
+def LeanInstall.ccLinkFlags (shared : Bool) (self : LeanInstall) : Array String :=
+  if shared then self.ccLinkSharedFlags else self.ccLinkStaticFlags
+
 /-- Lake executable file name. -/
 def lakeExe : FilePath :=
   FilePath.addExtension "lake" FilePath.exeExtension
@@ -178,16 +190,15 @@ def LeanInstall.get (sysroot : FilePath) (collocated : Bool := false) : BaseIO L
       -- Remark: This is expensive (at least on Windows), so try to avoid it.
       getGithash
   let ar ← findAr
-  let (cc, customCc) ← findCc
-  return {sysroot, githash, ar, cc, customCc}
+  setCc {sysroot, githash, ar}
 where
   getGithash := do
     EIO.catchExceptions (h := fun _ => pure "") do
       let out ← IO.Process.output {
         cmd := leanExe sysroot |>.toString,
         args := #["--githash"]
       }
-      pure <| out.stdout.trim
+      return out.stdout.trim
   findAr := do
     if let some ar ← IO.getEnv "LEAN_AR" then
       return FilePath.mk ar
@@ -199,19 +210,27 @@ where
         return ar
       else
         return "ar"
-  findCc := do
+  setCc i := do
     if let some cc ← IO.getEnv "LEAN_CC" then
-      return (FilePath.mk cc, true)
+      return withCustomCc i cc
     else
       let cc := leanCcExe sysroot
-      let cc ←
-        if (← cc.pathExists) then
-          pure cc
-        else if let some cc ← IO.getEnv "CC" then
-          pure cc
-        else
-          pure "cc"
-      return (cc, false)
+      if (← cc.pathExists) then
+        return withInternalCc i cc
+      else if let some cc ← IO.getEnv "CC" then
+        return withCustomCc i cc
+      else
+        return withCustomCc i "cc"
+  @[inline] withCustomCc (i : LeanInstall) cc :=
+    {i with cc}
+  withInternalCc (i : LeanInstall) cc :=
+    let ccLinkFlags := getInternalLinkerFlags sysroot
+    {i with
+      cc, customCc := false
+      ccFlags := i.cFlags ++ getInternalCFlags sysroot
+      ccLinkStaticFlags := ccLinkFlags ++ i.linkStaticFlags
+      ccLinkSharedFlags := ccLinkFlags ++ i.linkSharedFlags
+    }
 
 /--
 Attempt to detect the installation of the given `lean` command

src/lake/Lake/Config/LeanExe.lean

@@ -3,7 +3,6 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lean.Compiler.FFI
 import Lake.Config.Module
 
 namespace Lake
@@ -74,21 +73,27 @@ The file name of binary executable
 
 /--
 The arguments to pass to `leanc` when linking the binary executable.
-By default, the package's plus the executable's `moreLinkArgs`.
 
-If `supportInterpreter := true`, Lake links directly to the Lean shared
-libraries on Windows by prepending `-leanshared` and adds `-rdynamic` on
-other systems.
+By default, the package's plus the executable's `moreLinkArgs`.
+If `supportInterpreter := true`, Lake prepends `-rdynamic` on non-Windows
+systems.
 -/
 def linkArgs (self : LeanExe) : Array String :=
-  if self.config.supportInterpreter then
-    if Platform.isWindows then
-      #["-leanshared"] ++ self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
-    else
-      #["-rdynamic"] ++ self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
+  if self.config.supportInterpreter && !Platform.isWindows then
+    #["-rdynamic"] ++ self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
   else
     self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
 
+/--
+Whether the Lean shared library should be dynamically linked to the executable.
+
+If `supportInterpreter := true`, Lean symbols must be visible to the
+interpreter. On Windows, it is not possible to statically include these
+symbols in the executable due to symbol limits, so Lake dynamically links to
+the Lean shared library. Otherwise, Lean is linked statically.
+-/
+@[inline] def sharedLean (self : LeanExe) : Bool :=
+  strictAnd Platform.isWindows self.config.supportInterpreter
 
 /--
 The arguments to weakly pass to `leanc` when linking the binary executable.

src/lake/examples/bootstrap/lakefile.lean

@@ -8,5 +8,5 @@ lean_lib Lake
 
 @[default_target]
 lean_exe lake where
-  root := `Lake.Main
+  root := `LakeMain
   supportInterpreter := true

src/lake/tests/buildArgs/test.sh

@@ -3,39 +3,37 @@ set -exo pipefail
 
 LAKE=${LAKE:-../../.lake/build/bin/lake}
 
-unamestr=`uname`
-if [ "$unamestr" = Darwin ] || [ "$unamestr" = FreeBSD ]; then
-  sed_i() { sed -i '' "$@"; }
-else
-  sed_i() { sed -i "$@"; }
-fi
-
 ./clean.sh
 
 # Test that changing `moreLean/Leanc/LinkArgs` triggers a rebuild
 # Test that changing `weakLean/Leanc/LinkArgs` does not
 
+# Test `leanArgs`
 ${LAKE} build +Hello -R
 # see https://github.com/leanprover/lake/issues/50
 ${LAKE} build +Hello -R -KleanArgs=-DwarningAsError=true -v | grep --color warningAsError
 
+# Test `weakLeanArgs`
 ${LAKE} build +Hello -R
 # see https://github.com/leanprover/lake/issues/172
 ${LAKE} build +Hello -R -KweakLeanArgs=-DwarningAsError=true --no-build
 
+# Test `leancArgs`
 ${LAKE} build +Hello:o -R
-${LAKE} build +Hello:o -R -KleancArgs=-DBAR -v | grep --color leanc
+${LAKE} build +Hello:o -R -KleancArgs=-DBAR -v | grep --color "Built Hello:c.o"
 
+# Test `weakLeancArgs`
 ${LAKE} build +Hello:o -R
 ${LAKE} build +Hello:o -R -KweakLeancArgs=-DBAR --no-build
 
+# Test `linkArgs`
 ${LAKE} build +Hello:dynlib Hello:shared hello -R
-${LAKE} build +Hello:dynlib -R -KlinkArgs=-L.lake/build/lib -v | grep --color leanc
-${LAKE} build Hello:shared -R -KlinkArgs=-L.lake/build/lib -v | grep --color leanc
-${LAKE} build hello -R -KlinkArgs=-L.lake/build/lib -v | grep --color leanc
+${LAKE} build +Hello:dynlib -R -KlinkArgs=-L.lake/build/lib -v | grep --color "Built Hello:dynlib"
+${LAKE} build Hello:shared -R -KlinkArgs=-L.lake/build/lib -v | grep --color "Built Hello:shared"
+${LAKE} build hello -R -KlinkArgs=-L.lake/build/lib -v | grep --color "Built hello"
 
+# Test `weakLinkArgs`
 ${LAKE} build +Hello:dynlib Hello:shared hello  -R
 ${LAKE} build +Hello:dynlib -R -KweakLinkArgs=-L.lake/build/lib  --no-build
 ${LAKE} build Hello:shared -R -KweakLinkArgs=-L.lake/build/lib  --no-build
 ${LAKE} build hello -R -KweakLinkArgs=-L.lake/build/lib  --no-build
-