Documentation

Lake.Build.Actions

Common Build Actions #

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

source
def Lake.compileLeanModule (leanFile : Lake.FilePath) (oleanFile? : Option Lake.FilePath) (ileanFile? : Option Lake.FilePath) (cFile? : Option Lake.FilePath) (bcFile? : Option Lake.FilePath) (leanPath : optParam Lake.SearchPath []) (rootDir : optParam Lake.FilePath { toString := "." }) (dynlibs : optParam (Array Lake.FilePath) #[]) (dynlibPath : optParam Lake.SearchPath ∅) (leanArgs : optParam (Array String) #[]) (lean : optParam Lake.FilePath { toString := "lean" }) :
Lake.LogIO Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lake.compileO (oFile : Lake.FilePath) (srcFile : Lake.FilePath) (moreArgs : optParam (Array String) #[]) (compiler : optParam Lake.FilePath { toString := "cc" }) :
Lake.LogIO Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lake.compileStaticLib (libFile : Lake.FilePath) (oFiles : Array Lake.FilePath) (ar : optParam Lake.FilePath { toString := "ar" }) :
Lake.LogIO Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lake.compileSharedLib (libFile : Lake.FilePath) (linkArgs : Array String) (linker : optParam Lake.FilePath { toString := "cc" }) :
Lake.LogIO Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lake.compileExe (binFile : Lake.FilePath) (linkFiles : Array Lake.FilePath) (linkArgs : optParam (Array String) #[]) (linker : optParam Lake.FilePath { toString := "cc" }) :
Lake.LogIO Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lake.download (url : String) (file : Lake.FilePath) (headers : optParam (Array String) #[]) :
Lake.LogIO PUnit

Download a file using curl, clobbering any existing file.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lake.untar (file : Lake.FilePath) (dir : Lake.FilePath) (gzip : optParam Bool true) :
Lake.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.
source
def Lake.tar (dir : Lake.FilePath) (file : Lake.FilePath) (gzip : optParam Bool true) (excludePaths : optParam (Array Lake.FilePath) #[]) :
Lake.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.