Documentation

Lake.Config.Defaults

source
def Lake.defaultLakeDir :
System.FilePath

The default directory to output Lake-related files (e.g., build artifacts, packages, caches, etc.). Currently not configurable.

Instances For
    source
    def Lake.defaultPackagesDir :
    System.FilePath

    The default setting for a WorkspaceConfig's packagesDir option.

    Instances For
      source
      def Lake.defaultConfigFile :
      System.FilePath

      The default name of the Lake configuration file (i.e., lakefile).

      Instances For
        source
        def Lake.defaultLeanConfigFile :
        System.FilePath

        The default name of the Lean Lake configuration file (i.e., lakefile.lean).

        Instances For
          source
          def Lake.defaultTomlConfigFile :
          System.FilePath

          The default name of the TOML Lake configuration file (i.e., lakefile.toml).

          Instances For
            source
            def Lake.defaultManifestFile :
            System.FilePath

            The default name of the Lake manifest file (i.e., lake-manifest.json).

            Instances For
              source
              def Lake.defaultBuildDir :
              System.FilePath

              The default build directory for packages (i.e., .lake/build).

              Instances For
                source
                def Lake.defaultLeanLibDir :
                System.FilePath

                The default Lean library directory for packages.

                Instances For
                  source
                  def Lake.defaultNativeLibDir :
                  System.FilePath

                  The default native library directory for packages.

                  Instances For
                    source
                    def Lake.defaultBinDir :
                    System.FilePath

                    The default binary directory for packages.

                    Instances For
                      source
                      def Lake.defaultIrDir :
                      System.FilePath

                      The default IR directory for packages.

                      Instances For