feat: lake: improved platform information & control

src/lake/Lake/Build/Common.lean

@@ -16,6 +16,13 @@ namespace Lake
 
 /-! ## General Utilities -/
 
+/--
+Build trace for the host platform.
+If an artifact includes this in its trace, it is platform-dependent
+and will be rebuilt on different host platforms.
+-/
+def platformTrace := pureHash System.Platform.target
+
 /-- Check if the `info` is up-to-date by comparing `depTrace` with `traceFile`. -/
 @[specialize] def BuildTrace.checkUpToDate [CheckExists ι] [GetMTime ι]
 (info : ι) (depTrace : BuildTrace) (traceFile : FilePath) : JobM Bool := do
@@ -138,15 +145,17 @@ which will be computed in the resulting `BuildJob` before building.
 (oFile : FilePath) (srcJob : BuildJob FilePath)
 (weakArgs traceArgs : Array String := #[]) (compiler : FilePath := "cc")
 (extraDepTrace : BuildM _ := pure BuildTrace.nil) : SchedulerM (BuildJob FilePath) :=
-  let extraDepTrace := return mixTrace (← extraDepTrace) (← computeHash traceArgs)
+  let extraDepTrace :=
+    return (← extraDepTrace).mix <| (pureHash traceArgs).mix platformTrace
   buildFileAfterDep oFile srcJob (extraDepTrace := extraDepTrace) fun srcFile => do
     compileO name oFile srcFile (weakArgs ++ traceArgs) compiler
 
 /-- Build an object file from a source fie job (i.e, a `lean -c` output) using `leanc`. -/
 @[inline] def buildLeanO (name : String)
 (oFile : FilePath) (srcJob : BuildJob FilePath)
 (weakArgs traceArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) :=
-  let extraDepTrace := return mixTrace (← getLeanTrace) (← computeHash traceArgs)
+  let extraDepTrace :=
+    return (← getLeanTrace).mix <| (pureHash traceArgs).mix platformTrace
   buildFileAfterDep oFile srcJob (extraDepTrace := extraDepTrace) fun srcFile => do
      compileO name oFile srcFile (weakArgs ++ traceArgs) (← getLeanc)
 
@@ -162,7 +171,8 @@ def buildLeanSharedLib
 (libFile : FilePath) (linkJobs : Array (BuildJob FilePath))
 (weakArgs traceArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) :=
   let name := libFile.fileName.getD libFile.toString
-  let extraDepTrace := return mixTrace (← getLeanTrace) (← computeHash traceArgs)
+  let extraDepTrace :=
+    return (← getLeanTrace).mix <| (pureHash traceArgs).mix platformTrace
   buildFileAfterDepArray libFile linkJobs (extraDepTrace := extraDepTrace) fun links => do
     compileSharedLib name libFile (links.map toString ++ weakArgs ++ traceArgs) (← getLeanc)
 
@@ -171,7 +181,8 @@ def buildLeanExe
 (exeFile : FilePath) (linkJobs : Array (BuildJob FilePath))
 (weakArgs traceArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) :=
   let name := exeFile.fileName.getD exeFile.toString
-  let extraDepTrace := return mixTrace (← getLeanTrace) (← computeHash traceArgs)
+  let extraDepTrace :=
+    return (← getLeanTrace).mix <| (pureHash traceArgs).mix platformTrace
   buildFileAfterDepArray exeFile linkJobs (extraDepTrace := extraDepTrace) fun links => do
     compileExe name exeFile links (weakArgs ++ traceArgs) (← getLeanc)
 
@@ -186,7 +197,7 @@ def buildLeanSharedLibOfStatic (staticLibJob : BuildJob FilePath)
       else
         #["-Wl,--whole-archive", staticLib.toString, "-Wl,--no-whole-archive"]
     let depTrace := staticTrace.mix <|
-      mixTrace (← getLeanTrace) (← computeHash traceArgs)
+      (← getLeanTrace).mix <| (pureHash traceArgs).mix <| platformTrace
     let args := baseArgs ++ weakArgs ++ traceArgs
     let trace ← buildFileUnlessUpToDate dynlib depTrace do
       let name := dynlib.fileName.getD dynlib.toString

src/lake/Lake/Build/Module.lean

@@ -122,7 +122,12 @@ def Module.recBuildDeps (mod : Module) : IndexBuildM (BuildJob (SearchPath × Ar
   importJob.bindAsync fun _ importTrace => do
   modDynlibsJob.bindAsync fun modDynlibs modTrace => do
   return externDynlibsJob.mapWithTrace fun externDynlibs externTrace =>
-    let depTrace := extraDepTrace.mix <| importTrace.mix <| modTrace.mix externTrace
+    let depTrace := extraDepTrace.mix <| importTrace.mix <| modTrace
+    let depTrace :=
+      match mod.platformIndependent with
+      | none => depTrace.mix <| externTrace
+      | some false => depTrace.mix <| externTrace.mix <| platformTrace
+      | some true => depTrace
     /-
     Requirements:
     * Lean wants the external library symbols before module symbols.
@@ -241,8 +246,10 @@ def Module.recBuildDynlib (mod : Module) : IndexBuildM (BuildJob Dynlib) := do
     externDynlibsJob.bindSync fun externDynlibs externLibsTrace => do
       let libNames := modDynlibs.map (·.name) ++ externDynlibs.map (·.name)
       let libDirs := pkgLibDirs ++ externDynlibs.filterMap (·.dir?)
-      let depTrace := linksTrace.mix <| modLibsTrace.mix <| externLibsTrace.mix
-        <| (← getLeanTrace).mix <| ← computeHash mod.linkArgs
+      let depTrace :=
+        linksTrace.mix <| modLibsTrace.mix <| externLibsTrace.mix
+        <| (← getLeanTrace).mix <| (pureHash mod.linkArgs).mix <|
+        platformTrace
       let trace ← buildFileUnlessUpToDate mod.dynlibFile depTrace do
         let args :=
           links.map toString ++

src/lake/Lake/Config/LeanConfig.lean

@@ -157,10 +157,31 @@ structure LeanConfig where
   They come *before* `moreLinkArgs`.
   -/
   weakLinkArgs : Array String := #[]
-
   /--
-    Compiler backend that modules should be built using (e.g., `C`, `LLVM`).
-    Defaults to `C`.
+  Compiler backend that modules should be built using (e.g., `C`, `LLVM`).
+  Defaults to `C`.
   -/
   backend : Backend := .default
+  /--
+  Asserts whether Lake should assume Lean modules are platform-independent.
+
+  * If `false`, Lake will add `System.Platform.target` to the module traces
+  within the code unit (e.g., package or library). This will force Lean code
+  to be re-elaborated on different platforms.
+
+  * If `true`, Lake will exclude platform-dependent elements
+  (e.g., precompiled modules, external libraries) from a module's trace,
+  preventing re-elaboration on different platforms. Note that this will not
+  effect  modules outside the code unit in question. For example, a
+  platform-independent package which depends on a platform-dependent library
+  will still be platform-dependent.
+
+  * If `none`, Lake will construct traces as natural. That is, it will include
+  platform-dependent artifacts in the trace if they module depends on them,
+  but otherwise not force modules to be platform-dependent.
+
+  There is no check  for correctness here, so a configuration can lie
+  and Lake will not catch it. Defaults to `none`.
+  -/
+  platformIndependent : Option Bool := none
 deriving Inhabited, Repr

src/lake/Lake/Config/LeanLib.lean

@@ -79,6 +79,14 @@ Is true if either the package or the library have `precompileModules` set.
 @[inline] def precompileModules (self : LeanLib) : Bool :=
   self.pkg.precompileModules || self.config.precompileModules
 
+/--
+Whether to the library's Lean code is platform-independent.
+Returns the library's `platformIndependent` configuration if non-`none`.
+Otherwise, falls back to the package's.
+-/
+@[inline] def platformIndependent (self : LeanLib) : Option Bool :=
+  self.config.platformIndependent <|> self.pkg.platformIndependent
+
 /-- The library's `defaultFacets` configuration. -/
 @[inline] def defaultFacets (self : LeanLib) : Array Name :=
   self.config.defaultFacets

src/lake/Lake/Config/Module.lean

@@ -135,6 +135,9 @@ def dynlibSuffix := "-1"
 @[inline] def weakLinkArgs (self : Module) : Array String :=
   self.lib.weakLinkArgs
 
+@[inline] def platformIndependent (self : Module) : Option Bool :=
+  self.lib.platformIndependent
+
 @[inline] def shouldPrecompile (self : Module) : Bool :=
   self.lib.precompileModules
 

src/lake/Lake/Config/Package.lean

@@ -13,21 +13,11 @@ import Lake.Config.Script
 import Lake.Load.Config
 import Lake.Util.DRBMap
 import Lake.Util.OrdHashSet
-import Lake.Util.Platform
 
 open System Lean
 
 namespace Lake
 
-/--
-Platform-specific archive file with an optional name prefix
-(i.e., `{name}-{platformDescriptor}.tar.gz`).
--/
-def nameToArchive (name? : Option String) : String :=
-  match name? with
-  | none => s!"{platformDescriptor}.tar.gz"
-  | some name => s!"{name}-{platformDescriptor}.tar.gz"
-
 /--
 First tries to convert a string into a legal name.
 If that fails, defaults to making it a simple name (e.g., `Lean.Name.mkSimple`).
@@ -151,11 +141,27 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
   releaseRepo? : Option String := none
 
   /--
-  The name of the build archive on GitHub. Defaults to `none`.
-  The archive's full file name will be `nameToArchive buildArchive?`.
+  The URL of the GitHub repository to upload and download releases of this package.
+  If `none` (the default), for downloads, Lake uses the URL the package was download
+  from (if it is a dependency) and for uploads, uses `gh`'s default.
+  -/
+  releaseRepo : Option String := none
+
+  /--
+  A custom name for the build archive for the GitHub cloud release.
+  If `none` (the default), Lake uses `buildArchive`, which defaults to
+  `{(pkg-)name}-{System.Platform.target}.tar.gz`.
   -/
   buildArchive? : Option String := none
 
+  /--
+  A custom name for the build archive for the GitHub cloud release.
+  Defaults to `{(pkg-)name}-{System.Platform.target}.tar.gz`.
+  -/
+  buildArchive : String :=
+    if let some name := buildArchive? then name else
+    s!"{name.toString false}-{System.Platform.target}.tar.gz"
+
   /--
   Whether to prefer downloading a prebuilt release (from GitHub) rather than
   building this package from the source when this package is used as a dependency.
@@ -295,19 +301,19 @@ namespace Package
 @[inline] def extraDepTargets (self : Package) : Array Name :=
   self.config.extraDepTargets
 
-/-- The package's `releaseRepo?` configuration. -/
-@[inline] def releaseRepo? (self : Package) : Option String :=
-  self.config.releaseRepo?
+/-- The package's `platformIndependent` configuration. -/
+@[inline] def platformIndependent (self : Package) : Option Bool :=
+  self.config.platformIndependent
 
-/-- The package's `buildArchive?` configuration. -/
-@[inline] def buildArchive? (self : Package) : Option String :=
-  self.config.buildArchive?
+/-- The package's `releaseRepo`/`releaseRepo?` configuration. -/
+@[inline] def releaseRepo? (self : Package) : Option String :=
+  self.config.releaseRepo <|> self.config.releaseRepo?
 
-/-- The file name of the package's build archive derived from `buildArchive?`. -/
+/-- The package's `buildArchive`/`buildArchive?` configuration. -/
 @[inline] def buildArchive (self : Package) : String :=
-  nameToArchive self.buildArchive?
+  self.config.buildArchive
 
-/-- The package's `lakeDir` joined with its `buildArchive` configuration. -/
+/-- The package's `lakeDir` joined with its `buildArchive`. -/
 @[inline] def buildArchiveFile (self : Package) : FilePath :=
   self.lakeDir / self.buildArchive
 

src/lake/Lake/Load/Elab.lean

@@ -8,7 +8,6 @@ import Lake.DSL.Extensions
 import Lake.DSL.Attributes
 import Lake.Load.Config
 import Lake.Build.Trace
-import Lake.Util.Platform
 import Lake.Util.Log
 
 namespace Lake
@@ -184,7 +183,7 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeOpts : NameMap String)
       let .ok (trace : ConfigTrace) := Json.parse contents >>= fromJson?
         | error "compiled configuration is invalid; run with `-R` to reconfigure"
       let upToDate :=
-        (← olean.pathExists) ∧ trace.platform = platformDescriptor ∧
+        (← olean.pathExists) ∧ trace.platform = System.Platform.target ∧
         trace.leanHash = Lean.githash ∧ trace.configHash = configHash
       if upToDate then
         return .olean h
@@ -220,7 +219,7 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeOpts : NameMap String)
     match (← IO.FS.removeFile olean |>.toBaseIO) with
     | .ok _ | .error (.noFileOrDirectory ..) =>
       h.putStrLn <| Json.pretty <| toJson
-        {platform := platformDescriptor, leanHash := Lean.githash,
+        {platform := System.Platform.target, leanHash := Lean.githash,
           configHash, options := lakeOpts : ConfigTrace}
       h.truncate
       let env ← elabConfigFile pkgDir lakeOpts leanOpts configFile

src/lake/README.md

@@ -159,7 +159,7 @@ Lake provides a large assortment of configuration options for packages.
 
 ### Build & Run
 
-* `postUpdate?`: A post-`lake update` hook. The monadic action is run after a successful `lake update` execution on this package or one of its downstream dependents. Defaults to `none`. See the option's docstring for a complete example.
+* `platformIndependent`: Asserts whether Lake should assume Lean modules are platform-independent. That is, whether lake should include the platform and platform-dependent elements in a module's trace. See the docstring of `Lake.LeanConfig.platformIndependent` for more details. Defaults to `none`.
 * `precompileModules`:  Whether to compile each module into a native shared library that is loaded whenever the module is imported. This speeds up the evaluation of metaprograms and enables the interpreter to run functions marked `@[extern]`. Defaults to `false`.
 * `moreServerOptions`: An `Array` of additional options to pass to the Lean language server (i.e., `lean --server`) launched by `lake serve`.
 * `moreGlobalServerArgs`: An `Array` of additional arguments to pass to `lean --server` which apply both to this package and anything else in the same server session (e.g. when browsing other packages from the same session via go-to-definition)
@@ -175,9 +175,9 @@ Lake provides a large assortment of configuration options for packages.
 
 ### Cloud Releases
 
-* `releaseRepo?`: The optional URL of the GitHub repository to upload and download releases of this package.  If `none` (the default), for downloads, Lake uses the URL the package was download from (if it is a dependency) and for uploads, uses `gh`'s default.
-* `buildArchive?`: The name of the build archive on GitHub. Defaults to `none`.
-The archive's full file name will end up being `nameToArchive buildArchive?`.
+* `releaseRepo`: The URL of the GitHub repository to upload and download releases of this package.  If `none` (the default), for downloads, Lake uses the URL the package was download from (if it is a dependency) and for uploads, uses `gh`'s default.
+* `buildArchive`: The name of the build archive for the GitHub cloud release.
+Defaults to `{(pkg-)name}-{System.Platform.target}.tar.gz`.
 * `preferReleaseBuild`: Whether to prefer downloading a prebuilt release (from GitHub) rather than building this package from the source when this package is used as a dependency.
 
 ## Defining Build Targets
@@ -204,7 +204,7 @@ lean_lib «target-name» where
 * `extraDepTargets`: An `Array` of [target](#custom-targets) names to build before the library's modules.
 * `defaultFacets`: An `Array` of library facets to build on a bare `lake build` of the library. For example, setting this to `#[LeanLib.sharedLib]` will build the shared library facet.
 * `nativeFacets`: An `Array` of [module facets](#defining-new-facets) to build and combine into the library's static and shared libraries. Defaults to ``#[Module.oFacet]`` (i.e., the object file compiled from the Lean source).
-* `precompileModules`, `buildType`, `leanOptions`, `<more|weak><Lean|Leanc|Link>Args`, `moreServerOptions`: Augments the package's corresponding configuration option. The library's arguments come after, modules are precompiled if either the library or package are precompiled, and the build type is the minimum of the two (`debug` is the lowest, and `release` is the highest)
+* `platformIndependent`, `precompileModules`, `buildType`, `leanOptions`, `<more|weak><Lean|Leanc|Link>Args`, `moreServerOptions`: Augments the package's corresponding configuration option. The library's arguments come after, modules are precompiled if either the library or package are, `platformIndependent` falls back to the package on `none`, and the build type is the minimum of the two (`debug` is the lowest, and `release` is the highest).
 
 ### Binary Executables
 
@@ -225,7 +225,7 @@ lean_exe «target-name» where
 * `extraDepTargets`: An `Array` of [target](#custom-targets) names to build before the executable's modules.
 * `nativeFacets`: An `Array` of [module facets](#defining-new-facets) to build and combine into the executable. Defaults to ``#[Module.oFacet]`` (i.e., the object file compiled from the Lean source).
 * `supportInterpreter`: Whether to expose symbols within the executable to the Lean interpreter. This allows the executable to interpret Lean files (e.g., via `Lean.Elab.runFrontend`). Implementation-wise, this passes `-rdynamic` to the linker when building on a non-Windows systems. Defaults to `false`.
-* `precompileModules`, `buildType`, `<more|weak><Lean|Leanc|Link>Args`, `moreServerOptions`: Augments the package's corresponding configuration option. The executable's arguments come after and the build type is the minimum of the two (`debug` is the lowest, and `release` is the highest).
+* `platformIndependent`, `precompileModules`, `buildType`, `leanOptions`, `<more|weak><Lean|Leanc|Link>Args`, `moreServerOptions`: Augments the package's corresponding configuration option. The library's arguments come after, modules are precompiled if either the library or package are, `platformIndependent` falls back to the package on `none`, and the build type is the minimum of the two (`debug` is the lowest, and `release` is the highest).
 
 ### External Libraries