HepLean Documentation

Lake.Build.Store

The Lake Build Store #

The Lake build store is the map of Lake build keys to build task and/or build results that is slowly filled during a recursive build (e.g., via topological-based build of an initial key's dependencies).

source
@[reducible, inline]
abbrev Lake.MonadBuildStore (m : Type → Type u_1) :
Type u_1

A monad equipped with a Lake build store.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Lake.BuildStore :
    Type

    The type of the Lake build store.

    Equations
    Instances For
      source
      @[inline]
      def Lake.BuildStore.empty :
      Lake.BuildStore
      Equations
      Instances For
        source
        def Lake.BuildStore.collectModuleFacetArray {α : Type} (self : Lake.BuildStore) (facet : Lean.Name) [Lake.FamilyOut Lake.ModuleData facet α] :
        Array α

        Derive an array of built module facets from the store.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lake.BuildStore.collectModuleFacetMap {α : Type} (self : Lake.BuildStore) (facet : Lean.Name) [Lake.FamilyOut Lake.ModuleData facet α] :
          Lean.NameMap α

          Derive a map of module names to built facets from the store.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lake.BuildStore.collectPackageFacetArray {α : Type} (self : Lake.BuildStore) (facet : Lean.Name) [Lake.FamilyOut Lake.PackageData facet α] :
            Array α

            Derive an array of built package facets from the store.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Lake.BuildStore.collectTargetFacetArray {α : Type} (self : Lake.BuildStore) (facet : Lean.Name) [Lake.FamilyOut Lake.TargetData facet α] :
              Array α

              Derive an array of built target facets from the store.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Lake.BuildStore.collectSharedExternLibs {α : Type} (self : Lake.BuildStore) [Lake.FamilyOut Lake.TargetData `externLib.shared α] :
                Array α

                Derive an array of built external shared libraries from the store.

                Equations
                • self.collectSharedExternLibs = self.collectTargetFacetArray `externLib.shared
                Instances For