Documentation

Lake.Build.Module

Module Build Definitions #

Facet Builds #

Build function definitions for a module's builtin facets.

source
def Lake.Module.inputFacetConfig :
ModuleFacetConfig inputFacet

The ModuleFacetConfig for the builtin inputFacet.

Equations
    Instances For
      source
      def Lake.Module.leanFacetConfig :
      ModuleFacetConfig leanFacet

      The ModuleFacetConfig for the builtin leanFacet.

      Equations
        Instances For
          source
          def Lake.Module.headerFacetConfig :
          ModuleFacetConfig headerFacet

          The ModuleFacetConfig for the builtin headerFacet.

          Equations
            Instances For
              source
              def Lake.Module.importsFacetConfig :
              ModuleFacetConfig importsFacet

              The ModuleFacetConfig for the builtin importsFacet.

              Equations
                Instances For
                  source
                  def Lake.Module.transImportsFacetConfig :
                  ModuleFacetConfig transImportsFacet

                  The ModuleFacetConfig for the builtin transImportsFacet.

                  Equations
                    Instances For
                      source
                      def Lake.Module.precompileImportsFacetConfig :
                      ModuleFacetConfig precompileImportsFacet

                      The ModuleFacetConfig for the builtin precompileImportsFacet.

                      Equations
                        Instances For
                          source
                          def Lake.Module.importInfoFacetConfig :
                          ModuleFacetConfig importInfoFacet

                          The ModuleFacetConfig for the builtin importInfoFacet.

                          Equations
                            Instances For
                              source
                              def Lake.Module.exportInfoFacetConfig :
                              ModuleFacetConfig exportInfoFacet

                              The ModuleFacetConfig for the builtin exportInfoFacet.

                              Equations
                                Instances For
                                  source
                                  def Lake.Module.importArtsFacetConfig :
                                  ModuleFacetConfig importArtsFacet

                                  The ModuleFacetConfig for the builtin importArtsFacet.

                                  Equations
                                    Instances For
                                      source
                                      def Lake.Module.importAllArtsFacetConfig :
                                      ModuleFacetConfig importAllArtsFacet

                                      The ModuleFacetConfig for the builtin importAllArtsFacet.

                                      Equations
                                        Instances For
                                          source
                                          def Lake.Module.setupFacetConfig :
                                          ModuleFacetConfig setupFacet

                                          The ModuleFacetConfig for the builtin setupFacet.

                                          Equations
                                            Instances For
                                              source
                                              def Lake.Module.depsFacetConfig :
                                              ModuleFacetConfig depsFacet

                                              The ModuleFacetConfig for the builtin depsFacet.

                                              Equations
                                                Instances For
                                                  source
                                                  def Lake.Module.clearOutputArtifacts (mod : Module) :
                                                  IO PUnit

                                                  Remove all existing artifacts produced by the Lean build of the module.

                                                  Equations
                                                    Instances For
                                                      source
                                                      def Lake.Module.clearOutputHashes (mod : Module) :
                                                      IO PUnit

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

                                                      Equations
                                                        Instances For
                                                          source
                                                          def Lake.Module.cacheOutputHashes (mod : Module) :
                                                          IO PUnit

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

                                                          Equations
                                                            Instances For
                                                              source
                                                              def Lake.Module.leanArtsFacetConfig :
                                                              ModuleFacetConfig leanArtsFacet

                                                              The ModuleFacetConfig for the builtin leanArtsFacet.

                                                              Equations
                                                                Instances For
                                                                  source
                                                                  def Lake.Module.oleanFacetConfig :
                                                                  ModuleFacetConfig oleanFacet

                                                                  The ModuleFacetConfig for the builtin oleanFacet.

                                                                  Equations
                                                                    Instances For
                                                                      source
                                                                      def Lake.Module.oleanServerFacetConfig :
                                                                      ModuleFacetConfig oleanServerFacet

                                                                      The ModuleFacetConfig for the builtin oleanServerFacet.

                                                                      Equations
                                                                        Instances For
                                                                          source
                                                                          def Lake.Module.oleanPrivateFacetConfig :
                                                                          ModuleFacetConfig oleanPrivateFacet

                                                                          The ModuleFacetConfig for the builtin oleanPrivateFacet.

                                                                          Equations
                                                                            Instances For
                                                                              source
                                                                              def Lake.Module.ileanFacetConfig :
                                                                              ModuleFacetConfig ileanFacet

                                                                              The ModuleFacetConfig for the builtin ileanFacet.

                                                                              Equations
                                                                                Instances For
                                                                                  source
                                                                                  def Lake.Module.irFacetConfig :
                                                                                  ModuleFacetConfig irFacet

                                                                                  The ModuleFacetConfig for the builtin irFacet.

                                                                                  Equations
                                                                                    Instances For
                                                                                      source
                                                                                      def Lake.Module.cFacetConfig :
                                                                                      ModuleFacetConfig cFacet

                                                                                      The ModuleFacetConfig for the builtin cFacet.

                                                                                      Equations
                                                                                        Instances For
                                                                                          source
                                                                                          def Lake.Module.bcFacetConfig :
                                                                                          ModuleFacetConfig bcFacet

                                                                                          The ModuleFacetConfig for the builtin bcFacet.

                                                                                          Equations
                                                                                            Instances For
                                                                                              source
                                                                                              def Lake.Module.coExportFacetConfig :
                                                                                              ModuleFacetConfig coExportFacet

                                                                                              The ModuleFacetConfig for the builtin coExportFacet.

                                                                                              Equations
                                                                                                Instances For
                                                                                                  source
                                                                                                  def Lake.Module.coNoExportFacetConfig :
                                                                                                  ModuleFacetConfig coNoExportFacet

                                                                                                  The ModuleFacetConfig for the builtin coNoExportFacet.

                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      source
                                                                                                      def Lake.Module.coFacetConfig :
                                                                                                      ModuleFacetConfig coFacet

                                                                                                      The ModuleFacetConfig for the builtin coFacet.

                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          source
                                                                                                          def Lake.Module.bcoFacetConfig :
                                                                                                          ModuleFacetConfig bcoFacet

                                                                                                          The ModuleFacetConfig for the builtin bcoFacet.

                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              source
                                                                                                              def Lake.Module.oExportFacetConfig :
                                                                                                              ModuleFacetConfig oExportFacet

                                                                                                              The ModuleFacetConfig for the builtin oExportFacet.

                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  source
                                                                                                                  def Lake.Module.oNoExportFacetConfig :
                                                                                                                  ModuleFacetConfig oNoExportFacet

                                                                                                                  The ModuleFacetConfig for the builtin oNoExportFacet.

                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      source
                                                                                                                      def Lake.Module.oFacetConfig :
                                                                                                                      ModuleFacetConfig oFacet

                                                                                                                      The ModuleFacetConfig for the builtin oFacet.

                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          source
                                                                                                                          def Lake.Module.dynlibFacetConfig :
                                                                                                                          ModuleFacetConfig dynlibFacet

                                                                                                                          The ModuleFacetConfig for the builtin dynlibFacet.

                                                                                                                          Equations
                                                                                                                            Instances For
                                                                                                                              source
                                                                                                                              def Lake.Module.initFacetConfigs :
                                                                                                                              DNameMap ModuleFacetConfig

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

                                                                                                                              Equations
                                                                                                                                Instances For
                                                                                                                                  source
                                                                                                                                  @[reducible, inline]
                                                                                                                                  abbrev Lake.initModuleFacetConfigs :
                                                                                                                                  DNameMap ModuleFacetConfig

                                                                                                                                  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.

                                                                                                                                      source
                                                                                                                                      def Lake.setupServerModule (fileName : String) (path : System.FilePath) (header? : Option Lean.ModuleHeader) :
                                                                                                                                      FetchM (Job Lean.ModuleSetup)

                                                                                                                                      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
                                                                                                                                        Instances For
                                                                                                                                          source
                                                                                                                                          def Lake.prepareLeanCommand (leanFile : System.FilePath) (moreArgs : Array String := #[]) :
                                                                                                                                          FetchM (Job IO.Process.SpawnArgs)

                                                                                                                                          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
                                                                                                                                            Instances For