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

refactor: cleanup Compile.lean

Browse source
This commit is contained in:
tydeu 2021-10-04 17:51:47 -04:00
parent a9b87adbeb
commit e906f39201
2 changed files with 14 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
Lake/BuildTargets.lean
View file

@ -19,12 +19,12 @@ def oFileTarget
trace
def staticLibTarget
(libFile : FilePath) (oFileTargets : Array FileTarget) : FileTarget :=
(libFile : FilePath) (oFileTargets : Array FileTarget) (cmd := "ar") : FileTarget :=
Target.mk libFile do
let depTarget ← Target.collectArray oFileTargets
depTarget.mapAsync fun oFiles trace => do
unless (← checkIfNewer libFile trace.mtime) do
compileStaticLib libFile oFiles
compileStaticLib libFile oFiles cmd
trace
def binTarget

29
Lake/Compile.lean
View file

@ -27,11 +27,12 @@ def proc (args : IO.Process.SpawnArgs) : BuildM PUnit := do
throw <| IO.userError msg
def compileOlean (leanFile oleanFile : FilePath)
(oleanDirs : List FilePath := []) (rootDir : FilePath := ".") (leanArgs : Array String := #[])
(oleanDirs : List FilePath := []) (rootDir : FilePath := ".")
(leanArgs : Array String := #[]) (lean := "lean")
: BuildM PUnit := do
createParentDirs oleanFile
proc {
cmd := "lean"
cmd := lean
args := leanArgs ++ #[
"-R", rootDir.toString, "-o", oleanFile.toString, leanFile.toString
]
@ -39,12 +40,13 @@ def compileOlean (leanFile oleanFile : FilePath)
}
def compileOleanAndC (leanFile oleanFile cFile : FilePath)
(oleanDirs : List FilePath := []) (rootDir : FilePath := ".") (leanArgs : Array String := #[])
(oleanDirs : List FilePath := []) (rootDir : FilePath := ".")
(leanArgs : Array String := #[]) (lean := "lean")
: BuildM PUnit := do
createParentDirs cFile
createParentDirs oleanFile
proc {
cmd := "lean"
cmd := lean
args := leanArgs ++ #[
"-R", rootDir.toString, "-o", oleanFile.toString, "-c",
cFile.toString, leanFile.toString
@ -52,33 +54,26 @@ def compileOleanAndC (leanFile oleanFile cFile : FilePath)
env := #[("LEAN_PATH", SearchPath.toString oleanDirs)]
}
def compileO (oFile cFile : FilePath)
def compileO (oFile srcFile : FilePath)
(moreArgs : Array String := #[]) (cmd := "cc") : BuildM PUnit := do
createParentDirs oFile
proc {
cmd
args := #["-c", "-o", oFile.toString, cFile.toString] ++ moreArgs
args := #["-c", "-o", oFile.toString, srcFile.toString] ++ moreArgs
}
def compileLeanO (oFile cFile : FilePath) (leancArgs : Array String := #[]) : BuildM PUnit :=
compileO oFile cFile leancArgs "leanc"
def compileStaticLib
(libFile : FilePath) (oFiles : Array FilePath) : BuildM PUnit := do
(libFile : FilePath) (oFiles : Array FilePath) (cmd := "ar") : BuildM PUnit := do
createParentDirs libFile
proc {
cmd := "ar"
cmd
args := #["rcs", libFile.toString] ++ oFiles.map toString
}
def compileBin (binFile : FilePath)
(linkFiles : Array FilePath) (linkArgs : Array String := #[]) (cmd := "cc") : BuildM PUnit := do
(linkFiles : Array FilePath) (linkArgs : Array String := #[]) (cc := "cc") : BuildM PUnit := do
createParentDirs binFile
proc {
cmd
cmd := cc
args := #["-o", binFile.toString] ++ linkFiles.map toString ++ linkArgs
}
def compileLeanBin (binFile : FilePath)
(linkFiles : Array FilePath) (linkArgs : Array String := #[]) : BuildM PUnit :=
compileBin binFile linkFiles linkArgs "leanc"