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.

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

    The ModuleFacetConfig for the builtin leanFacet.

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

      The ModuleFacetConfig for the builtin headerFacet.

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

        The ModuleFacetConfig for the builtin importsFacet.

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

          The ModuleFacetConfig for the builtin transImportsFacet.

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

            The ModuleFacetConfig for the builtin precompileImportsFacet.

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

              The ModuleFacetConfig for the builtin importInfoFacet.

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

                The ModuleFacetConfig for the builtin exportInfoFacet.

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

                  The ModuleFacetConfig for the builtin importArtsFacet.

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

                    The ModuleFacetConfig for the builtin importAllArtsFacet.

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

                      The ModuleFacetConfig for the builtin setupFacet.

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

                        The ModuleFacetConfig for the builtin depsFacet.

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

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

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

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

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

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

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

                                The ModuleFacetConfig for the builtin leanArtsFacet.

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

                                  The ModuleFacetConfig for the builtin oleanFacet.

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

                                    The ModuleFacetConfig for the builtin oleanServerFacet.

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

                                      The ModuleFacetConfig for the builtin oleanPrivateFacet.

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

                                        The ModuleFacetConfig for the builtin ileanFacet.

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

                                          The ModuleFacetConfig for the builtin irFacet.

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

                                            The ModuleFacetConfig for the builtin cFacet.

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

                                              The ModuleFacetConfig for the builtin bcFacet.

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

                                                The ModuleFacetConfig for the builtin coExportFacet.

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

                                                  The ModuleFacetConfig for the builtin coNoExportFacet.

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

                                                    The ModuleFacetConfig for the builtin coFacet.

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

                                                      The ModuleFacetConfig for the builtin bcoFacet.

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

                                                        The ModuleFacetConfig for the builtin oExportFacet.

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

                                                          The ModuleFacetConfig for the builtin oNoExportFacet.

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

                                                            The ModuleFacetConfig for the builtin oFacet.

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

                                                              The ModuleFacetConfig for the builtin dynlibFacet.

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

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

                                                                  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.

                                                                    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.

                                                                      Instances For