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

feat: create .ilean files

Browse source
This commit is contained in:
Sebastian Ullrich 2022-01-18 16:38:19 +01:00 • committed by tydeu
parent bffcfde602
commit e6894c058b
2 changed files with 10 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
Lake/Build/Actions.lean
View file

@ -27,31 +27,20 @@ def proc (args : IO.Process.SpawnArgs) : BuildM PUnit := do
logError s!"external command {args.cmd} exited with status {out.exitCode}"
failure
def compileOlean (leanFile oleanFile : FilePath)
def compileModule (leanFile oleanFile : FilePath) (cFile? : Option FilePath)
(oleanPath : SearchPath := []) (rootDir : FilePath := ".")
(leanArgs : Array String := #[]) (lean : FilePath := "lean")
: BuildM PUnit := do
createParentDirs oleanFile
let ileanFile := oleanFile.withExtension "ilean"
let mut args := leanArgs ++ #[
"-R", rootDir.toString, "-o", oleanFile.toString, "-i", ileanFile.toString]
if let some cFile := cFile? then
createParentDirs cFile
args := args ++ #["-c", cFile.toString]
proc {
cmd := lean.toString
args := leanArgs ++ #[
"-R", rootDir.toString, "-o", oleanFile.toString, leanFile.toString
]
env := #[("LEAN_PATH", oleanPath.toString)]
}
def compileOleanAndC (leanFile oleanFile cFile : FilePath)
(oleanPath : SearchPath := []) (rootDir : FilePath := ".")
(leanArgs : Array String := #[]) (lean : FilePath := "lean")
: BuildM PUnit := do
createParentDirs cFile
createParentDirs oleanFile
proc {
cmd := lean.toString
args := leanArgs ++ #[
"-R", rootDir.toString, "-o", oleanFile.toString, "-c",
cFile.toString, leanFile.toString
]
args := args ++ #[leanFile.toString]
env := #[("LEAN_PATH", oleanPath.toString)]
}

4
Lake/Build/Module.lean
View file

@ -136,14 +136,14 @@ def moduleOleanAndCTarget
(contents : String) (depTarget : BuildTarget x)
(rootDir : FilePath := ".") (leanArgs : Array String := #[]) : OleanAndCTarget :=
moduleTarget (OleanAndC.mk oleanFile cFile) leanFile traceFile contents depTarget do
compileOleanAndC leanFile oleanFile cFile (← getOleanPath) rootDir leanArgs (← getLean)
compileModule leanFile oleanFile cFile (← getOleanPath) rootDir leanArgs (← getLean)
def moduleOleanTarget
(leanFile oleanFile traceFile : FilePath)
(contents : String) (depTarget : BuildTarget x)
(rootDir : FilePath := ".") (leanArgs : Array String := #[]) : FileTarget :=
let target := moduleTarget oleanFile leanFile traceFile contents depTarget do
compileOlean leanFile oleanFile (← getOleanPath) rootDir leanArgs (← getLean)
compileModule leanFile oleanFile none (← getOleanPath) rootDir leanArgs (← getLean)
target.withTask do target.bindSync fun oleanFile depTrace => do
return mixTrace (← computeTrace oleanFile) depTrace