Documentation

Lake.Config.Package

structure Lake.Package :

A Lake package -- its location plus its configuration.

  • name : Lean.Name

    The name of the package.

  • The absolute path to the package's directory.

  • The path to the package's directory relative to the workspace.

  • config : PackageConfig self.name

    The package's user-defined configuration.

  • configFile : System.FilePath

    The absolute path to the package's configuration file.

  • relConfigFile : System.FilePath

    The path to the package's configuration file (relative to dir).

  • relManifestFile : System.FilePath

    The path to the package's JSON manifest of remote dependencies (relative to dir).

  • scope : String

    The package's scope (e.g., in Reservoir).

  • remoteUrl : String

    The URL to this package's Git remote.

  • depConfigs : Array Dependency

    Dependency configurations for the package.

  • targetDecls : Array (PConfigDecl self.name)

    Target configurations in the order declared by the package.

  • targetDeclMap : DNameMap (NConfigDecl self.name)

    Name-declaration map of target configurations in the package.

  • defaultTargets : Array Lean.Name

    The names of the package's targets to build by default (i.e., on a bare lake build of the package).

  • Scripts for the package.

  • defaultScripts : Array Script

    The names of the package's scripts run by default (i.e., on a bare lake run of the package).

  • postUpdateHooks : Array (OpaquePostUpdateHook self.name)

    Post-lake update hooks for the package.

  • buildArchive : String

    The package's buildArchive/buildArchive? configuration.

  • testDriver : String

    The driver used for lake test when this package is the workspace root.

  • lintDriver : String

    The driver used for lake lint when this package is the workspace root.

  • cacheRef? : Option CacheRef

    Input-to-content map for hashes of package artifacts. If none, the artifact cache is disabled for the package.

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      @[reducible, inline]
      Equations
      Instances For
        @[reducible, inline]
        Equations
        Instances For
          Equations
          @[reducible, inline]
          abbrev Lake.PostUpdateFn (pkgName : Lean.Name) :

          The type of a post-update hooks monad. IO equipped with logging ability and information about the Lake configuration.

          Equations
          Instances For
            structure Lake.PostUpdateHook (pkgName : Lean.Name) :
            Instances For
              @[implemented_by _private.Lake.Config.Package.0.Lake.OpaquePostUpdateHook.unsafeGet]
              @[implemented_by _private.Lake.Config.Package.0.Lake.OpaquePostUpdateHook.unsafeMk]
              Instances For
                @[inline]

                For internal use. Whether this package is Lean itself.

                Equations
                Instances For
                  @[inline]

                  The package version.

                  Equations
                  Instances For
                    @[inline]

                    The package's versionTags configuration.

                    Equations
                    Instances For
                      @[inline]

                      The package's description configuration.

                      Equations
                      Instances For
                        @[inline]

                        The package's keywords configuration.

                        Equations
                        Instances For
                          @[inline]

                          The package's homepage configuration.

                          Equations
                          Instances For
                            @[inline]

                            The package's reservoir configuration.

                            Equations
                            Instances For
                              @[inline]

                              The package's license configuration.

                              Equations
                              Instances For
                                @[inline]

                                The package's licenseFiles configuration.

                                Equations
                                Instances For
                                  @[inline]

                                  The package's dir joined with each of its relLicenseFiles.

                                  Equations
                                  Instances For
                                    @[inline]

                                    The package's readmeFile configuration.

                                    Equations
                                    Instances For
                                      @[inline]

                                      The package's dir joined with its relReadmeFile.

                                      Equations
                                      Instances For
                                        @[inline]

                                        The path to the package's Lake directory relative to dir (e.g., .lake).

                                        Equations
                                        Instances For
                                          @[inline]

                                          The full path to the package's Lake directory (i.e, dir joined with relLakeDir).

                                          Equations
                                          Instances For
                                            @[inline]

                                            The path for storing the package's remote dependencies relative to dir (i.e., packagesDir).

                                            Equations
                                            Instances For
                                              @[inline]

                                              The package's dir joined with its relPkgsDir.

                                              Equations
                                              Instances For
                                                @[inline]

                                                The path to the package's JSON manifest of remote dependencies.

                                                Equations
                                                Instances For
                                                  @[inline]

                                                  The package's dir joined with its buildDir configuration.

                                                  Equations
                                                  Instances For
                                                    @[inline]

                                                    The package's testDriverArgs configuration.

                                                    Equations
                                                    Instances For
                                                      @[inline]

                                                      The package's lintDriverArgs configuration.

                                                      Equations
                                                      Instances For
                                                        @[inline]

                                                        The package's extraDepTargets configuration.

                                                        Equations
                                                        Instances For
                                                          @[inline]

                                                          The package's platformIndependent configuration.

                                                          Equations
                                                          Instances For
                                                            @[inline]

                                                            The package's releaseRepo/releaseRepo? configuration.

                                                            Equations
                                                            Instances For
                                                              @[inline]

                                                              The packages remoteUrl as an Option (none if empty).

                                                              Equations
                                                              Instances For
                                                                @[inline]

                                                                The package's lakeDir joined with its buildArchive.

                                                                Equations
                                                                Instances For
                                                                  @[inline]

                                                                  The path where Lake stores the package's barrel (downloaded from Reservoir).

                                                                  Equations
                                                                  Instances For
                                                                    @[inline]

                                                                    The package's preferReleaseBuild configuration.

                                                                    Equations
                                                                    Instances For
                                                                      @[inline]

                                                                      The package's precompileModules configuration.

                                                                      Equations
                                                                      Instances For
                                                                        @[inline]

                                                                        The package's moreGlobalServerArgs configuration.

                                                                        Equations
                                                                        Instances For
                                                                          @[inline]

                                                                          The package's moreServerOptions configuration appended to its leanOptions configuration.

                                                                          Equations
                                                                          Instances For
                                                                            @[inline]

                                                                            The package's buildType configuration.

                                                                            Equations
                                                                            Instances For
                                                                              @[inline]

                                                                              The package's backend configuration.

                                                                              Equations
                                                                              Instances For
                                                                                @[inline]

                                                                                The package's dynlibs configuration.

                                                                                Equations
                                                                                Instances For
                                                                                  @[inline]

                                                                                  The package's plugins configuration.

                                                                                  Equations
                                                                                  Instances For
                                                                                    @[inline]

                                                                                    The package's leanOptions configuration.

                                                                                    Equations
                                                                                    Instances For
                                                                                      @[inline]

                                                                                      The package's moreLeanArgs configuration.

                                                                                      Equations
                                                                                      Instances For
                                                                                        @[inline]

                                                                                        The package's weakLeanArgs configuration.

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[inline]

                                                                                          The package's moreLeancArgs configuration.

                                                                                          Equations
                                                                                          Instances For
                                                                                            @[inline]

                                                                                            The package's weakLeancArgs configuration.

                                                                                            Equations
                                                                                            Instances For
                                                                                              @[inline]

                                                                                              The package's moreLinkObjs configuration.

                                                                                              Equations
                                                                                              Instances For
                                                                                                @[inline]

                                                                                                The package's moreLinkLibs configuration.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[inline]

                                                                                                  The package's moreLinkArgs configuration.

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    @[inline]

                                                                                                    The package's weakLinkArgs configuration.

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      @[inline]

                                                                                                      The package's dir joined with its srcDir configuration.

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[inline]

                                                                                                        The package's root directory for lean (i.e., srcDir).

                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          @[inline]

                                                                                                          The package's buildDir joined with its leanLibDir configuration.

                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            @[inline]

                                                                                                            Where static libraries for the package are located. The package's buildDir joined with its nativeLibDir configuration.

                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              @[inline]

                                                                                                              Where shared libraries for the package are located. The package's buildDir joined with its nativeLibDir configuration.

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[inline, deprecated "Use staticLibDir or sharedLibDir instead." (since := "2025-03-29")]

                                                                                                                The package's buildDir joined with its nativeLibDir configuration.

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[inline]

                                                                                                                  The package's buildDir joined with its binDir configuration.

                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    @[inline]

                                                                                                                    The package's buildDir joined with its irDir configuration.

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      @[inline]

                                                                                                                      The package's libPrefixOnWindows configuration.

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        @[inline]

                                                                                                                        The package's enableArtifactCache? configuration.

                                                                                                                        Equations
                                                                                                                        Instances For

                                                                                                                          The file where the package's input-to-content mapping is stored in the Lake cache.

                                                                                                                          Equations
                                                                                                                          Instances For

                                                                                                                            Try to find a target configuration in the package with the given name.

                                                                                                                            Equations
                                                                                                                            Instances For

                                                                                                                              Whether the given module is considered local to the package.

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

                                                                                                                                Whether the given module is in the package (i.e., can build it).

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

                                                                                                                                  Remove the package's build outputs (i.e., delete its build directory).

                                                                                                                                  Equations
                                                                                                                                  Instances For