Common Build Actions

Low level actions to build common Lean artifacts via the Lean toolchain.

def Lake.compileLeanModule (leanFile relLeanFile : System.FilePath) (oleanFile? ileanFile? cFile? bcFile? : Option System.FilePath) (leanPath : System.SearchPath := []) (rootDir : System.FilePath := { toString := "." }) (dynlibs plugins : Array Dynlib := #[]) (leanArgs : Array String := #[]) (lean : System.FilePath := { toString := "lean" }) : LogIO Unit

Equations

• One or more equations did not get rendered due to their size.

def Lake.compileO (oFile srcFile : System.FilePath) (moreArgs : Array String := #[]) (compiler : System.FilePath := { toString := "cc" }) : LogIO Unit

Equations

• Lake.compileO oFile srcFile moreArgs compiler = do liftM (Lake.createParentDirs oFile) Lake.proc { cmd := compiler.toString, args := #["-c", "-o", oFile.toString, srcFile.toString] ++ moreArgs }

def Lake.mkArgs (basePath : System.FilePath) (args : Array String) : LogIO (Array String)

Equations

• One or more equations did not get rendered due to their size.

def Lake.compileStaticLib (libFile : System.FilePath) (oFiles : Array System.FilePath) (ar : System.FilePath := { toString := "ar" }) (thin : Bool := false) : LogIO Unit

Equations

• One or more equations did not get rendered due to their size.

def Lake.compileSharedLib (libFile : System.FilePath) (linkArgs : Array String) (linker : System.FilePath := { toString := "cc" }) : LogIO Unit

Equations

• One or more equations did not get rendered due to their size.

def Lake.compileExe (binFile : System.FilePath) (linkArgs : Array String) (linker : System.FilePath := { toString := "cc" }) : LogIO Unit

Equations

• One or more equations did not get rendered due to their size.

def Lake.download (url : String) (file : System.FilePath) (headers : Array String := #[]) : LogIO PUnit

Download a file using curl, clobbering any existing file.

Equations

• One or more equations did not get rendered due to their size.

def Lake.untar (file dir : System.FilePath) (gzip : Bool := true) : LogIO PUnit

Unpack an archive file using tar into the directory dir.

Equations

• One or more equations did not get rendered due to their size.

def Lake.tar (dir file : System.FilePath) (gzip : Bool := true) (excludePaths : Array System.FilePath := #[]) : LogIO PUnit

Pack a directory dir using tar into the archive file.

Equations

• One or more equations did not get rendered due to their size.