Common Build Actions #
Low level actions to build common Lean artifacts via the Lean toolchain.
def
Lake.compileLeanModule
(leanFile : System.FilePath)
(oleanFile? ileanFile? cFile? bcFile? : Option System.FilePath)
(leanPath : System.SearchPath := [])
(rootDir : System.FilePath := { toString := "." })
(dynlibs : Array System.FilePath := #[])
(dynlibPath : System.SearchPath := ∅)
(leanArgs : Array String := #[])
(lean : System.FilePath := { toString := "lean" })
:
Instances For
def
Lake.compileO
(oFile srcFile : System.FilePath)
(moreArgs : Array String := #[])
(compiler : System.FilePath := { toString := "cc" })
:
Instances For
def
Lake.compileStaticLib
(libFile : System.FilePath)
(oFiles : Array System.FilePath)
(ar : System.FilePath := { toString := "ar" })
:
Instances For
def
Lake.compileExe
(binFile : System.FilePath)
(linkFiles : Array System.FilePath)
(linkArgs : Array String := #[])
(linker : System.FilePath := { toString := "cc" })
:
Instances For
Download a file using curl
, clobbering any existing file.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Unpack an archive file
using tar
into the directory dir
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lake.tar
(dir file : System.FilePath)
(gzip : Bool := true)
(excludePaths : Array System.FilePath := #[])
:
Pack a directory dir
using tar
into the archive file
.