Lake will now update a package's `lean-toolchain` file on `lake update`
if it finds the package's direct dependencies use a newer compatible
toolchain. To skip this step, use the `--keep-toolchain` CLI option.
Closes#2582. Closes#2752. Closes#5615.
### Toolchain update details
To determine "newest compatible" toolchain, Lake parses the toolchain
listed in the packages' `lean-toolchain` files into four categories:
release , nightly, PR, and other. For newness, release toolchains are
compared by semantic version (e.g., `"v4.4.0" < "v4.8.0"` and
`"v4.6.0-rc1" < "v4.6.0"`) and nightlies are compared by date (e.g.,
`"nightly-2024-01-10" < "nightly-2014-10-01"`). All other toolchain
types and mixtures are incompatible. If there is not a single newest
toolchain, Lake will print a warning and continue updating without
changing the toolchain.
If Lake does find a new toolchain, Lake updates the workspace's
`lean-toolchain` file accordingly and restarts the update process on the
new Lake. If Elan is detected, it will spawn the new Lake process via
`elan run` with the same arguments Lake was initially run with. If Elan
is missing, it will prompt the user to restart Lake manually and exit
with a special error code (4).
### Other changes
To implement this new logic, various other refactors were needed. Here
are some key highlights:
* Logs emitted during package and workspace loading are now eagerly
printed.
* The Elan executable used by Lake is now configurable by the `ELAN`
environment variable.
* The `--lean` CLI option was removed. Use the `LEAN` environment
variable instead.
* `Package.deps` / `Package.opaqueDeps` have been removed. Use
`findPackage?` with a dependency's name instead.
* The dependency resolver now uses a pure breadth-first traversal to
resolve dependencies. It also resolves dependencies in reverse order,
which is done for consistency with targets. Latter targets shadow
earlier ones and latter dependencies take precedence over earlier ones.
**These changes mean the order of dependencies in a Lake manifest will
change after the first `lake update` on this version of Lake.**
Following up #5928, updates the syntax for `omega` and `solve_by_elim`
and restores the syntax quotations in their implementations.
Following up #5898, uses the new tactic syntax in the library, replacing
all uses of `(config := ...)`.
Adds an optional `text` argument to the `fetchFile*` and `buildFile*`
definitions that can be used to hash built files as text files (with
normalized line endings) instead of as binary files (the previous
default).
Separately, this change also significantly expands the documentation in
the `Lake.Build.Trace` module and preforms minor touchups of some build
job signatures.
I'd previously added an instance from `ForIn'` to `ForIn`, but this then
caused some non-defeq duplication. It seems fine to just remove the
concrete `ForIn` instances in cases where the `ForIn'` instance exists
too. We can even remove a number of type-specific lemmas in favour of
the general ones.
Fixes a serious issue where Lake would delete path dependencies when
attempting to cleanup a dependency required with an incorrect name.
Closes#5876. Originally part of #5684, but also independently
discovered by François.
Makes `MessageData.ofConstName` available without needing to import the
pretty printer. Any code making use of `MessageData` can write `m!" ...
{.ofConstName n} ... "` to have the name print with hover information.
More error messages now have hover information.
* Now `.ofConstName` also has a boolean flag to make names print fully
qualified. Default: false.
* Now `.ofConstName` will sanitize names that aren't constants. It is OK
to use it in `"unknown constant '{.ofConstName constName}'"` errors.
Usability note: it is more user-friendly to have "has already been
declared" errors report the fully qualified name. For this, write
`m!"{.ofConstName n true} has already been declared"`.
An important part of the interface of a function is the parameter names,
for making used of named arguments. This PR makes the parameter names
print in a reliable way. The parameters of the type now appear as
hygienic names if they cannot be used as named arguments.
Modifies the heuristic for how parameters are chosen to appear before or
after the colon. The rule is now that parameters start appearing after
the colon at the first non-dependent non-instance-implicit parameter
that has a name unusable as a named argument. This is a refinement of
#2846.
Fixes the issue where consecutive hygienic names pretty print without a
space separating them, so we now have `(x✝ y✝ : Nat)` rather than `(x✝y✝
: Nat)`.
Breaking change: `Lean.PrettyPrinter.Formatter.pushToken` now takes an
additional boolean `ident` argument, which should be `true` for
identifiers. Used to insert discretionary space between consecutive
identifiers.
Closes#5810
This replaces `export Lean (Name NameMap)` and `export System
(SearchPath FilePath)` with the relevant `open` commands. This fixes
docgen output so that it can refer to, for example, `Lean.Name` instead
of `Lake.Name`.
The reason for these `export`s was convenience: by doing `open Lake` you
could get these aliases for free. However, aliases affect pretty
printing, and the Lake aliases took precedence. We don't want to disable
pretty printing re-exported names because this can be a valid pattern
(names could incrementally get re-exported from namespace to parent
namespace).
In the future we might implement a feature to be able to `scoped open`
some names.
Breaking change: Lakefiles that refer to `FilePath` may need to change
this to `System.FilePath` or otherwise add `open System (FilePath)`.
Closes#2524
I made a few choices so far that can probably be discussed:
- got rid of `modn` on `UInt`, nobody seems to use it apart from the
definition of `shift` which can use normal `mod`
- removed the previous defeq optimized definition of `USize.size` in
favor for a normal one. The motivation was to allow `OfNat` to work
which doesn't seem to be necessary anymore afaict.
- Minimized uses of `.val`, should we maybe mark it deprecated?
- Mostly got rid of `.val` in basically all theorems as the proper next
level of API would now be `.toBitVec`. We could probably re-prove them
but it would be more annoying given the change of definition.
- Did not yet redefine `log2` in terms of `BitVec` as this would require
a `log2` in `BitVec` as well, do we want this?
- I added a couple of theorems around the relation of `<` on `UInt` and
`Nat`. These were previously not needed because defeq was used all over
the place to save us. I did not yet generalize these to all types as I
wasn't sure if they are the appropriate lemma that we want to have.
Lake will now only automatically fetch Reservoir build caches for
package in the the `leanprover` and `leanprover-community`
organizations. We are not planning to expand the Reservoir build cache
to other packages until farther in the future.
A Lake build of target within a a package will no longer build a
package's dependencies package-level extra targets dependencies. At the
technical level, a package's `extraDep` facet no longer transitively
builds its dependencies' `extraDep` facet.
Closes#5633.
Lake no longer attempts to fetch the Reservoir build cache if the build
directory is already present. Plus, failure of the automatic fetch now
only produces a trace message, not a warning.
Lake no longer attempts to fetch Reservoir build caches (barrels) for
non-Reservoir dependencies, and it will only fetch them for Reservoir
dependencies in the presence of a known toolchain.
Also, optional build job failures are now only displayed in verbose
mode.
Adds Reservoir as another possible source of build caches in addition to
GitHub releases. If a GitHub release is not configured for a Reservoir
dependency, it will attempt download a build cache from Reservoir. Like
with GitHub releases, failure will not stop the build and instead issue
a warning. Many of the Lake API calls related to these build caches were
refactored and renamed, with the old names remaining around as
deprecated aliases.
Build cache downloads (from Reservoir or GitHub) can now be disabled via
the `--no-cache` CLI option or the `LAKE_NO_CACHE` environment variable.
A disabled cache can be re-enable with the `--try-cache` CLI option.
Adds additional fields to the package configuration which will be used
by Reservoir:
* `version`: The version of the package. Follows Lean's model of
`<major>.<minor>.<patch>[-<specialDescr>]`.
* `versionTags`: A pattern matching the set of Git tags Reservoir should
consider package version revisions.
* `description`: A short description for the package. Takes precedence
over the GitHub's description.
* `keywords`: An array of package keywords that will be used to group
packages into categories on Reservoir. Takes precedence over labels on
the repository.
* `homepage`: A URL to a website for the package. Takes precedence over
GitHub's homepage.
* `license`: An SPFX license identifier for the package's license (not
verified to be well-formed).
* `licenseFiles`: An array of (relative) files the contain license
information (e.g., `#["LICENSE", "NOTICE"]` for Apache 2.0).
* `readmeFile`: Relative path to the package's readme (enables
non-standard README locations).
* `reservoir`: Reservoir will use this setting to determine whether to
include packages in its index.
Also adds two new CLI commands:
* `lake reservoir-config`: Used by Reservoir to extract a package's
configuration.
* `lake check-build`: Determines whether the package has any default
build targets configured.
The Reservoir configuration also makes uses of the exiting `name` and
`platformIndependent` fields.
`simp only` will not apply this simproc anymore. Users must now write
`simp only [reduceCtorEq]`. See RFC #5046 for motivation.
This PR also renames simproc to `reduceCtorEq`.
close#5046
@semorrison A few `simp only ...` tactics will probably break in
Mathlib. Fix: include `reduceCtorEq`.
This restores all of the imports of `Lean.Data.HashMap` and
`Lean.Data.HashSet` so that users actually see the deprecation warnings
instead of a "declaration not found" error.
This PR resolves two language server bugs that especially affect Windows
users:
1. Editing the header could result in the watchdog not correctly
restarting the file worker (#3786, #3787), which would lead to the file
seemingly being processed forever.
- The cause of this issue was a race condition in the watchdog that was
accidentally introduced as far back as #1884: In specific circumstances,
the watchdog will attempt forwarding a message to the file worker after
the process has exited due to a changed header, but before the file
worker exiting has been noticed by the watchdog (which will then restart
the file worker). In this case, the watchdog would mark the file worker
as having crashed and not look at its exit code to restart the file
worker, but instead treat it like a crashed file worker that will only
be restarted when editing the file again. Not inspecting the exit code
of the file worker when it crashed from forwarding a message from the
file worker is necessary since we do not restart the file worker until
another notification from the client arrives, and so we would read the
same crash exit code over and over again in the main loop of the
watchdog if we did not remove it from our list of file workers that we
listen to.
- This PR resolves this issue by distinguishing between "crashes when
forwarding messages to the file worker" and "crashes when forwarding
messages from the file worker". In the former case, we still inspect the
exit code of the file worker and potentially restart it if the imports
changed, whereas in the latter case, we stop inspecting the exit code of
the file worker. This is correct because the latter case is exactly the
one where we need to stop inspecting the exit code but where a crash
cannot occur as a result of a changed header, whereas the former case is
exactly the one where we still need to inspect the exit code after a
crash to ensure that we restart the file worker in case it exited
because the header changed.
- At some point in the future, it would be nice to revamp the
concurrency model of the watchdog entirely now that we have all those
fancy concurrency primitives that were not available four years ago when
the watchdog was first written.
2. On an especially slow Windows machine, we found that starting the
language server would sometimes not succeed at all because reading from
the stdin pipe in the watchdog produced an EINVAL error, which was in
turn caused by an NT "pipe empty" error.
- After lots of debugging, @Kha found that Lake accidentally passes its
stdin to Git because it does not explicitly set the `stdin` field to
`null` when spawning the process.
- Changing this fixes the issue, which suggests that Git may mutate the
pipe we pass to it to be non-blocking, which then causes a "pipe empty"
error in the watchdog when we also attempt to read from that same pipe.
- I'm still very uncertain why we only saw this issue on one
particularly slow machine and not across the whole eco system.
This PR also resolves an issue where we would not correctly emit
messages that we received while the file worker is being restarted to
the corresponding file worker after the restart.
Closes#3786, closes#3787.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Adds the `--log-level=<lv>` CLI option for controlling the minimum log
level Lake should output. For instance, `--log-level=error` will only
print errors (not warnings or info).
Also, adds the parallel `--fail-level` CLI option to control what the
minimum log level of build failures is. The existing `--iofail` and
`--wfail` options are equivalent to `--fail-level=info` and
`--fail-level=warning` , respectively.
Closes#4805,
Draft of adding ci workflow using lean-action on `lake new/init`
This PR is currently missing lake options for the user to control this
feature.
Closes#4606
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Improves a number of elements related to Git checkouts, cloud releases,
and related error handling.
* On error, Lake now prints all top-level logs. Top-level logs are those
produced by Lake outside of the job monitor (e.g., when cloning
dependencies).
* When fetching a remote for a dependency, Lake now forcibly fetches
tags. This prevents potential errors caused by a repository recreating
tags already fetched.
* Tweaked Git error handling to hopefully be more informative.
* The builtin package facets `release`, `optRelease`, `extraDep` are now
caption in the same manner as other facets. Previously, they were
attempting to be too clever.
* `afterReleaseSync` and `afterReleaseAsync` now fetch `optRelease`
rather than `release`.
* Added support for optional jobs, whose failure does not cause the
whole build to failure (and made `optRelease` such a job).
Closes#4302.
Adds syntactic sugar specifying a git revision as a dependency version
in a `require` command. For example:
```
require "leanprover-community" / "proofwidgets" @ git "v0.0.39"
```
Adds a new type of `require` which fetches package metadata from a
registry API endpoint (i.e., Reservoir) and then clones a Git package
using the information provided. To require such a dependency, the new
syntax is:
```lean
require <scope> / <pkg-name> [@ "git#<rev>"] -- e.g., require "leanprover" / "doc-gen4"
```
Or in TOML:
```toml
[[require]]
name = "<pkg-name>"
scope = "<scope>"
rev = "<rev>"
```
Unlike with Git dependencies, Lake can make use of the richer
information provided by the registry to determine the default branch of
the package. This means for repositories of packages like `doc-gen4`
which have a default branch that is not `master`, Lake will now use said
default branch (e.g., in `doc-gen4`'s case, `main`).
Lake also supports configuring the registry endpoint via an environment
variable: `RESERVIOR_API_URL`. Thus, any server providing a similar
interface to Reservoir can be used as the registry. Further
configuration options paralleling those of Cargo's [Alternative
Registries](https://doc.rust-lang.org/cargo/reference/registries.html)
and [Source
Replacement](https://doc.rust-lang.org/cargo/reference/source-replacement.html)
will come in the future.
Updated and split from #3174.
