HepLean Documentation

Lake.Build.Index

The Lake Build Index #

The Lake build index is the complete map of Lake build keys to Lake build functions, which is used by Lake to build any Lake build info.

This module leverages the index to perform topologically-based recursive builds.

source
@[macro_inline]
def Lake.mkTargetFacetBuild {α : Type} (facet : Lean.Name) (build : Lake.FetchM (Lake.BuildJob α)) [h : Lake.FamilyOut Lake.TargetData facet (Lake.BuildJob α)] :
Lake.FetchM (Lake.TargetData facet)

Converts a conveniently-typed target facet build function into its dynamically-typed equivalent.

Equations
Instances For
    source
    def Lake.ExternLib.recBuildStatic (lib : Lake.ExternLib) :
    Lake.FetchM (Lake.BuildJob System.FilePath)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lake.ExternLib.recBuildShared (lib : Lake.ExternLib) :
      Lake.FetchM (Lake.BuildJob System.FilePath)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lake.ExternLib.recComputeDynlib (lib : Lake.ExternLib) :
        Lake.FetchM (Lake.BuildJob Lake.Dynlib)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Topologically-based Recursive Build Using the Index #

          source
          def Lake.recBuildWithIndex (info : Lake.BuildInfo) :
          Lake.FetchM (Lake.BuildData info.key)

          Recursive build function for anything in the Lake build index.

          Equations
          Instances For
            source
            def Lake.FetchM.run {α : Type} (x : Lake.FetchM α) :
            Lake.RecBuildM α

            Run a recursive Lake build using the Lake build index and a topological / suspending scheduler.

            Equations
            Instances For