refactor: lake: cleanup Build/Module/Trace code
This commit is contained in:
tydeu
Mac Malone
parent
a7efe5b60e
commit
c6299eef45
14 changed files with 141 additions and 175 deletions
|
|
@ -11,10 +11,10 @@ namespace Lake
|
|||
|
||||
/-! # General Utilities -/
|
||||
|
||||
@[inline] def inputFile (path : FilePath) : SchedulerM (BuildJob FilePath) :=
|
||||
def inputFile (path : FilePath) : SchedulerM (BuildJob FilePath) :=
|
||||
Job.async <| (path, ·) <$> computeTrace path
|
||||
|
||||
@[inline] def buildUnlessUpToDate [CheckExists ι] [GetMTime ι] (info : ι)
|
||||
@[specialize] def buildUnlessUpToDate [CheckExists ι] [GetMTime ι] (info : ι)
|
||||
(depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit) : JobM PUnit := do
|
||||
let isOldMode ← getIsOldMode
|
||||
let upToDate ←
|
||||
|
|
@ -27,7 +27,7 @@ namespace Lake
|
|||
unless isOldMode do
|
||||
depTrace.writeToFile traceFile
|
||||
|
||||
@[inline] def buildFileUnlessUpToDate (file : FilePath)
|
||||
def buildFileUnlessUpToDate (file : FilePath)
|
||||
(depTrace : BuildTrace) (build : BuildM PUnit) : BuildM BuildTrace := do
|
||||
let traceFile := FilePath.mk <| file.toString ++ ".trace"
|
||||
buildUnlessUpToDate file depTrace traceFile build
|
||||
|
|
@ -53,13 +53,13 @@ namespace Lake
|
|||
|
||||
/-! # Common Builds -/
|
||||
|
||||
def buildO (name : String)
|
||||
@[inline] def buildO (name : String)
|
||||
(oFile : FilePath) (srcJob : BuildJob FilePath)
|
||||
(args : Array String := #[]) (compiler : FilePath := "cc") : SchedulerM (BuildJob FilePath) :=
|
||||
buildFileAfterDep oFile srcJob (extraDepTrace := computeHash args) fun srcFile => do
|
||||
compileO name oFile srcFile args compiler
|
||||
compileO name oFile srcFile args compiler
|
||||
|
||||
def buildLeanO (name : String)
|
||||
@[inline] def buildLeanO (name : String)
|
||||
(oFile : FilePath) (srcJob : BuildJob FilePath)
|
||||
(args : Array String := #[]) : SchedulerM (BuildJob FilePath) :=
|
||||
buildFileAfterDep oFile srcJob (extraDepTrace := computeHash args) fun srcFile => do
|
||||
|
|
|
|||
|
|
@ -54,34 +54,27 @@ abbrev Module.depsFacet := `deps
|
|||
module_data deps : BuildJob (SearchPath × Array FilePath)
|
||||
|
||||
/--
|
||||
The core compilation / elaboration of the Lean file via `lean`,
|
||||
which produce the Lean binaries of the module (i.e., `olean`, `ilean`, `c`).
|
||||
The core build facet of a Lean file.
|
||||
Elaborates the Lean file via `lean` and produces all the Lean artifacts
|
||||
of the module (i.e., `olean`, `ilean`, `c`).
|
||||
Its trace just includes its dependencies.
|
||||
-/
|
||||
abbrev Module.leanBinFacet := `bin
|
||||
module_data bin : BuildJob Unit
|
||||
abbrev Module.leanArtsFacet := `leanArts
|
||||
module_data leanArts : BuildJob Unit
|
||||
|
||||
/--
|
||||
The `leanBinFacet` combined with the module's trace
|
||||
(i.e., the trace of its `olean` and `ilean`).
|
||||
It is the facet used for building a Lean import of a module.
|
||||
-/
|
||||
abbrev Module.importBinFacet := `importBin
|
||||
module_data importBin : BuildJob Unit
|
||||
|
||||
/-- The `olean` file produced by `lean` -/
|
||||
/-- The `olean` file produced by `lean`. -/
|
||||
abbrev Module.oleanFacet := `olean
|
||||
module_data olean : BuildJob FilePath
|
||||
|
||||
/-- The `ilean` file produced by `lean` -/
|
||||
/-- The `ilean` file produced by `lean`. -/
|
||||
abbrev Module.ileanFacet := `ilean
|
||||
module_data ilean : BuildJob FilePath
|
||||
|
||||
/-- The C file built from the Lean file via `lean` -/
|
||||
/-- The C file built from the Lean file via `lean`. -/
|
||||
abbrev Module.cFacet := `c
|
||||
module_data c : BuildJob FilePath
|
||||
|
||||
/-- The object file built from `lean.c` -/
|
||||
/-- The object file built from `c`. -/
|
||||
abbrev Module.oFacet := `o
|
||||
module_data o : BuildJob FilePath
|
||||
|
||||
|
|
@ -97,15 +90,15 @@ package_data extraDep : BuildJob Unit
|
|||
|
||||
/-! ## Target Facets -/
|
||||
|
||||
/-- A Lean library's Lean libraries. -/
|
||||
abbrev LeanLib.leanFacet := `lean
|
||||
library_data lean : BuildJob Unit
|
||||
/-- A Lean library's Lean artifacts (i.e., `olean`, `ilean`, `c`). -/
|
||||
abbrev LeanLib.leanArtsFacet := `leanArts
|
||||
library_data leanArts : BuildJob Unit
|
||||
|
||||
/-- A Lean library's static binary. -/
|
||||
/-- A Lean library's static artifact. -/
|
||||
abbrev LeanLib.staticFacet := `static
|
||||
library_data static : BuildJob FilePath
|
||||
|
||||
/-- A Lean library's shared binary. -/
|
||||
/-- A Lean library's shared artifact. -/
|
||||
abbrev LeanLib.sharedFacet := `shared
|
||||
library_data shared : BuildJob FilePath
|
||||
|
||||
|
|
|
|||
|
|
@ -38,7 +38,7 @@ def recBuildImports (imports : Array Module)
|
|||
precompileImports := precompileImports.appendArray (← mod.transImports.fetch) |>.insert mod
|
||||
else
|
||||
precompileImports := precompileImports.appendArray (← mod.precompileImports.fetch)
|
||||
modJobs := modJobs.push <| ← mod.leanBin.fetch
|
||||
modJobs := modJobs.push <| ← mod.leanArts.fetch
|
||||
let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
|
||||
let externJobs ← pkgs.concatMapM (·.externLibs.mapM (·.dynlib.fetch))
|
||||
let precompileJobs ← precompileImports.toArray.mapM (·.dynlib.fetch)
|
||||
|
|
|
|||
|
|
@ -193,11 +193,8 @@ abbrev facet (facet : Name) (self : Module) : BuildInfo :=
|
|||
@[inherit_doc depsFacet] abbrev deps (self : Module) :=
|
||||
self.facet depsFacet
|
||||
|
||||
@[inherit_doc leanBinFacet] abbrev leanBin (self : Module) :=
|
||||
self.facet leanBinFacet
|
||||
|
||||
@[inherit_doc importBinFacet] abbrev importBin (self : Module) :=
|
||||
self.facet importBinFacet
|
||||
@[inherit_doc leanArtsFacet] abbrev leanArts (self : Module) :=
|
||||
self.facet leanArtsFacet
|
||||
|
||||
@[inherit_doc oleanFacet] abbrev olean (self : Module) :=
|
||||
self.facet oleanFacet
|
||||
|
|
@ -240,9 +237,9 @@ abbrev LeanLib.facet (self : LeanLib) (facet : Name) : BuildInfo :=
|
|||
abbrev LeanLib.modules (self : LeanLib) : BuildInfo :=
|
||||
self.facet modulesFacet
|
||||
|
||||
@[inherit_doc leanFacet]
|
||||
abbrev LeanLib.lean (self : LeanLib) : BuildInfo :=
|
||||
self.facet leanFacet
|
||||
@[inherit_doc leanArtsFacet]
|
||||
abbrev LeanLib.leanArts (self : LeanLib) : BuildInfo :=
|
||||
self.facet leanArtsFacet
|
||||
|
||||
@[inherit_doc staticFacet]
|
||||
abbrev LeanLib.static (self : LeanLib) : BuildInfo :=
|
||||
|
|
|
|||
|
|
@ -45,10 +45,10 @@ protected def LeanLib.recBuildLean
|
|||
(self : LeanLib) : IndexBuildM (BuildJob Unit) := do
|
||||
let mods ← self.modules.fetch
|
||||
mods.foldlM (init := BuildJob.nil) fun job mod => do
|
||||
job.mix <| ← mod.leanBin.fetch
|
||||
job.mix <| ← mod.leanArts.fetch
|
||||
|
||||
/-- The `LibraryFacetConfig` for the builtin `leanFacet`. -/
|
||||
def LeanLib.leanFacetConfig : LibraryFacetConfig leanFacet :=
|
||||
/-- The `LibraryFacetConfig` for the builtin `leanArtsFacet`. -/
|
||||
def LeanLib.leanArtsFacetConfig : LibraryFacetConfig leanArtsFacet :=
|
||||
mkFacetJobConfigSmall LeanLib.recBuildLean
|
||||
|
||||
protected def LeanLib.recBuildStatic
|
||||
|
|
@ -96,7 +96,7 @@ the initial set of Lake library facets (e.g., `lean`, `static`, and `shared`).
|
|||
def initLibraryFacetConfigs : DNameMap LibraryFacetConfig :=
|
||||
DNameMap.empty
|
||||
|>.insert modulesFacet modulesFacetConfig
|
||||
|>.insert leanFacet leanFacetConfig
|
||||
|>.insert leanArtsFacet leanArtsFacetConfig
|
||||
|>.insert staticFacet staticFacetConfig
|
||||
|>.insert sharedFacet sharedFacetConfig
|
||||
|>.insert extraDepFacet extraDepFacetConfig
|
||||
|
|
|
|||
|
|
@ -15,25 +15,6 @@ open System
|
|||
|
||||
namespace Lake
|
||||
|
||||
def Module.buildUnlessUpToDate (mod : Module)
|
||||
(dynlibPath : SearchPath) (dynlibs : Array FilePath)
|
||||
(depTrace : BuildTrace) : BuildM PUnit := do
|
||||
let isOldMode ← getIsOldMode
|
||||
let argTrace : BuildTrace := pureHash mod.leanArgs
|
||||
let srcTrace : BuildTrace ← computeTrace { path := mod.leanFile : TextFilePath }
|
||||
let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace
|
||||
let modUpToDate ← do
|
||||
if isOldMode then
|
||||
srcTrace.checkAgainstTime mod
|
||||
else
|
||||
modTrace.checkAgainstFile mod mod.traceFile
|
||||
let name := mod.name.toString
|
||||
unless modUpToDate do
|
||||
compileLeanModule name mod.leanFile mod.oleanFile mod.ileanFile mod.cFile
|
||||
(← getLeanPath) mod.rootDir dynlibs dynlibPath (mod.leanArgs ++ mod.weakLeanArgs) (← getLean)
|
||||
unless isOldMode do
|
||||
modTrace.writeToFile mod.traceFile
|
||||
|
||||
/-- Compute library directories and build external library Jobs of the given packages. -/
|
||||
def recBuildExternDynlibs (pkgs : Array Package)
|
||||
: IndexBuildM (Array (BuildJob Dynlib) × Array FilePath) := do
|
||||
|
|
@ -108,7 +89,12 @@ def Module.recComputePrecompileImports (mod : Module) : IndexBuildM (Array Modul
|
|||
def Module.precompileImportsFacetConfig : ModuleFacetConfig precompileImportsFacet :=
|
||||
mkFacetConfig (·.recComputePrecompileImports)
|
||||
|
||||
/-- Recursively build a module's transitive local imports and shared library dependencies. -/
|
||||
/--
|
||||
Recursively build a module's dependencies, including:
|
||||
* Transitive local imports
|
||||
* Shared libraries (e.g., `extern_lib` targets or precompiled modules)
|
||||
* `extraDepTargets` of its library
|
||||
-/
|
||||
def Module.recBuildDeps (mod : Module) : IndexBuildM (BuildJob (SearchPath × Array FilePath)) := do
|
||||
let imports ← mod.imports.fetch
|
||||
let extraDepJob ← mod.lib.extraDep.fetch
|
||||
|
|
@ -117,7 +103,7 @@ def Module.recBuildDeps (mod : Module) : IndexBuildM (BuildJob (SearchPath × Ar
|
|||
let pkgs := precompileImports.foldl (·.insert ·.pkg)
|
||||
OrdPackageSet.empty |>.insert mod.pkg |>.toArray
|
||||
let (externJobs, libDirs) ← recBuildExternDynlibs pkgs
|
||||
let importJob ← BuildJob.mixArray <| ← imports.mapM (·.importBin.fetch)
|
||||
let importJob ← BuildJob.mixArray <| ← imports.mapM (·.olean.fetch)
|
||||
let externDynlibsJob ← BuildJob.collectArray externJobs
|
||||
let modDynlibsJob ← BuildJob.collectArray modJobs
|
||||
|
||||
|
|
@ -132,7 +118,7 @@ def Module.recBuildDeps (mod : Module) : IndexBuildM (BuildJob (SearchPath × Ar
|
|||
* Unix requires the file extension of the dynlib.
|
||||
* For some reason, building from the Lean server requires full paths.
|
||||
Everything else loads fine with just the augmented library path.
|
||||
* Linux still needs the augmented path to resolve nested dependencies in dynlibs.
|
||||
* Linux needs the augmented path to resolve nested dependencies in dynlibs.
|
||||
-/
|
||||
let dynlibPath := libDirs ++ externDynlibs.filterMap (·.dir?) |>.toList
|
||||
let dynlibs := externDynlibs.map (·.path) ++ modDynlibs.map (·.path)
|
||||
|
|
@ -142,38 +128,41 @@ def Module.recBuildDeps (mod : Module) : IndexBuildM (BuildJob (SearchPath × Ar
|
|||
def Module.depsFacetConfig : ModuleFacetConfig depsFacet :=
|
||||
mkFacetJobConfigSmall (·.recBuildDeps)
|
||||
|
||||
/-- Recursively build a module and its dependencies. -/
|
||||
def Module.recBuildLeanCore (mod : Module) : IndexBuildM (BuildJob Unit) := do
|
||||
/--
|
||||
Recursively build a Lean module.
|
||||
Fetch its dependencies and then elaborate the Lean source file, producing
|
||||
all possible artifacts (i.e., `.olean`, `ilean`, and `.c`).
|
||||
-/
|
||||
def Module.recBuildLean (mod : Module) : IndexBuildM (BuildJob Unit) := do
|
||||
(← mod.deps.fetch).bindSync fun (dynlibPath, dynlibs) depTrace => do
|
||||
mod.buildUnlessUpToDate dynlibPath dynlibs depTrace
|
||||
let argTrace : BuildTrace := pureHash mod.leanArgs
|
||||
let srcTrace : BuildTrace ← computeTrace { path := mod.leanFile : TextFilePath }
|
||||
let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace
|
||||
buildUnlessUpToDate mod modTrace mod.traceFile do
|
||||
compileLeanModule mod.name.toString mod.leanFile mod.oleanFile mod.ileanFile mod.cFile
|
||||
(← getLeanPath) mod.rootDir dynlibs dynlibPath (mod.leanArgs ++ mod.weakLeanArgs) (← getLean)
|
||||
return ((), depTrace)
|
||||
|
||||
/-- The `ModuleFacetConfig` for the builtin `leanBinFacet`. -/
|
||||
def Module.leanBinFacetConfig : ModuleFacetConfig leanBinFacet :=
|
||||
mkFacetJobConfig (·.recBuildLeanCore)
|
||||
|
||||
/-- The `ModuleFacetConfig` for the builtin `importBinFacet`. -/
|
||||
def Module.importBinFacetConfig : ModuleFacetConfig importBinFacet :=
|
||||
mkFacetJobConfigSmall fun mod => do
|
||||
(← mod.leanBin.fetch).bindSync fun _ depTrace =>
|
||||
return ((), mixTrace (← computeTrace mod) depTrace)
|
||||
/-- The `ModuleFacetConfig` for the builtin `leanArtsFacet`. -/
|
||||
def Module.leanArtsFacetConfig : ModuleFacetConfig leanArtsFacet :=
|
||||
mkFacetJobConfig (·.recBuildLean)
|
||||
|
||||
/-- The `ModuleFacetConfig` for the builtin `oleanFacet`. -/
|
||||
def Module.oleanFacetConfig : ModuleFacetConfig oleanFacet :=
|
||||
mkFacetJobConfigSmall fun mod => do
|
||||
(← mod.leanBin.fetch).bindSync fun _ depTrace =>
|
||||
(← mod.leanArts.fetch).bindSync fun _ depTrace =>
|
||||
return (mod.oleanFile, mixTrace (← computeTrace mod.oleanFile) depTrace)
|
||||
|
||||
/-- The `ModuleFacetConfig` for the builtin `ileanFacet`. -/
|
||||
def Module.ileanFacetConfig : ModuleFacetConfig ileanFacet :=
|
||||
mkFacetJobConfigSmall fun mod => do
|
||||
(← mod.leanBin.fetch).bindSync fun _ depTrace =>
|
||||
(← mod.leanArts.fetch).bindSync fun _ depTrace =>
|
||||
return (mod.ileanFile, mixTrace (← computeTrace mod.ileanFile) depTrace)
|
||||
|
||||
/-- The `ModuleFacetConfig` for the builtin `cFacet`. -/
|
||||
def Module.cFacetConfig : ModuleFacetConfig cFacet :=
|
||||
mkFacetJobConfigSmall fun mod => do
|
||||
(← mod.leanBin.fetch).bindSync fun _ _ =>
|
||||
(← mod.leanArts.fetch).bindSync fun _ _ =>
|
||||
-- do content-aware hashing so that we avoid recompiling unchanged C files
|
||||
return (mod.cFile, ← computeTrace mod.cFile)
|
||||
|
||||
|
|
@ -233,8 +222,7 @@ def initModuleFacetConfigs : DNameMap ModuleFacetConfig :=
|
|||
|>.insert transImportsFacet transImportsFacetConfig
|
||||
|>.insert precompileImportsFacet precompileImportsFacetConfig
|
||||
|>.insert depsFacet depsFacetConfig
|
||||
|>.insert leanBinFacet leanBinFacetConfig
|
||||
|>.insert importBinFacet importBinFacetConfig
|
||||
|>.insert leanArtsFacet leanArtsFacetConfig
|
||||
|>.insert oleanFacet oleanFacetConfig
|
||||
|>.insert ileanFacet ileanFacetConfig
|
||||
|>.insert cFacet cFacetConfig
|
||||
|
|
|
|||
|
|
@ -28,7 +28,7 @@ class ComputeTrace.{u,v,w} (i : Type u) (m : outParam $ Type v → Type w) (t :
|
|||
/-- Compute the trace of some target info using information from the monadic context. -/
|
||||
computeTrace : i → m t
|
||||
|
||||
def computeTrace [ComputeTrace i m t] [MonadLiftT m n] (info : i) : n t :=
|
||||
@[inline] def computeTrace [ComputeTrace i m t] [MonadLiftT m n] (info : i) : n t :=
|
||||
liftM <| ComputeTrace.computeTrace info
|
||||
|
||||
class NilTrace.{u} (t : Type u) where
|
||||
|
|
@ -45,9 +45,6 @@ class MixTrace.{u} (t : Type u) where
|
|||
|
||||
export MixTrace (mixTrace)
|
||||
|
||||
def mixTraceM [MixTrace t] [Pure m] (t1 t2 : t) : m t :=
|
||||
pure <| mixTrace t1 t2
|
||||
|
||||
section
|
||||
variable [MixTrace t] [NilTrace t]
|
||||
|
||||
|
|
@ -59,13 +56,13 @@ def mixTraceArray (traces : Array t) : t :=
|
|||
|
||||
variable [ComputeTrace i m t]
|
||||
|
||||
def computeListTrace [MonadLiftT m n] [Monad n] (artifacts : List i) : n t :=
|
||||
mixTraceList <$> artifacts.mapM computeTrace
|
||||
@[specialize] def computeListTrace [MonadLiftT m n] [Monad n] (artifacts : List i) : n t :=
|
||||
artifacts.foldlM (fun ts t => return mixTrace ts (← computeTrace t)) nilTrace
|
||||
|
||||
instance [Monad m] : ComputeTrace (List i) m t := ⟨computeListTrace⟩
|
||||
|
||||
def computeArrayTrace [MonadLiftT m n] [Monad n] (artifacts : Array i) : n t :=
|
||||
mixTraceArray <$> artifacts.mapM computeTrace
|
||||
@[specialize] def computeArrayTrace [MonadLiftT m n] [Monad n] (artifacts : Array i) : n t :=
|
||||
artifacts.foldlM (fun ts t => return mixTrace ts (← computeTrace t)) nilTrace
|
||||
|
||||
instance [Monad m] : ComputeTrace (Array i) m t := ⟨computeArrayTrace⟩
|
||||
end
|
||||
|
|
@ -84,31 +81,31 @@ structure Hash where
|
|||
|
||||
namespace Hash
|
||||
|
||||
def ofNat (n : Nat) :=
|
||||
@[inline] def ofNat (n : Nat) :=
|
||||
mk n.toUInt64
|
||||
|
||||
def loadFromFile (hashFile : FilePath) : IO (Option Hash) :=
|
||||
return (← IO.FS.readFile hashFile).toNat?.map ofNat
|
||||
def load? (hashFile : FilePath) : BaseIO (Option Hash) :=
|
||||
(·.toNat?.map ofNat) <$> IO.FS.readFile hashFile |>.catchExceptions fun _ => pure none
|
||||
|
||||
def nil : Hash :=
|
||||
mk <| 1723 -- same as Name.anonymous
|
||||
|
||||
instance : NilTrace Hash := ⟨nil⟩
|
||||
|
||||
def mix (h1 h2 : Hash) : Hash :=
|
||||
@[inline] def mix (h1 h2 : Hash) : Hash :=
|
||||
mk <| mixHash h1.val h2.val
|
||||
|
||||
instance : MixTrace Hash := ⟨mix⟩
|
||||
|
||||
protected def toString (self : Hash) : String :=
|
||||
@[inline] protected def toString (self : Hash) : String :=
|
||||
toString self.val
|
||||
|
||||
instance : ToString Hash := ⟨Hash.toString⟩
|
||||
|
||||
def ofString (str : String) :=
|
||||
@[inline] def ofString (str : String) :=
|
||||
mix nil <| mk <| hash str -- same as Name.mkSimple
|
||||
|
||||
def ofByteArray (bytes : ByteArray) : Hash :=
|
||||
@[inline] def ofByteArray (bytes : ByteArray) : Hash :=
|
||||
⟨hash bytes⟩
|
||||
|
||||
end Hash
|
||||
|
|
@ -118,10 +115,10 @@ class ComputeHash (α : Type u) (m : outParam $ Type → Type v) where
|
|||
|
||||
instance [ComputeHash α m] : ComputeTrace α m Hash := ⟨ComputeHash.computeHash⟩
|
||||
|
||||
def pureHash [ComputeHash α Id] (a : α) : Hash :=
|
||||
@[inline] def pureHash [ComputeHash α Id] (a : α) : Hash :=
|
||||
ComputeHash.computeHash a
|
||||
|
||||
def computeHash [ComputeHash α m] [MonadLiftT m n] (a : α) : n Hash :=
|
||||
@[inline] def computeHash [ComputeHash α m] [MonadLiftT m n] (a : α) : n Hash :=
|
||||
liftM <| ComputeHash.computeHash a
|
||||
|
||||
instance : ComputeHash String Id := ⟨Hash.ofString⟩
|
||||
|
|
@ -131,14 +128,8 @@ def computeFileHash (file : FilePath) : IO Hash :=
|
|||
|
||||
instance : ComputeHash FilePath IO := ⟨computeFileHash⟩
|
||||
|
||||
/--
|
||||
A wrapper around `FilePath` that adjusts its `ComputeHash` implementation
|
||||
to normalize `\r\n` sequences to `\n` for cross-platform compatibility. -/
|
||||
structure TextFilePath where
|
||||
path : FilePath
|
||||
|
||||
/-- This is the same as `String.replace text "\r\n" "\n"`, but more efficient. -/
|
||||
partial def crlf2lf (text : String) : String :=
|
||||
@[inline] partial def crlf2lf (text : String) : String :=
|
||||
go "" 0 0
|
||||
where
|
||||
go (acc : String) (accStop pos : String.Pos) : String :=
|
||||
|
|
@ -154,14 +145,26 @@ where
|
|||
else
|
||||
go acc accStop pos'
|
||||
|
||||
instance : ComputeHash TextFilePath IO where
|
||||
computeHash file := do
|
||||
let text ← IO.FS.readFile file.path
|
||||
let text := crlf2lf text
|
||||
return Hash.ofString text
|
||||
def computeTextFileHash (file : FilePath) : IO Hash := do
|
||||
let text ← IO.FS.readFile file
|
||||
let text := crlf2lf text
|
||||
return Hash.ofString text
|
||||
|
||||
instance [ComputeHash α m] [Monad m] : ComputeHash (Array α) m where
|
||||
computeHash ar := ar.foldlM (fun b a => Hash.mix b <$> computeHash a) Hash.nil
|
||||
/--
|
||||
A wrapper around `FilePath` that adjusts its `ComputeHash` implementation
|
||||
to normalize `\r\n` sequences to `\n` for cross-platform compatibility. -/
|
||||
structure TextFilePath where
|
||||
path : FilePath
|
||||
|
||||
instance : Coe TextFilePath FilePath := ⟨(·.path)⟩
|
||||
|
||||
instance : ComputeHash TextFilePath IO where
|
||||
computeHash file := computeTextFileHash file
|
||||
|
||||
@[specialize] def computeArrayHash [ComputeHash α m] [Monad m] (xs : Array α) : m Hash :=
|
||||
xs.foldlM (fun h a => return h.mix (← computeHash a)) .nil
|
||||
|
||||
instance [ComputeHash α m] [Monad m] : ComputeHash (Array α) m := ⟨computeArrayHash⟩
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
/-! # Modification Time (MTime) Trace -/
|
||||
|
|
@ -196,15 +199,15 @@ class GetMTime (α) where
|
|||
export GetMTime (getMTime)
|
||||
instance [GetMTime α] : ComputeTrace α IO MTime := ⟨getMTime⟩
|
||||
|
||||
def getFileMTime (file : FilePath) : IO MTime :=
|
||||
@[inline] def getFileMTime (file : FilePath) : IO MTime :=
|
||||
return (← file.metadata).modified
|
||||
|
||||
instance : GetMTime FilePath := ⟨getFileMTime⟩
|
||||
instance : GetMTime TextFilePath := ⟨(getFileMTime ·.path)⟩
|
||||
|
||||
/-- Check if the info's `MTIme` is at least `depMTime`. -/
|
||||
def checkIfNewer [GetMTime i] (info : i) (depMTime : MTime) : BaseIO Bool :=
|
||||
(do pure ((← getMTime info) >= depMTime : Bool)).catchExceptions fun _ => pure false
|
||||
@[inline] def checkIfNewer [GetMTime i] (info : i) (depMTime : MTime) : BaseIO Bool :=
|
||||
(return (depMTime < (← getMTime info) : Bool)).catchExceptions fun _ => pure false
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
/-! # Lake Build Trace (Hash + MTIme) -/
|
||||
|
|
@ -218,34 +221,22 @@ structure BuildTrace where
|
|||
|
||||
namespace BuildTrace
|
||||
|
||||
def withHash (hash : Hash) (self : BuildTrace) : BuildTrace :=
|
||||
{self with hash}
|
||||
|
||||
def withoutHash (self : BuildTrace) : BuildTrace :=
|
||||
{self with hash := Hash.nil}
|
||||
|
||||
def withMTime (mtime : MTime) (self : BuildTrace) : BuildTrace :=
|
||||
{self with mtime}
|
||||
|
||||
def withoutMTime (self : BuildTrace) : BuildTrace :=
|
||||
{self with mtime := 0}
|
||||
|
||||
def fromHash (hash : Hash) : BuildTrace :=
|
||||
@[inline] def ofHash (hash : Hash) : BuildTrace :=
|
||||
mk hash 0
|
||||
|
||||
instance : Coe Hash BuildTrace := ⟨fromHash⟩
|
||||
instance : Coe Hash BuildTrace := ⟨ofHash⟩
|
||||
|
||||
def fromMTime (mtime : MTime) : BuildTrace :=
|
||||
@[inline] def ofMTime (mtime : MTime) : BuildTrace :=
|
||||
mk Hash.nil mtime
|
||||
|
||||
instance : Coe MTime BuildTrace := ⟨fromMTime⟩
|
||||
instance : Coe MTime BuildTrace := ⟨ofMTime⟩
|
||||
|
||||
def nil : BuildTrace :=
|
||||
mk Hash.nil 0
|
||||
|
||||
instance : NilTrace BuildTrace := ⟨nil⟩
|
||||
|
||||
def compute [ComputeHash i m] [MonadLiftT m IO] [GetMTime i] (info : i) : IO BuildTrace :=
|
||||
@[specialize] def compute [ComputeHash i m] [MonadLiftT m IO] [GetMTime i] (info : i) : IO BuildTrace :=
|
||||
return mk (← computeHash info) (← getMTime info)
|
||||
|
||||
instance [ComputeHash i m] [MonadLiftT m IO] [GetMTime i] : ComputeTrace i IO BuildTrace := ⟨compute⟩
|
||||
|
|
@ -256,35 +247,34 @@ def mix (t1 t2 : BuildTrace) : BuildTrace :=
|
|||
instance : MixTrace BuildTrace := ⟨mix⟩
|
||||
|
||||
/--
|
||||
Check the build trace against the given target info and hash
|
||||
to see if the target is up-to-date.
|
||||
Check if the info is up-to-date using a hash.
|
||||
That is, check that info exists and its input hash matches this trace's hash.
|
||||
-/
|
||||
def checkAgainstHash [CheckExists i]
|
||||
@[inline] def checkAgainstHash [CheckExists i]
|
||||
(info : i) (hash : Hash) (self : BuildTrace) : BaseIO Bool :=
|
||||
pure (hash == self.hash) <&&> checkExists info
|
||||
|
||||
/--
|
||||
Check the build trace against the given target info and its modification time
|
||||
to see if the target is up-to-date.
|
||||
Check if the info is up-to-date using modification time.
|
||||
That is, check if the info is newer than this input trace's modification time.
|
||||
-/
|
||||
def checkAgainstTime [CheckExists i] [GetMTime i]
|
||||
@[inline] def checkAgainstTime [GetMTime i]
|
||||
(info : i) (self : BuildTrace) : BaseIO Bool :=
|
||||
checkIfNewer info self.mtime
|
||||
|
||||
/--
|
||||
Check the build trace against the given target info and its trace file
|
||||
to see if the target is up-to-date.
|
||||
Check if the info is up-to-date using a trace file.
|
||||
If the file exists, match its hash to this trace's hash.
|
||||
If not, check if the info is newer than this trace's modification time.
|
||||
-/
|
||||
def checkAgainstFile [CheckExists i] [GetMTime i]
|
||||
@[inline] def checkAgainstFile [CheckExists i] [GetMTime i]
|
||||
(info : i) (traceFile : FilePath) (self : BuildTrace) : BaseIO Bool := do
|
||||
let act : IO _ := do
|
||||
if let some hash ← Hash.loadFromFile traceFile then
|
||||
self.checkAgainstHash info hash
|
||||
else
|
||||
return self.mtime < (← getMTime info)
|
||||
act.catchExceptions fun _ => pure false
|
||||
if let some hash ← Hash.load? traceFile then
|
||||
self.checkAgainstHash info hash
|
||||
else
|
||||
self.checkAgainstTime info
|
||||
|
||||
def writeToFile (traceFile : FilePath) (self : BuildTrace) : IO PUnit :=
|
||||
@[inline] def writeToFile (traceFile : FilePath) (self : BuildTrace) : IO PUnit :=
|
||||
IO.FS.writeFile traceFile self.hash.toString
|
||||
|
||||
end BuildTrace
|
||||
|
|
|
|||
|
|
@ -52,7 +52,7 @@ def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package
|
|||
open Module in
|
||||
def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : Name) : Except CliError BuildSpec :=
|
||||
if facet.isAnonymous then
|
||||
return mkBuildSpec <| mod.facet leanBinFacet
|
||||
return mkBuildSpec <| mod.facet leanArtsFacet
|
||||
else if let some config := ws.findModuleFacetConfig? facet then do
|
||||
mkConfigBuildSpec "module" (mod.facet facet) config rfl
|
||||
else
|
||||
|
|
|
|||
|
|
@ -79,20 +79,23 @@ The optional `@` and `+` markers can be used to disambiguate packages
|
|||
and modules from other kinds of targets (i.e., executables and libraries).
|
||||
|
||||
LIBRARY FACETS: build the library's ...
|
||||
lean (default) Lean binaries (*.olean, *.ilean files)
|
||||
static static binary (*.a file)
|
||||
shared shared binary (*.so, *.dll, or *.dylib file)
|
||||
leanArts (default) Lean artifacts (*.olean, *.ilean, *.c files)
|
||||
static static artifact (*.a file)
|
||||
shared shared artifact (*.so, *.dll, or *.dylib file)
|
||||
|
||||
MODULE FACETS: build the module's ...
|
||||
deps transitive local imports & shared library dependencies
|
||||
bin (default) Lean binaries (*.olean, *.ilean files) and *.c file
|
||||
o *.o object file (of its C file)
|
||||
deps dependencies (e.g., imports, shared libraries, etc.)
|
||||
leanArts (default) Lean artifacts (*.olean, *.ilean, *.c files)
|
||||
olean OLean (binary blob of Lean data for importers)
|
||||
ilean ILean (binary blob of metadata for the Lean LSP server)
|
||||
c compiled C file
|
||||
o compiled object file (of its C file)
|
||||
dynlib shared library (e.g., for `--load-dynlib`)
|
||||
|
||||
TARGET EXAMPLES: build the ...
|
||||
a default facet of target `a`
|
||||
@a default target(s) of package `a`
|
||||
+A olean and .ilean files of module `A`
|
||||
+A Lean artifacts of module `A`
|
||||
a/b default facet of target `b` of package `a`
|
||||
a/+A:c C file of module `A` of package `a`
|
||||
:foo facet `foo` of the root package
|
||||
|
|
|
|||
|
|
@ -68,7 +68,7 @@ structure LeanLibConfig extends LeanConfig where
|
|||
An `Array` of library facets to build on a bare `lake build` of the library.
|
||||
For example, `#[LeanLib.sharedLib]` will build the shared library facet.
|
||||
-/
|
||||
defaultFacets : Array Name := #[LeanLib.leanFacet]
|
||||
defaultFacets : Array Name := #[LeanLib.leanArtsFacet]
|
||||
|
||||
/--
|
||||
An `Array` of module facets to build and combine into the library's static
|
||||
|
|
|
|||
|
|
@ -119,16 +119,11 @@ abbrev pkg (self : Module) : Package :=
|
|||
/-! ## Trace Helpers -/
|
||||
|
||||
protected def getMTime (self : Module) : IO MTime := do
|
||||
return mixTrace (← getMTime self.oleanFile) (← getMTime self.ileanFile)
|
||||
return mixTrace (mixTrace (← getMTime self.oleanFile) (← getMTime self.ileanFile)) (← getMTime self.cFile)
|
||||
|
||||
instance : GetMTime Module := ⟨Module.getMTime⟩
|
||||
|
||||
protected def computeHash (self : Module) : IO Hash := do
|
||||
return mixTrace (← computeHash self.oleanFile) (← computeHash self.ileanFile)
|
||||
|
||||
instance : ComputeHash Module IO := ⟨Module.computeHash⟩
|
||||
|
||||
protected def checkExists (self : Module) : BaseIO Bool := do
|
||||
return (← checkExists self.oleanFile) && (← checkExists self.ileanFile)
|
||||
return (← checkExists self.oleanFile) && (← checkExists self.ileanFile) && (← checkExists self.cFile)
|
||||
|
||||
instance : CheckExists Module := ⟨Module.checkExists⟩
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@ instance : MonadError (Except String) where
|
|||
Perform an EIO action.
|
||||
If it throws an error, invoke `error` with its string representation.
|
||||
-/
|
||||
protected def MonadError.runEIO [Monad m]
|
||||
@[inline] protected def MonadError.runEIO [Monad m]
|
||||
[MonadError m] [MonadLiftT BaseIO m] [ToString ε] (x : EIO ε α) : m α := do
|
||||
match (← x.toBaseIO) with
|
||||
| Except.ok a => pure a
|
||||
|
|
|
|||
|
|
@ -29,10 +29,10 @@ class MonadLog (m : Type u → Type v) where
|
|||
|
||||
export MonadLog (log getVerbosity)
|
||||
|
||||
def getIsVerbose [Functor m] [MonadLog m] : m Bool :=
|
||||
@[inline] def getIsVerbose [Functor m] [MonadLog m] : m Bool :=
|
||||
getVerbosity <&> (· == .verbose)
|
||||
|
||||
def getIsQuiet [Functor m] [MonadLog m] : m Bool :=
|
||||
@[inline] def getIsQuiet [Functor m] [MonadLog m] : m Bool :=
|
||||
getVerbosity <&> (· == .quiet)
|
||||
|
||||
@[inline] def logVerbose [Monad m] [MonadLog m] (message : String) : m PUnit := do
|
||||
|
|
@ -41,41 +41,41 @@ def getIsQuiet [Functor m] [MonadLog m] : m Bool :=
|
|||
@[inline] def logInfo [Monad m] [MonadLog m] (message : String) : m PUnit := do
|
||||
if !(← getIsQuiet) then log message .info
|
||||
|
||||
abbrev logWarning [MonadLog m] (message : String) : m PUnit :=
|
||||
@[inline] def logWarning [MonadLog m] (message : String) : m PUnit :=
|
||||
log message .warning
|
||||
|
||||
abbrev logError [MonadLog m] (message : String) : m PUnit :=
|
||||
@[inline] def logError [MonadLog m] (message : String) : m PUnit :=
|
||||
log message .error
|
||||
|
||||
namespace MonadLog
|
||||
|
||||
def nop [Pure m] : MonadLog m :=
|
||||
@[specialize] def nop [Pure m] : MonadLog m :=
|
||||
⟨pure .normal, fun _ _ => pure ()⟩
|
||||
|
||||
instance [Pure m] : Inhabited (MonadLog m) := ⟨MonadLog.nop⟩
|
||||
|
||||
def io [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
|
||||
@[specialize] def io [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
|
||||
getVerbosity := (pure verbosity : BaseIO _)
|
||||
log msg
|
||||
| .info => IO.println msg.trim |>.catchExceptions fun _ => pure ()
|
||||
| .warning => IO.eprintln s!"warning: {msg.trim}" |>.catchExceptions fun _ => pure ()
|
||||
| .error => IO.eprintln s!"error: {msg.trim}" |>.catchExceptions fun _ => pure ()
|
||||
|
||||
def eio [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
|
||||
@[specialize] def eio [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
|
||||
getVerbosity := (pure verbosity : BaseIO _)
|
||||
log msg
|
||||
| .info => IO.eprintln s!"info: {msg.trim}" |>.catchExceptions fun _ => pure ()
|
||||
| .warning => IO.eprintln s!"warning: {msg.trim}" |>.catchExceptions fun _ => pure ()
|
||||
| .error => IO.eprintln s!"error: {msg.trim}" |>.catchExceptions fun _ => pure ()
|
||||
|
||||
def lift [MonadLiftT m n] (self : MonadLog m) : MonadLog n where
|
||||
@[specialize] def lift [MonadLiftT m n] (self : MonadLog m) : MonadLog n where
|
||||
getVerbosity := liftM <| self.getVerbosity
|
||||
log msg lv := liftM <| self.log msg lv
|
||||
|
||||
instance [MonadLift m n] [methods : MonadLog m] : MonadLog n := lift methods
|
||||
|
||||
/-- Log the given error message and then fail. -/
|
||||
protected def error [Alternative m] [MonadLog m] (msg : String) : m α :=
|
||||
@[inline] protected def error [Alternative m] [MonadLog m] (msg : String) : m α :=
|
||||
logError msg *> failure
|
||||
|
||||
end MonadLog
|
||||
|
|
@ -92,11 +92,11 @@ instance [Monad n] [MonadLiftT m n] : MonadLog (MonadLogT m n) where
|
|||
getVerbosity := do (← read).getVerbosity
|
||||
log msg lv := do (← read).log msg lv
|
||||
|
||||
abbrev MonadLogT.adaptMethods [Monad n]
|
||||
@[inline] def MonadLogT.adaptMethods [Monad n]
|
||||
(f : MonadLog m → MonadLog m') (self : MonadLogT m' n α) : MonadLogT m n α :=
|
||||
ReaderT.adapt f self
|
||||
|
||||
abbrev MonadLogT.ignoreLog [Pure m] (self : MonadLogT m n α) : n α :=
|
||||
@[inline] def MonadLogT.ignoreLog [Pure m] (self : MonadLogT m n α) : n α :=
|
||||
self MonadLog.nop
|
||||
|
||||
abbrev LogIO :=
|
||||
|
|
|
|||
|
|
@ -46,5 +46,5 @@ instance : Alternative OptionIO where
|
|||
| some a => h (some a) <&> ((a, ·))
|
||||
| none => h none *> failure
|
||||
|
||||
def asTask (self : OptionIO α) (prio := Task.Priority.dedicated) : BaseIO (Task (Option α)) :=
|
||||
@[inline] def asTask (self : OptionIO α) (prio := Task.Priority.dedicated) : BaseIO (Task (Option α)) :=
|
||||
self.toBaseIO.asTask prio
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue