HepLean Documentation

Lake.Build.Data

Build Data Subtypes #

source
opaque Lake.ModuleData (facet : Lean.Name) :
Type

The open type family which maps a module facet's name to its build data in the Lake build store. For example, a transitive × direct import pair for the lean.imports facet or an active build target for lean.c.

It is an open type, meaning additional mappings can be add lazily as needed (via module_data).

source
opaque Lake.PackageData (facet : Lean.Name) :
Type

The open type family which maps a package facet's name to its build data in the Lake build store. For example, a transitive dependencies of the package for the facet deps.

It is an open type, meaning additional mappings can be add lazily as needed (via package_data).

source
opaque Lake.TargetData (facet : Lean.Name) :
Type

The open type family which maps a (builtin) Lake target's (e.g., extern_lib) facet to its associated build data. For example, an active build target for the externLib.static facet.

It is an open type, meaning additional mappings can be add lazily as needed (via target_data).

source
@[reducible, inline]
abbrev Lake.LibraryData (facet : Lean.Name) :
Type
Equations
Instances For
    source
    instance Lake.instFamilyDefNameTargetDataHAppendMkStr1OfFamilyOutLibraryData {facet : Lean.Name} {α : Type} [h : Lake.FamilyOut Lake.LibraryData facet α] :
    Lake.FamilyDef Lake.TargetData (`leanLib ++ facet) α
    Equations
    • ⋯ = ⋯
    source
    instance Lake.instFamilyDefNameLibraryDataOfFamilyOutTargetDataHAppendMkStr1 {facet : Lean.Name} {α : Type} [h : Lake.FamilyOut Lake.TargetData (`leanLib ++ facet) α] :
    Lake.FamilyDef Lake.LibraryData facet α
    Equations
    • ⋯ = ⋯
    source
    opaque Lake.CustomData (target : Lean.Name × Lean.Name) :
    Type

    The open type family which maps a custom target (package × target name) to its build data in the Lake build store.

    It is an open type, meaning additional mappings can be add lazily as needed (via custom_data).

    Build Data #

    source
    @[reducible, inline]
    abbrev Lake.BuildData :
    Lake.BuildKey → Type

    A mapping between a build key and its associated build data in the store. It is a simple type function composed of the separate open type families for modules facets, package facets, Lake target facets, and custom targets.

    Equations
    Instances For
      source
      @[instance 100]
      instance Lake.instFamilyDefBuildKeyBuildData {k : Lake.BuildKey} :
      Lake.FamilyDef Lake.BuildData k (Lake.BuildData k)
      Equations
      • ⋯ = ⋯
      source
      @[instance 100]
      instance Lake.instFamilyDefBuildKeyBuildDataModuleFacetModuleData {m f : Lean.Name} :
      Lake.FamilyDef Lake.BuildData (Lake.BuildKey.moduleFacet m f) (Lake.ModuleData f)
      Equations
      • ⋯ = ⋯
      source
      @[instance 100]
      instance Lake.instFamilyDefBuildKeyBuildDataPackageFacetPackageData {p f : Lean.Name} :
      Lake.FamilyDef Lake.BuildData (Lake.BuildKey.packageFacet p f) (Lake.PackageData f)
      Equations
      • ⋯ = ⋯
      source
      @[instance 100]
      instance Lake.instFamilyDefBuildKeyBuildDataTargetFacetTargetData {p t f : Lean.Name} :
      Lake.FamilyDef Lake.BuildData (Lake.BuildKey.targetFacet p t f) (Lake.TargetData f)
      Equations
      • ⋯ = ⋯
      source
      @[instance 100]
      instance Lake.instFamilyDefBuildKeyBuildDataCustomTargetCustomDataMkName {p t : Lean.Name} :
      Lake.FamilyDef Lake.BuildData (Lake.BuildKey.customTarget p t) (Lake.CustomData (p, t))
      Equations
      • ⋯ = ⋯

      Macros for Declaring Build Data #

      source
      def Lake.packageDataDecl :
      Lean.ParserDescr

      Macro for declaring new PackageData.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lake.moduleDataDecl :
        Lean.ParserDescr

        Macro for declaring new ModuleData.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lake.libraryDataDecl :
          Lean.ParserDescr

          Macro for declaring new TargetData for libraries.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lake.targetDataDecl :
            Lean.ParserDescr

            Macro for declaring new TargetData.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Lake.customDataDecl :
              Lean.ParserDescr

              Macro for declaring new CustomData.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For