Documentation

Lake.Build.Targets

Build Target Fetching #

Utilities for fetching package, library, module, and executable targets and facets.

Package Facets & Targets #

source
def Lake.Package.fetchTargetJob (self : Lake.Package) (target : Lean.Name) :
Lake.FetchM (Lake.BuildJob Unit)

Fetch the build job of the specified package target.

Instances For
    source
    def Lake.TargetDecl.fetch {α : Type} (self : Lake.TargetDecl) [Lake.FamilyOut Lake.CustomData (self.pkg, self.name) α] :
    Lake.FetchM α

    Fetch the build result of a target.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lake.TargetDecl.fetchJob (self : Lake.TargetDecl) :
      Lake.FetchM (Lake.BuildJob Unit)

      Fetch the build job of the target.

      Instances For
        source
        @[inline]
        def Lake.PackageFacetDecl.fetch {α : Type} (pkg : Lake.Package) (self : Lake.PackageFacetDecl) [Lake.FamilyOut Lake.PackageData self.name α] :
        Lake.FetchM α

        Fetch the build result of a package facet.

        Instances For
          source
          def Lake.PackageFacetConfig.fetchJob {name : Lean.Name} (pkg : Lake.Package) (self : Lake.PackageFacetConfig name) :
          Lake.FetchM (Lake.BuildJob Unit)

          Fetch the build job of a package facet.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lake.Package.fetchFacetJob (name : Lean.Name) (self : Lake.Package) :
            Lake.FetchM (Lake.BuildJob Unit)

            Fetch the build job of a library facet.

            Instances For

              Module Facets #

              source
              @[inline]
              def Lake.ModuleFacetDecl.fetch {α : Type} (mod : Lake.Module) (self : Lake.ModuleFacetDecl) [Lake.FamilyOut Lake.ModuleData self.name α] :
              Lake.FetchM α

              Fetch the build result of a module facet.

              Equations
              Instances For
                source
                def Lake.ModuleFacetConfig.fetchJob {name : Lean.Name} (mod : Lake.Module) (self : Lake.ModuleFacetConfig name) :
                Lake.FetchM (Lake.BuildJob Unit)

                Fetch the build job of a module facet.

                Instances For
                  source
                  def Lake.Module.fetchFacetJob (name : Lean.Name) (self : Lake.Module) :
                  Lake.FetchM (Lake.BuildJob Unit)

                  Fetch the build job of a module facet.

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

                    Lean Library Facets #

                    source
                    @[inline]
                    def Lake.LeanLibConfig.get {m : Type → Type u_1} (self : Lake.LeanLibConfig) [Monad m] [Lake.MonadError m] [Lake.MonadLake m] :
                    m Lake.LeanLib

                    Get the Lean library in the workspace with the configuration's name.

                    Instances For
                      source
                      @[inline]
                      def Lake.LibraryFacetDecl.fetch {α : Type} (lib : Lake.LeanLib) (self : Lake.LibraryFacetDecl) [Lake.FamilyOut Lake.LibraryData self.name α] :
                      Lake.FetchM α

                      Fetch the build result of a library facet.

                      Instances For
                        source
                        def Lake.LibraryFacetConfig.fetchJob {name : Lean.Name} (lib : Lake.LeanLib) (self : Lake.LibraryFacetConfig name) :
                        Lake.FetchM (Lake.BuildJob Unit)

                        Fetch the build job of a library facet.

                        Instances For
                          source
                          def Lake.LeanLib.fetchFacetJob (name : Lean.Name) (self : Lake.LeanLib) :
                          Lake.FetchM (Lake.BuildJob Unit)

                          Fetch the build job of a library facet.

                          Instances For

                            Lean Executable Target #

                            source
                            @[inline]
                            def Lake.LeanExeConfig.get {m : Type → Type u_1} (self : Lake.LeanExeConfig) [Monad m] [Lake.MonadError m] [Lake.MonadLake m] :
                            m Lake.LeanExe

                            Get the Lean executable in the workspace with the configuration's name.

                            Instances For
                              source
                              @[inline]
                              def Lake.LeanExeConfig.fetch (self : Lake.LeanExeConfig) :
                              Lake.FetchM (Lake.BuildJob System.FilePath)

                              Fetch the build of the Lean executable.

                              Equations
                              • self.fetch = do let __do_lift ← self.get __do_lift.exe.fetch
                              Instances For
                                source
                                @[inline]
                                def Lake.LeanExe.fetch (self : Lake.LeanExe) :
                                Lake.FetchM (Lake.BuildJob System.FilePath)

                                Fetch the build of the Lean executable.

                                Equations
                                • self.fetch = self.exe.fetch
                                Instances For