max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add args to binary & .o file traces + some cleanup

Browse source 
closes leanprover/lake#41
This commit is contained in:
tydeu 2021-12-27 12:07:15 -05:00
parent 2680e1c66f
commit 752bc24f78
1 changed files with 22 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

45
Lake/Build/Targets.lean
View file

@ -16,43 +16,42 @@ def inputFileTarget (path : FilePath) : FileTarget :=
instance : Coe FilePath FileTarget := ⟨inputFileTarget⟩
def buildUnlessUpToDate [CheckExists i] [GetMTime i] (info : i)
(depTrace : BuildTrace) (traceFile : FilePath) (build : BuildM PUnit) : BuildM PUnit := do
let upToDate ← depTrace.checkAgainstFile info traceFile
unless upToDate do
build
depTrace.writeToFile traceFile
def buildFileUnlessUpToDate (file : FilePath)
(depTrace : BuildTrace) (build : BuildM PUnit) : BuildM BuildTrace := do
let traceFile := FilePath.mk <| file.toString ++ ".trace"
let upToDate ← depTrace.checkAgainstFile file traceFile
unless upToDate do
build
depTrace.writeToFile traceFile
buildUnlessUpToDate file depTrace traceFile build
computeTrace file
def fileTargetWithDep (file : FilePath)
(depTarget : BuildTarget i) (build : i → BuildM PUnit) : FileTarget :=
Target.mk file do
depTarget.bindSync fun depInfo depTrace =>
buildFileUnlessUpToDate file depTrace <| build depInfo
def fileTargetWithDep (file : FilePath) (depTarget : BuildTarget i)
(build : i → BuildM PUnit) (extraDepTrace := BuildTrace.nil) : FileTarget :=
Target.mk file <| depTarget.bindSync fun depInfo depTrace =>
buildFileUnlessUpToDate file (depTrace.mix extraDepTrace) <| build depInfo
def fileTargetWithDepList (file : FilePath)
(depTargets : List (BuildTarget i)) (build : List i → BuildM PUnit) : FileTarget :=
Target.mk file do
Target.collectList depTargets |>.bindSync fun depInfos depTrace =>
buildFileUnlessUpToDate file depTrace <| build depInfos
def fileTargetWithDepList (file : FilePath) (depTargets : List (BuildTarget i))
(build : List i → BuildM PUnit) (extraDepTrace := BuildTrace.nil) : FileTarget :=
fileTargetWithDep file (Target.collectList depTargets) build extraDepTrace
def fileTargetWithDepArray (file : FilePath)
(depTargets : Array (BuildTarget i)) (build : Array i → BuildM PUnit) : FileTarget :=
Target.mk file do
Target.collectArray depTargets |>.bindSync fun depInfos depTrace =>
buildFileUnlessUpToDate file depTrace <| build depInfos
def fileTargetWithDepArray (file : FilePath) (depTargets : Array (BuildTarget i))
(build : Array i → BuildM PUnit) (extraDepTrace := BuildTrace.nil) : FileTarget :=
fileTargetWithDep file (Target.collectArray depTargets) build extraDepTrace
-- # Specific Targets
def oFileTarget (oFile : FilePath) (srcTarget : FileTarget)
(args : Array String := #[]) (compiler : FilePath := "c++") : FileTarget :=
fileTargetWithDep oFile srcTarget fun srcFile => do
fileTargetWithDep oFile srcTarget (extraDepTrace := pureHash args) fun srcFile => do
compileO oFile srcFile args compiler
def leanOFileTarget (oFile : FilePath)
(srcTarget : FileTarget) (args : Array String := #[]) : FileTarget :=
fileTargetWithDep oFile srcTarget fun srcFile => do
fileTargetWithDep oFile srcTarget (extraDepTrace := pureHash args) fun srcFile => do
compileO oFile srcFile args (← getLeanc)
def staticLibTarget (libFile : FilePath)
@ -67,10 +66,10 @@ def leanSharedLibTarget (binFile : FilePath)
def binTarget (binFile : FilePath) (linkTargets : Array FileTarget)
(linkArgs : Array String := #[]) (linker : FilePath := "cc") : FileTarget :=
fileTargetWithDepArray binFile linkTargets fun links => do
fileTargetWithDepArray binFile linkTargets (extraDepTrace := pureHash linkArgs) fun links => do
compileBin binFile links linkArgs linker
def leanBinTarget (binFile : FilePath)
(linkTargets : Array FileTarget) (linkArgs : Array String := #[]) : FileTarget :=
fileTargetWithDepArray binFile linkTargets fun links => do
fileTargetWithDepArray binFile linkTargets (extraDepTrace := pureHash linkArgs) fun links => do
compileBin binFile links linkArgs (← getLeanc)