Documentation

Lake.Build.Actions

Common Build Actions #

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

source
def Lake.compileLeanModule (name : String) (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.BuildM Unit
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lake.compileO (name : String) (oFile : Lake.FilePath) (srcFile : Lake.FilePath) (moreArgs : optParam (Array String) #[]) (compiler : optParam Lake.FilePath { toString := "cc" }) :
    Lake.BuildM Unit
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lake.compileStaticLib (name : String) (libFile : Lake.FilePath) (oFiles : Array Lake.FilePath) (ar : optParam Lake.FilePath { toString := "ar" }) :
      Lake.BuildM Unit
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lake.compileSharedLib (name : String) (libFile : Lake.FilePath) (linkArgs : Array String) (linker : optParam Lake.FilePath { toString := "cc" }) :
        Lake.BuildM Unit
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lake.compileExe (name : String) (binFile : Lake.FilePath) (linkFiles : Array Lake.FilePath) (linkArgs : optParam (Array String) #[]) (linker : optParam Lake.FilePath { toString := "cc" }) :
          Lake.BuildM Unit
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lake.download (name : String) (url : String) (file : Lake.FilePath) :
            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.
            Instances For
              source
              def Lake.untar (name : String) (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.
              Instances For
                source
                def Lake.tar (name : String) (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.
                Instances For