perf: cache lean exe trace in BuildM

This commit is contained in:
tydeu 2021-10-23 14:36:37 -04:00
parent 20788e8237
commit 168ec3d178
3 changed files with 14 additions and 9 deletions

View file

@ -87,8 +87,7 @@ def OleanAndCTarget.run' (self : OleanAndCTarget) : BuildM ActiveOleanAndCTarget
let oleanTask ← t.mapAsync fun info depTrace => do
return mixTrace (← computeTrace info.oleanFile) depTrace
let cTask ← t.mapAsync fun info _ => do
let leanTrace ← BuildTrace.compute (← getLean)
return mixTrace (← computeTrace info.cFile) leanTrace
return mixTrace (← computeTrace info.cFile) (← getLeanTrace)
return t.withInfo {
oleanTarget := ActiveTarget.mk self.oleanFile oleanTask
cTarget := ActiveTarget.mk self.cFile cTask
@ -100,9 +99,8 @@ def moduleTarget [CheckExists i] [GetMTime i] [ComputeHash i] (info : i)
(leanFile traceFile : FilePath) (contents : String) (depTarget : BuildTarget x)
(build : BuildM PUnit) : BuildTarget i :=
Target.mk info <| depTarget.mapOpaqueAsync fun depTrace => do
let leanTrace ← BuildTrace.compute (← getLean)
let srcTrace : BuildTrace := ⟨Hash.ofString contents, ← getMTime leanFile⟩
let fullTrace := leanTrace.mix <| srcTrace.mix depTrace
let fullTrace := (← getLeanTrace).mix <| srcTrace.mix depTrace
let (upToDate, trace) ← fullTrace.check info traceFile
unless upToDate do
build

View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Task
import Lake.Trace
import Lake.InstallPath
open System
@ -20,6 +21,7 @@ constant BuildMethodsRefPointed : PointedType.{0}
def BuildMethodsRef : Type := BuildMethodsRefPointed.type
structure BuildContext where
leanTrace : BuildTrace
leanInstall : LeanInstall
lakeInstall : LakeInstall
methodsRef : BuildMethodsRef
@ -82,10 +84,13 @@ def getLeanIncludeDir : BuildM FilePath :=
LeanInstall.includeDir <$> getLeanInstall
def getLeanc : BuildM FilePath :=
LeanInstall.leanc <$> getLeanInstall
LeanInstall.leanc <$> getLeanInstall
def getLean : BuildM FilePath :=
LeanInstall.lean <$> getLeanInstall
LeanInstall.lean <$> getLeanInstall
def getLeanTrace : BuildM BuildTrace := do
BuildContext.leanTrace <$> read
def getLakeInstall : BuildM LakeInstall :=
BuildContext.lakeInstall <$> read
@ -107,7 +112,7 @@ def runIn (ctx : BuildContext) (self : BuildM α) : IO α :=
end BuildM
export BuildM (getLeanInstall getLeanIncludeDir getLean getLeanc getLakeInstall)
export BuildM (getLeanInstall getLeanIncludeDir getLean getLeanTrace getLeanc getLakeInstall)
def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α
| Except.ok a => a

View file

@ -143,8 +143,9 @@ def getInstall : CliM (LeanInstall × LakeInstall) := do
/-- Perform the given build action using information from CLI. -/
def runBuildM (x : BuildM α) : CliM α := do
let (leanInstall, lakeInstall) ← getInstall
let leanTrace ← runIO <| computeTrace leanInstall.lean
runIO <| x.runIn {
leanInstall, lakeInstall
leanTrace, leanInstall, lakeInstall,
methodsRef := BuildMethodsRef.mk {
logInfo := fun msg => IO.println msg
logError := fun msg => IO.eprintln msg
@ -257,8 +258,9 @@ def printPaths (imports : List String := []) : CliM PUnit := do
if (← runIO' configFile.pathExists noConfigFileCode) then
let pkg ← loadPkg (← getSubArgs)
runIO do
let leanTrace ← computeTrace leanInstall.lean
let pkgs ← pkg.buildImportsAndDeps imports |>.runIn {
leanInstall, lakeInstall
leanTrace, leanInstall, lakeInstall
methodsRef := BuildMethodsRef.mk {
logInfo := fun msg => IO.eprintln msg
logError := fun msg => IO.eprintln msg