Documentation

Lake.Build.Module

Module Build Definitions #

Facet Builds #

Build function definitions for a module's builtin facets.

@[deprecated "Deprecated without replacement" (since := "2025-03-28")]

Compute library directories and build external library Jobs of the given packages.

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

    The ModuleFacetConfig for the builtin leanFacet.

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

      The ModuleFacetConfig for the builtin headerFacet.

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

        The ModuleFacetConfig for the builtin importInfoFacet.

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

          The ModuleFacetConfig for the builtin importArtsFacet.

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

            The ModuleFacetConfig for the builtin importAllArtsFacet.

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

              The ModuleFacetConfig for the builtin depsFacet.

              Equations
              Instances For

                Remove any cached file hashes of the module build outputs (in .hash files).

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

                  Cache the file hashes of the module build outputs in .hash files.

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

                    The ModuleFacetConfig for the builtin oleanFacet.

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

                      The ModuleFacetConfig for the builtin oleanPrivateFacet.

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

                        The ModuleFacetConfig for the builtin ileanFacet.

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

                          The ModuleFacetConfig for the builtin cFacet.

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

                            The ModuleFacetConfig for the builtin bcFacet.

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

                              The ModuleFacetConfig for the builtin oExportFacet.

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

                                The ModuleFacetConfig for the builtin oNoExportFacet.

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

                                  The ModuleFacetConfig for the builtin oFacet.

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

                                    A name-configuration map for the initial set of Lake module facets (e.g., imports, c, o, dynlib).

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[reducible, inline]

                                      A name-configuration map for the initial set of Lake module facets (e.g., imports, c, o, dynlib).

                                      Equations
                                      Instances For

                                        Top-Level Builds #

                                        Definitions to support lake setup-file and lake lean builds.

                                        Computes the module setup of edited Lean code for the Lean language server, building its imports and other dependencies. Used by lake setup-file.

                                        Due to its exclusive use as a top-level build, it does not construct a proper trace state.

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

                                          Computes the arguments required to evaluate the Lean file with lean, building its imports and other dependencies. Used by lake lean.

                                          Due to its exclusive use as a top-level build, it does not construct a proper trace state.

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