Skip to content

doc: cover more of lake cache #956

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
tydeu wants to merge 1 commit into
base: main
Choose a base branch
from
+78 −19
Open

doc: cover more of lake cache #956

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .vale/styles/config/ignore/terms.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -244,6 +244,7 @@ unparenthesized
unregister
unregisters
unregistering
untrusted
uploader
upvote
VC
Expand Down
94 changes: 76 additions & 18 deletions Manual/BuildTools/Lake/Cache.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,33 +32,25 @@ Lake's {ref "lake-cache-local"}[local artifact cache] enables reuse of builds wh
The {ref "lake-cache-remote"}[remote artifact cache] expands this to sharing artifact caches across machines. However, it requires the package developers to own cloud storage.
As an alternative for developers without cloud storage but already using GitHub, {ref "lake-github"}[release builds] provide a low-setup way to ship complete builds to users.

# Artifact Caches
# Local Artifact Caches
%%%
tag := "lake-cache-local"
%%%

*This is an experimental feature that is still undergoing development.*

Lake supports a {deftech (key := "local cache")}_local artifact cache_ that stores individual build products, tracking the complete set of inputs that contributed to their final value.
Each {tech}[toolchain] has its own cache because intermediate build products are not compatible between toolchain versions.
By default, each {tech}[toolchain] has its own cache because intermediate build products are usually not compatible between toolchain versions.
However, a toolchain's cache is shared between all local {tech}[workspaces] that use it, so common dependencies don't need to be rebuilt.
If two separate workspaces with the same toolchain depend on the same package, then they can share each others' build products.

Because it is an experimental feature, the local cache is disabled by default.
It is only enabled when the {envVar}`LAKE_ARTIFACT_CACHE` environment variable is set to `true` or when the {tomlField Lake.PackageConfig}`enableArtifactCache` field is set to `true` in the {ref "lake-config"}[configuration file].


# Remote Artifact Caches
%%%
tag := "lake-cache-remote"
%%%

Build products can be retrieved from remote cache servers and placed into the local cache.
This makes it possible to completely avoid local builds.
The {lake}`cache get` command is used to download artifacts into the local cache.

Compared to {ref "lake-github"}[GitHub release builds], the remote artifact cache is much more fine-grained.
It tracks build products at the level of individual source files, {tech}[`.olean` files], and object code, rather than at the level of entire packages.
The location of the Lake cache can be configured with the {envVar}`LAKE_CACHE_DIR` environment variable .

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
The location of the Lake cache can be configured with the {envVar}`LAKE_CACHE_DIR` environment variable .
The location of the Lake cache can be configured with the {envVar}`LAKE_CACHE_DIR` environment variable.

If set to an empty value, Lake will locate the cache in appropriate system location for the OS (e.g., in a `.lake` folder in the home directory or under the `XDG_CACHE_GOME`).

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here "locate" is ambiguous - it can mean "Lake puts the cache in an appropriate location" or "Lake looks for the cache in an appropriate location".

Also, minor language issues:

Suggested change
If set to an empty value, Lake will locate the cache in appropriate system location for the OS (e.g., in a `.lake` folder in the home directory or under the `XDG_CACHE_GOME`).
If set to an empty value, Lake will locate the cache in an appropriate location for the system it's running on (e.g. in a `.lake` directory in the user's home directory or in the location pointed to by {envVar}`XDG_CACHE_HOME`).

When `LAKE_CACHE_DIR` is set, the cache is not toolchain-bound, so it will share build products across toolchains where possible.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
When `LAKE_CACHE_DIR` is set, the cache is not toolchain-bound, so it will share build products across toolchains where possible.
When {envVar}`LAKE_CACHE_DIR` is set, it applies to all {tech}[toolchain versions].
As a result, the cache will share build products across toolchains where possible.

"Where possible" does a lot of work here. Might be good to point out that the Lean compiler itself is part of the trace of most build products, so very few will in practice be shared.

However, since the format of the Lake cache may change between different Lean versions, it is often best to use separate directories per version, or to otherwise ensure only compatible toolchain versions are being used.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How might a user otherwise ensure this? It seems a bit like we're saying "Here's a footgun. Don't pull the trigger. We won't give you a trigger guard - just be creative!".

Can we provide users with a practical way to actually do this?


## Mappings

Expand All @@ -69,17 +61,83 @@ A mappings file tracks a single package within a build, and includes all interme
By default, {lake}`build` saves the workspace's {tech}[root package]'s mappings.
The {lakeOpt}`--package` option selects a different package in the workspace, such as a dependency, saving its mappings instead.
The tracked build products include those that were already up to date and not regenerated, but not the package's targets that the build did not cover.
The {lake}`cache put` command uploads the build products in the mappings file from the local cache to the remote cache.

Lake can bundle a mappings file along with the {tech}[artifacts] it reference into directory via {lake}`cache stage`.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
Lake can bundle a mappings file along with the {tech}[artifacts] it reference into directory via {lake}`cache stage`.
Lake can bundle a mappings file along with the {tech}[artifacts] it references into a single directory via {lake}`cache stage`.

The directory can then be transported to another setup and reinserted into local artifact cache via {lake}`cache unstage`.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
The directory can then be transported to another setup and reinserted into local artifact cache via {lake}`cache unstage`.
The directory can then be inserted into a different local artifact cache via {lake}`cache unstage`.

I think this means the same while being simpler.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(and "reinserted" implies that it was previously present, which I don't think is necessary for the feature)

To better automate the process of transferring cache artifacts between machines, Lake provides builtin support for {tech}[remote cache services].

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
To better automate the process of transferring cache artifacts between machines, Lake provides builtin support for {tech}[remote cache services].
To better automate the process of transferring cache artifacts between machines, Lake supports {tech}[remote cache services].

But I'd actually rewrite it a bit more, like:

Suggested change
To better automate the process of transferring cache artifacts between machines, Lake provides builtin support for {tech}[remote cache services].
Lake's {tech}[remote cache services] automate the process of transferring cache artifacts between machines.


# Remote Artifact Caches
%%%
tag := "lake-cache-remote"
%%%

A {deftech}_remote cache service_ is a cloud storage service that hosts a {deftech}_remote artifact cache_, a store of mappings and artifacts for many package builds.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is "cloud" an important word here? Can I use this with something like an organization's internal server? What about something like Dropbox or NFS/SMB or a shared drive at a university?

What about instead saying something like

Suggested change
A {deftech}_remote cache service_ is a cloud storage service that hosts a {deftech}_remote artifact cache_, a store of mappings and artifacts for many package builds.
A {deftech}_remote cache service_ is a data store that hosts a {deftech}_remote artifact cache_, a store of mappings and artifacts for many package builds.

The {lake}`cache put` command uploads the build products in a {tech}[mappings file] from the local cache to a remote cache, and the {lake}`cache get` command downloads artifacts from the service into the local cache.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The first part of this sentence talks about the local and remote caches, while the second talks about a cache service. If we're making this distinction in the text, then we should be careful about which we mean at each time.

Is this a correction?

Suggested change
The {lake}`cache put` command uploads the build products in a {tech}[mappings file] from the local cache to a remote cache, and the {lake}`cache get` command downloads artifacts from the service into the local cache.
The {lake}`cache put` command uploads the build products in a {tech}[mappings file] from the local cache to a remote cache service, and the {lake}`cache get` command downloads artifacts from the service into the local cache.

Setting up a remote artifact cache subscription to a separate cloud storage service with Amazon S3 interface (e.g., Amazon, Cloudflare), making it more involved than {ref "lake-github"}[GitHub release builds]

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This sentence is not entirely grammatical, and I don't quite get why you want to tell someone that setting something up is hard in the last sentence of a paragraph. Should this move to the next para?


However, compared to GitHub release builds, a remote artifact cache is much more fine-grained.
It tracks build products at the level of individual source files, {tech}[`.olean` files], and object code, rather than at the level of entire packages.
This makes it possible to use the cache _incrementally_, downloading only the parts of the cache necessary to build a particular module or uploading only artifacts which have changed between builds.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this reads better:

Suggested change
This makes it possible to use the cache _incrementally_, downloading only the parts of the cache necessary to build a particular module or uploading only artifacts which have changed between builds.
This makes it possible to use the cache _incrementally_, downloading only the parts of the cache that are necessary to build a particular module and uploading only those artifacts which change between builds.

It is, therefore, more space- and bandwidth-efficient, which is good for large projects which want to serve caches for many different builds.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
It is, therefore, more space- and bandwidth-efficient, which is good for large projects which want to serve caches for many different builds.
It is, therefore, more space- and bandwidth-efficient, which can provide significant cost savings for large projects that want to serve caches for many different builds.

I prefer "that" for restrictive clauses, but "which" isn't wrong


## Configuration

Services providing remote artifact caches are specified in the global Lake configuration file through the `cache` table.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
Services providing remote artifact caches are specified in the global Lake configuration file through the `cache` table.
{tech}[Remote artifact cache services] are specified in the global Lake configuration file's `cache` table.

If we're going to introduce a term, we should use it where it applies, which helps clarity.

Each service is a table in the `cache.service` array of tables.
The set of configured services can be listed through the {lake}`cache services` command.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
The set of configured services can be listed through the {lake}`cache services` command.
The {lake}`cache services` command lists the configured services.


S3 buckets provided by cloud storage services often have separate endpoints for downloads and uploads.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this suitable for everyone who needs to understand it? Do our audience for this section know what endpoints are?

The upload endpoint is usually authenticated whereas the download endpoint is made publicly available.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
The upload endpoint is usually authenticated whereas the download endpoint is made publicly available.
The upload endpoint usually requires authentication whereas the download endpoint is made publicly available.

It's the user who is authenticated by the service. If the service is authenticated that'd mean we checked it's key fingerprint to avoid mitm attacks or something.

In Lake, each set of endpoints is represented as a distinct service.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here we've gone from "endpoint" to "set of endpoints" but I'm pretty sure they refer to the same thing. Can this be consistent?

What about a phrasing like:

Suggested change
In Lake, each set of endpoints is represented as a distinct service.
In Lake, these differently-configured endpoints are configured as if they were separate services.

The default services for {lake}`cache get` and {lake}`cache put` are specified by the `cache.defaultService` and `cache.defaultUploadService` keys, respectively.

:::example "Configuring an S3 Remote Cache Service"
*~/.lake/config.toml*

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should be code font, not boldface. And it would be better to have a sentence here along with a prose description of the meaning of the configuration.

```toml
cache.defaultService = "s3-get"
cache.defaultUploadService = "s3-put"

[[cache.service]]
name = "s3-get"
kind = "s3"
artifactEndpoint = "https://s3-get.com/arts"
revisionEndpoint = "https://s3-get.com/revs"

[[cache.service]]
name = "s3-put"
kind = "s3"
artifactEndpoint = "https://s3-put.com/arts"
revisionEndpoint = "https://s3-put.com/revs"
```
:::

:::paragraph
Remote artifact caches are configured using the following environment variables:
A remote cache service can also be configured for per-command using the following environment variables:

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
A remote cache service can also be configured for per-command using the following environment variables:
A remote cache service can also be configured per command using the following environment variables:

But "command" is a bit ambiguous - are we configuring one for lake build and another for lake query?

What about:

Suggested change
A remote cache service can also be configured for per-command using the following environment variables:
A remote cache service can also be configured using the following environment variables, which take precedence over the configuration file and can modify the behavior of a single invocation of `lake`:

* {envVar}`LAKE_CACHE_KEY`
* {envVar}`LAKE_CACHE_ARTIFACT_ENDPOINT`
* {envVar}`LAKE_CACHE_REVISION_ENDPOINT`
:::

In general, the environment route is only recommended for CI or other workflows without a persistent configuration.
For local use, the global configuration is best.
Comment on lines +121 to +122

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"is recommended" is often a sign of something missing. Why is one thing better than another for most users?

And "route" here is figurative in a context where someone may initially think it's being literal.


## Uploading Builds

When uploading a trusted build, {lake}`cache put` provides the simplest interface.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What does it mean for a build to be trusted? Is this related to the notion of trust in our discussion of e.g. comparator?

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Basically I think this is an important term that really needs a clear definition (or link to one) so different ideas of trust don't end up exposing a user who picks the wrong one to harm.

However, when uploading builds from untrusted sources, it can leak service keys (e.g., caching builds of pull requests).

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This sentence also really needs some explicit definitions. What is an untrusted source? Is it the source file's author who needs to be trusted, the one doing the build, or both? Also, the e.g. doesn't really connect to the sentence unless readers already have significant expertise.

To avoid this, there is a {lake}`cache put-staged` command which uploads a directory produced by {lake}`cache stage`.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
To avoid this, there is a {lake}`cache put-staged` command which uploads a directory produced by {lake}`cache stage`.
The {lake}`cache put-staged` command, which uploads a directory produced by {lake}`cache stage`, can be used to mitigate these risks.

"mitigate" is I think better than "avoid" because it doesn't make readers overconfident

This command does not load a Lake workspace and thus does not run arbitrary code from the package.
However, it requires that build's identifiers (e.g., platform, toolchain, revision) be specified manually.
Comment on lines +129 to +130

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
This command does not load a Lake workspace and thus does not run arbitrary code from the package.
However, it requires that build's identifiers (e.g., platform, toolchain, revision) be specified manually.
This command does not load a Lake workspace and thus does not run arbitrary code from the package.
However, it requires that the build's identifiers (e.g., platform, toolchain, revision) be specified manually.

There's lots of e.g. s in this text. Can any of them become actual complete lists?

How might someone find out what the right identifiers are? I think this could use a little walkthrough

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ohh this is a segue to the next section :-)


## Identifying Builds

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This section should really list the allowed values for the platform and toolchain identifiers in a little table


By default, Lake segregates builds in the remote artifact cache by platform and toolchain (for each package revision).

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is a package revision? Do we have a definition of the term that we can link to?

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

And why not

Suggested change
By default, Lake segregates builds in the remote artifact cache by platform and toolchain (for each package revision).
By default, Lake segregates builds in the remote artifact cache by platform, toolchain, and package revision.

While the results of Lean elaboration are generally cross-platform, they do not have to be, and Lake cannot distinguish between such cases.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
While the results of Lean elaboration are generally cross-platform, they do not have to be, and Lake cannot distinguish between such cases.
While the results of Lean elaboration are generally cross-platform, this is not guaranteed.
For example, an elaborator might generate different terms depending on the user's operating system.
Lake cannot distinguish between platform-dependent and platform-independent code.
Pakages are assumed to package-dependent unless they indicate that ...

(and then on into the next)

Nonetheless, a package can promise Lake that its Lean code does not depend on platform specifics by setting {tomlField Lake.PackageConfig}`platformIndependent` to `true`.
Similarly, a package can set {tomlField Lake.PackageConfig}`fixedToolchain` to `true` to inform Lake that the package only compatible with a single toolchain.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
Similarly, a package can set {tomlField Lake.PackageConfig}`fixedToolchain` to `true` to inform Lake that the package only compatible with a single toolchain.
Similarly, a package can set {tomlField Lake.PackageConfig}`fixedToolchain` to `true` to inform Lake that the package is only compatible with a single {tech}[toolchain version].

Do we have a way to list a few?

With either option, Lake will no longer differentiate builds by that vector and, with both, the package's revision will be sole identifier.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These options respectively cause Lake to stop tracking platforms and toolchain versions for a package, using the same artifacts for this revision of the package on multiple platforms or toolchain versions.

An individual upload or download can also remove this identifiers by setting {lakeOpt}`--platform` or {lakeOpt}`--toolchain` to `none`.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
An individual upload or download can also remove this identifiers by setting {lakeOpt}`--platform` or {lakeOpt}`--toolchain` to `none`.
An individual upload or download can also remove these identifiers by setting {lakeOpt}`--platform` or {lakeOpt}`--toolchain` to `none`.


# GitHub Release Builds
%%%
tag := "lake-github"
Expand All @@ -91,8 +149,8 @@ The {envVar}`LAKE_NO_CACHE` environment variable can be used to disable this fea

## Downloading

To download artifacts, one should configure the package options `releaseRepo` and `buildArchive` to point to the GitHub repository hosting the release and the correct artifact name within it (if the defaults are not sufficient).
Then, set `preferReleaseBuild := true` to tell Lake to fetch and unpack it as an extra package dependency.
To download artifacts, one should configure the package options {tomlField Lake.PackageConfig}`releaseRepo` and {tomlField Lake.PackageConfig}`buildArchive` to point to the GitHub repository hosting the release and the correct artifact name within it (if the defaults are not sufficient).
Then, set {tomlField Lake.PackageConfig}`preferReleaseBuild` to `true` to tell Lake to fetch and unpack it as an extra package dependency.
Comment on lines +152 to +153

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This text suddenly switches from the indicative to the imperative mood, and the paragraph after switches back. This was also a problem with the text it's replacing, but it would be nice to clean it up while we're at it.

@david-christiansen david-christiansen Sep 29, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's also unclear to me where I should set preferReleaseBuild - is this on the package being cached or on the dependency that wants its own build to use the cache? Why isn't this user config instead?


Lake will only fetch release builds as part of its standard build process if the package wanting it is a dependency (as the root package is expected to modified and thus not often compatible with this scheme).
However, should one wish to fetch a release for a root package (e.g., after cloning the release's source but before editing), one can manually do so via `lake build :release`.
Expand Down
2 changes: 1 addition & 1 deletion Manual/BuildTools/Lake/Config.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@ These options control the top-level directory layout of the package and its buil
Further paths specified by libraries, executables, and targets within the package are relative to these directories.
:::

:::tomlFieldCategory "Building and Running" defaultTargets leanLibDir platformIndependent precompileModules precompileImports moreServerOptions moreGlobalServerArgs buildType leanOptions moreLeanArgs weakLeanArgs moreLeancArgs weakLeancArgs moreLinkArgs weakLinkArgs extraDepTargets
:::tomlFieldCategory "Building and Running" defaultTargets platformIndependent fixedToolchain enableArtifactCache restoreAllArtifacts precompileModules precompileImports moreServerOptions moreGlobalServerArgs buildType leanOptions moreLeanArgs weakLeanArgs moreLeancArgs weakLeancArgs moreLinkArgs weakLinkArgs extraDepTargets

These options configure how code is built and run in the package.
Libraries, executables, and other {tech}[targets] within a package can further add to parts of this configuration.
Expand Down
Loading