Documentation

Lake.Build.Actions

Common Build Actions #

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

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

            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 (name : String) (dir : Lake.FilePath) (file : Lake.FilePath) (gzip : optParam Bool true) (excludePaths : optParam (Array Lake.FilePath) #[]) :

                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