Documentation

Lake.Build.Common

General Utilities #

source
@[inline]
def Lake.inputFile (path : Lake.FilePath) :
Lake.SchedulerM (Lake.BuildJob Lake.FilePath)
Instances For
    source
    @[inline]
    def Lake.buildUnlessUpToDate {ι : Type u_1} [Lake.CheckExists ι] [Lake.GetMTime ι] (info : ι) (depTrace : Lake.BuildTrace) (traceFile : Lake.FilePath) (build : Lake.JobM PUnit) :
    Lake.JobM PUnit
    Instances For
      source
      @[inline]
      def Lake.buildFileUnlessUpToDate (file : Lake.FilePath) (depTrace : Lake.BuildTrace) (build : Lake.BuildM PUnit) :
      Lake.BuildM Lake.BuildTrace
      Instances For
        source
        @[inline]
        def Lake.buildFileAfterDep {α : Type} (file : Lake.FilePath) (dep : Lake.BuildJob α) (build : α → Lake.BuildM PUnit) (extraDepTrace : optParam (Lake.BuildM Lake.BuildTrace) (pure Lake.BuildTrace.nil)) :
        Lake.SchedulerM (Lake.BuildJob Lake.FilePath)
        Instances For
          source
          @[inline]
          def Lake.buildFileAfterDepList {α : Type} (file : Lake.FilePath) (deps : List (Lake.BuildJob α)) (build : List α → Lake.BuildM PUnit) (extraDepTrace : optParam (Lake.BuildM Lake.BuildTrace) (pure Lake.BuildTrace.nil)) :
          Lake.SchedulerM (Lake.BuildJob Lake.FilePath)
          Instances For
            source
            @[inline]
            def Lake.buildFileAfterDepArray {α : Type} (file : Lake.FilePath) (deps : Array (Lake.BuildJob α)) (build : Array α → Lake.BuildM PUnit) (extraDepTrace : optParam (Lake.BuildM Lake.BuildTrace) (pure Lake.BuildTrace.nil)) :
            Lake.SchedulerM (Lake.BuildJob Lake.FilePath)
            Instances For

              Common Builds #

              source
              def Lake.buildO (name : String) (oFile : Lake.FilePath) (srcJob : Lake.BuildJob Lake.FilePath) (args : optParam (Array String) #[]) (compiler : optParam Lake.FilePath { toString := "cc" }) :
              Lake.SchedulerM (Lake.BuildJob Lake.FilePath)
              Instances For
                source
                def Lake.buildLeanO (name : String) (oFile : Lake.FilePath) (srcJob : Lake.BuildJob Lake.FilePath) (args : optParam (Array String) #[]) :
                Lake.SchedulerM (Lake.BuildJob Lake.FilePath)
                Instances For
                  source
                  def Lake.buildStaticLib (libFile : Lake.FilePath) (oFileJobs : Array (Lake.BuildJob Lake.FilePath)) :
                  Lake.SchedulerM (Lake.BuildJob Lake.FilePath)
                  Instances For
                    source
                    def Lake.buildLeanSharedLib (libFile : Lake.FilePath) (linkJobs : Array (Lake.BuildJob Lake.FilePath)) (linkArgs : optParam (Array String) #[]) :
                    Lake.SchedulerM (Lake.BuildJob Lake.FilePath)
                    Instances For
                      source
                      def Lake.buildLeanExe (exeFile : Lake.FilePath) (linkJobs : Array (Lake.BuildJob Lake.FilePath)) (linkArgs : optParam (Array String) #[]) :
                      Lake.SchedulerM (Lake.BuildJob Lake.FilePath)
                      Instances For
                        source
                        def Lake.buildLeanSharedLibOfStatic (staticLibJob : Lake.BuildJob Lake.FilePath) (linkArgs : optParam (Array String) #[]) :
                        Lake.SchedulerM (Lake.BuildJob Lake.FilePath)
                        Instances For
                          source
                          def Lake.computeDynlibOfShared (sharedLibTarget : Lake.BuildJob Lake.FilePath) :
                          Lake.SchedulerM (Lake.BuildJob Lake.Dynlib)
                          Instances For