Documentation

Lake.Build.Data

Build Data Subtypes #

opaque Lake.ModuleData (facet : Lake.Name) :

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).

opaque Lake.PackageData (facet : Lake.Name) :

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).

opaque Lake.TargetData (facet : Lake.Name) :

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).

@[inline, reducible]
abbrev Lake.LibraryData (facet : Lake.Name) :
Equations
Instances For
    Equations
    • =

    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 #

    @[inline, reducible]

    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
    • One or more equations did not get rendered due to their size.
    Instances For

      Macros for Declaring Build Data #

      Macro for declaring new PackageData.

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

        Macro for declaring new ModuleData.

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

          Macro for declaring new TargetData for libraries.

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

            Macro for declaring new TargetData.

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

              Macro for declaring new CustomData.

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