From d4a70f37ac6e1fad8abe4a6c36586fa645c556b1 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Fri, 22 Nov 2024 15:40:37 -0500 Subject: [PATCH] feat: lake: build without `leanc` --- src/lake/Lake/Build/Common.lean | 37 ++++++++++++----- src/lake/Lake/Build/Executable.lean | 2 +- src/lake/Lake/Build/Trace.lean | 4 ++ src/lake/Lake/Config/InstallPath.lean | 49 ++++++++++++++++------- src/lake/Lake/Config/LeanExe.lean | 25 +++++++----- src/lake/examples/bootstrap/lakefile.lean | 2 +- 6 files changed, 82 insertions(+), 37 deletions(-) diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean index 4917f5ad181a..aec6f769e1c7 100644 --- a/src/lake/Lake/Build/Common.lean +++ b/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,7 +316,10 @@ 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 := #[]) @@ -323,19 +327,31 @@ def buildLeanSharedLib 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. -/ diff --git a/src/lake/Lake/Build/Executable.lean b/src/lake/Lake/Build/Executable.lean index ff8ec5239136..9e411d25f215 100644 --- a/src/lake/Lake/Build/Executable.lean +++ b/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 diff --git a/src/lake/Lake/Build/Trace.lean b/src/lake/Lake/Build/Trace.lean index 9a198679a64d..309a1f3cbb53 100644 --- a/src/lake/Lake/Build/Trace.lean +++ b/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⟩ /-- diff --git a/src/lake/Lake/Config/InstallPath.lean b/src/lake/Lake/Config/InstallPath.lean index a0877ef9316f..9257ea158087 100644 --- a/src/lake/Lake/Config/InstallPath.lean +++ b/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,8 +190,7 @@ 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 @@ -187,7 +198,7 @@ where 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 diff --git a/src/lake/Lake/Config/LeanExe.lean b/src/lake/Lake/Config/LeanExe.lean index dc880b08e5c6..62b849315e41 100644 --- a/src/lake/Lake/Config/LeanExe.lean +++ b/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. diff --git a/src/lake/examples/bootstrap/lakefile.lean b/src/lake/examples/bootstrap/lakefile.lean index 3b44e0853051..dfb02c2c60c8 100644 --- a/src/lake/examples/bootstrap/lakefile.lean +++ b/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