Documentation

Lake.Config.Defaults

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

Equations
Instances For

    The default setting for a WorkspaceConfig's packagesDir option.

    Equations
    Instances For

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

      Equations
      Instances For

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

        Equations
        Instances For

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

          Equations
          Instances For

            The default Lean library directory for packages.

            Equations
            Instances For

              The default native library directory for packages.

              Equations
              Instances For

                The default binary directory for packages.

                Equations
                Instances For

                  The default IR directory for packages.

                  Equations
                  Instances For