Fixes a bug where Lake incorrectly included the module dynlib in a
platform-independent trace. It was incorrectly excluded only external
native libraries from the trace. Also adds a test.
This is the groundwork for a tactic index in generated documentation, as
there was in Lean 3. There are a few challenges to getting this to work
well in Lean 4:
* There's no natural notion of *tactic identity* - a tactic may be
specified by multiple syntax rules (e.g. the pattern-matching version of
`intro` is specified apart from the default version, but both are the
same from a user perspective)
* There's no natural notion of *tactic name* - here, we take the
pragmatic choice of using the first keyword atom in the tactic's syntax
specification, but this may need to be overridable someday.
* Tactics are extensible, but we don't want to allow arbitrary imports
to clobber existing tactic docstrings, which could become unpredictable
in practice.
For tactic identity, this PR introduces the notion of a *tactic
alternative*, which is a `syntax` specification that is really "the same
as" an existing tactic, but needs to be separate for technical reasons.
This provides a notion of tactic identity, which we can use as the basis
of a tactic index in generated documentation. Alternative forms of
tactics are specified using a new `@[tactic_alt IDENT]` attribute,
applied to the new tactic syntax. It is an error to declare a tactic
syntax rule to be an alternative of another one that is itself an
alternative. Documentation hovers now take alternatives into account,
and display the docs for the canonical name.
*Tactic tags*, created with the `register_tactic_tag` command, specify
tags that may be applied to tactics. This is intended to be used by
doc-gen and Verso. Tags may be applied using the `@[tactic_tag TAG1 TAG2
...]` attribute on a canonical tactic parser, which may be used in any
module to facilitate downstream projects introducing tags that apply to
pre-existing tactics. Tags may not be removed, but it's fine to
redundantly add them. The collection of tags, and the tactics to which
they're applied, can be seen using the `#print tactic tags` command.
*Extension documentation* provides a structured way to document
extensions to tactics. The resulting documentation is gathered into a
bulleted list at the bottom of the tactic's docstring. Extensions are
added using the `tactic_extension TAC` command. This can be used when
adding new interpretations of a tactic via `macro_rules`, when extending
some table or search index used by the tactic, or in any other way. It
is a command to facilitate its flexible use with various extension
mechanisms.
The recent change of the trace format exposed some unexpected issues
with Lake's tracing handling. This aims to fix that.
Lake will now perform a rebuild if the trace file is invalid/unreadable.
However, it will still fall back to modification times if the trace file
is missing. Also, Lake is now backwards compatible with the previous
pure numeric traces (and tolerates the absence of a `log` field in the
JSON trace).
Fixes a bug in #4371 where the version of a package used by a dependency
would take precedence over that of a the same package as a direct
dependency if that package had a a manifest. This was because the direct
dependency's manifest entries were added before all the direct
dependencies were visited.
A set of general tweaks of the `require` syntax and docs that provide a
base for #4495.
The sole significant behavioral change is that the `name` field of a
`require` in TOML now falls back to being interpreted as a simple string
name if the value is not a valid Lean identifier. This means that a
require for a package like `doc-gen4` can be written without French
quotes.
This incorporates many general Lake DSL changes from #2439 and adds some
new related changes.
* Rework configuration names (e.g., `package <name>`)
* String literals ca now be used instead of identifiers for names.
* The name syntax is now optional and can instead be set via the `name`
field.
* Avoid French quotes in `lake new` / `lake init` templates (except in
`lean_lib` names). This is not done for `lean_lib` because it needs a
proper identifier for its root. It could use a string and reparse it as
an identifier, but this seems liable to produce confusion.
* The `exe` templates now names it main module `Main` like the `std`
template.
* Improve `math` template error if `lean-toolchain` fails to download.
* Lake now logs a warning rather than an error on unknown configuration
fields. This increases the Lake DSL's cross-version compatibility.
Closes#3385.
Moves the cached log into the trace file (no more `.log.json`). This
means logs are no longer cached on fatal errors and this ensures that an
out-of-date log is not associated with an up-to-date trace. Separately,
`.hash` file generation was changed to be more reliable as well. `.hash`
files are deleted as part of the build and always regenerate with
`--rehash`.
Closes#2751.
Use a TOML file for the Lake configuration of the `src/lake` directory
instead of a Lean file. This avoids having to load a version of the Lake
library to build Lake.
Deprecates `inputFile` and replaces it with `inputBinFile` and
`inputTextFile`. `inputTextFile` normalizes line endings, which helps
ensure text file traces are platform-independent.
Remark: when splitting an `if-then-else` term, the subgoals now have
tags `isTrue` and `isFalse` instead of `inl` and `inr`.
closes#4313
---------
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
The current manner of lifting `LogIO` into `CliM` produces excessive
specializations (due to a nested inlined `forM`). There was also a bug
where `IO` was lifted into `CliM` via `LogIO` rather than directly
through `MainM`.
Stores the dependency trace for a build in the cached build log and then
verifies that it matches the trace of the current build before replaying
the log. Includes test.
Closes#4303.
In `v4.8.0-rc2`, due to additional build refactor changes, `JobM` no
longer cleanly lifts in `FetchM`. Generally, a `JobM` action should not
be run `FetchM` directly but spawned asynchronously as job (e.g., via
`Job.async`). However, there may be some edge cases were this is
necessary and it is a backwards compatibility break, so this change adds
back the lift. This change also includes an `example` definition to
ensure the lift works in order to prevent similar accidental breakages
in the future.
This breakage was first reported by Mario on
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/v4.2E8.2E0-rc2.20discussion/near/440407037).
Switches the manifest format to use `major.minor.patch` semantic
versions. Major version increments indicate breaking changes (e.g., new
required fields and semantic changes to existing fields). Minor version
increments (after `0.x`) indicate backwards-compatible extensions (e.g.,
adding optional fields, removing fields). This change is backwards
compatible. Lake will still successfully read old manifest with numeric
versions. It will treat the numeric version `N` as semantic version
`0.N.0`. Lake will also accept manifest versions with `-` suffixes
(e.g., `x.y.z-foo`) and then ignore the suffix.
This change also includes the general cleanup/refactoring of the
manifest code and data structures that was part of #3174.
Adds two new Lake commands, `lake pack` and `lake unpack`, which pack
and unpack, respectively, Lake build artifacts from an archive. If a
path argument is given, creates the archive specified, otherwise uses
the information in a package's `buildArchive` configuration as the
default.
The pack command will be used by Reservoir to prepare crate-style build
archives for packages. In the future, the command will also be
extensible through configuration file hooks.
Extends the functionality of `lake test` and adds a parallel command in
`lake lint`.
* Rename `@[test_runner]` / `testRunner` to `@[test_driver]` /
`testDriver`. The old names are kept as deprecated aliases.
* Extend help page for `lake test` and adds one for `lake check-test`.
* Add `lake lint` and its parallel tag `@[lint_driver]` , setting
`lintDriver`, and checker `lake check-lint`.
* Add support for specifying test / lint drivers from dependencies.
* Add `testDriverArgs` / `lintDriverArgs` for fixing additional
arguments to the invocation of a driver script or executable.
* Add support for library test drivers (but not library lint drivers).
* `lake check-test` / `lake check-lint` only load the package (without
dependencies), not the whole workspace.
Closes#4116. Closes#4121. Closes#4142.
The type class `MonadStore1` and friends have an outParam, which should
not be an outParam, because there are multiple possible values for this
parameter. At this function
[fetchOrCreate](1382e9fbc4/src/lake/Lake/Load/Main.lean (L196C49-L196C63)),
there are multiple stacked `StateT` monad transformers that each give a
different instance to `MonadStore1`. It is an implementation detail of
type class synthesis which instance is found. This particular type class
synthesis fails when the unused instance
`Lake.instMonadStore1OfMonadDStoreOfFamilyOut` is set to a lower
priority, because then the synthesis order happens to go differently, so
the wrong instance is found.
Replacing the outParam with a semiOutParam solves this issue. Thus, we
make a new type class `MonadStore1Of`, which is the same, but with a
semiOutParam. This follows the design of `MonadState` and
`MonadStateOf`.
However, then it turns out that the instance cannot anymore be
synthesised.
There are two instances for `MonadStore1`:
```
instance [MonadDStore κ β m] : MonadStore1 k (β k) m
instance [MonadDStore κ β m] [FamilyOut β k α] : MonadStore1 k α m
```
The first one is problematic during unification, especially when `β`
should be instantiated as a constant function. We make the second one
sufficient by adding an instance for the general type family:
```
/-- The general type family -/
instance (priority := low) : FamilyDef Fam a (Fam a) where
family_key_eq_type := rfl
```
So then we can get rid of the first instance.
The ANSI mode build monitor now now longer displays built jobs (instead
only those that print info or failed). Also upgrades the progress ticker
with a spinner icon and information on the number of running jobs.
To eliminate parsing differences between Windows and other platforms,
the frontend now normalizes all CRLF line endings to LF, like [in
Rust](https://github.com/rust-lang/rust/issues/62865).
Effects:
- This makes Lake hashes be faithful to what Lean sees (Lake already
normalizes line endings before computing hashes).
- Docstrings now have normalized line endings. In particular, this fixes
`#guard_msgs` failing multiline tests for Windows users using CRLF.
- Now strings don't have different lengths depending on the platform.
Before this PR, the following theorem is true for LF and false for CRLF
files.
```lean
example : "
".length = 1 := rfl
```
Note: the normalization will take `\r\r\n` and turn it into `\r\n`. In
the elaborator, we reject loose `\r`'s that appear in whitespace. Rust
instead takes the approach of making the normalization routine fail.
They do this so that there's no downstream confusion about any `\r\n`
that appears.
Implementation note: the LSP maintains its own copy of a source file
that it updates when edit operations are applied. We are assuming that
edit operations never split or join CRLFs. If this assumption is not
correct, then the LSP copy of a source file can become slightly out of
sync. If this is an issue, there is some discussion
[here](https://github.com/leanprover/lean4/pull/3903#discussion_r1592930085).
Fixes two output bugs with cloud releases: (1) the fetch as part of an
`extraDep` was not properly isolated in a job, and (2) the release job
would be shown even if the release had already been successfully
fetched.
Also includes some related touchups, including the addition of show all
jobs on `-v` which helps with debugging job counts.
Messaged @tydeu about adding a README.md to new lake projects. I decided
to add it with the help of GPT.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
The new Lake build monitor is now more selective, accurate, and prettier
in what it prints.
**Key Changes:**
* Poll jobs at a fixed frequency (100ms), updating the caption and
finished job count.
* Add `action` field to jobs to record information about what jobs do.
It enables distinguishing between jobs which build something, fetch from
a store, or reload logs from the cache.
* At standard verbosity, print build captions only when a job is know to
build or fetch something (i.e., `action >= .fetch`).
* Add an icon and color to job captions based on their log-level / build
status. Also add color to levels in logs.
* Add `--ansi`/`--no-ansi` to toggle Lake's use of ANSI escape codes.
* Fix some `v4.8.0-rc1` bugs and `--old`.
Closes#2822.
This improves job captions, the grouping of logs underneath them, and
the handling of import errors. It also adds a number of log-related
utilities to help achieve this.
**Key Changes:**
* Job captions for facets now include the name of the object (e.g.,
module, library, facet). A caption has also been added to the top-level
build of imports (e.g., for the server and `lake lean`).
* Stray I/O and errors outside the build job in a build function
captioned with `withRegisterJob` (e.g., user-defined targets) will now
be properly grouped under that caption instead of ending up under
"Computing build jobs". Stray I/O will be converted to a single
informational log entry.
* Builds no longer fail immediately on erroneous imports. Lake will now
attempt to recover as best as possible from any import errors.
Information on the import error will appear both in the build of the
erroneous import and in the files which transitive import it. For
example, uf `Lib.B` imports a missing module `Lib.A`, then the build of
`Lib.A` will mention that the file does not exist, and the build of
`Lib.B` will mention the bad import of `Lib.A`.
Closes#3351. Closes#3809.
This makes the `leanArts` in `library_data leanArts : BuildJob Unit` get
a hover for the generated axiom. It also simplifies the `quoteFrom`
function so that it delaborates properly by using a name literal (which
elaborates to `mkStr1`, `mkStr2` etc) instead of a `mkStr` application.
Fixes some bugs with the log refactor (#3835). Namely, quiet mode
progress printing and missing string interpolation in the fetching cloud
release caption.
This is a major refactor of Lake's build code. The key changes:
* **Job Registration**: Significant build jobs are now registered by
build functions. The DSL inserts this registration automatically into
user-defined targets and facets, so this change should require no
end-user adaption. Registered jobs are incrementally awaited by the main
build function and the progress counter now indicates how many of these
jobs are completed and left-to-await. On the positive side, this means
the counter is now always accurate. On the negative side, this means
that jobs are displayed even if they are no-ops (i.e., if the target is
already up-to-date).
* **Log Retention**: Logs are now part of a Lake monad's state instead
of being eagerly printed. As a result, build jobs retain their logs.
Using this change, logs are are now always printed after their
associated caption (e.g., `[X/Y] Building Foo`) and are not arbitrarily
interleaved with the output of other jobs.
* **Simplify the build monad stack**: Previously, there was a lot of
confused mixing between the various build monads in the codebase (i.e.,
`JobM`, `ScedulerM`, `BuildM`, `RecBuildM`, and `IndexBuildM` ). This
refactor attempts to make there use more consistent and straightforward:
* `FetchM` (formerly `IndexBuildM`) is the top-level build monad used by
targets and facets and is now uniformly used in the codebase for all
top-level build functions.
* `JobM` is the monad of asynchronous build jobs. It is more limited
than `FetchM` due to the fact that the build cache can not be modified
asynchronously.
* `SpawnM` (formerly `SchedulerM`) is the monad used to spawn build
jobs. It lifts into `FetchM`.
* `RecBuildM` and `CoreBuildM` (formerly `BuildM`) have been relegated
to internal details of how `FetchM` / `JobM` are implemented / run and
are no longer used outside of that context.
* **Pretty progress.** Build progress (e.g., `[X/Y] Building Foo`) is
now updated on a single line via ANSI escape sequences when Lake is
outputting to a terminal. Redirected Lake output still sees progress on
separate lines.
* **Warnings-as-error option.** Adds a `--wfail` option to Lake that
will cause a build to fail if Lake logs any warnings doing a build.
Unlike some systems, this does not convert warnings into errors and it
does not abort jobs which log warnings. Instead, only the top-level
build fails.
* **Build log cache.** Logs from builds are now cached to a file and
replayed when the build is revisited. For example, this means multiple
runs of a `--wfail` Lean build (without changes) will still produce the
same warnings even though there is now an up-to-date `.olean` for the
module.
Closes#2349. Closes#2764.
Lake now errors instead of warns on a mismatch between a package name
and what is required as. This avoids sometimes confusing downstream
errors. Also, this change provides additional information for errors
that may be caused by the upcoming Std rename.
It currently only reports how many times each declaration has been
unfolded, and how often the `isDefEq` heuristic for `f a =?= f b` has
been used. Only counters above the threshold are reported.
Previously, there was a function `opaque fromUTF8Unchecked : ByteArray
-> String` which would convert a list of bytes into a string, but as the
name implies it does not validate that the string is UTF-8 before doing
so and as a result it produces unsound results in the compiler (because
the lean model of `String` indirectly asserts UTF-8 validity). This PR
replaces that function by
```lean
opaque validateUTF8 (a : @& ByteArray) : Bool
opaque fromUTF8 (a : @& ByteArray) (h : validateUTF8 a) : String
```
so that while the function is still "unchecked", we have a proof witness
that the string is valid. To recover the original, actually unchecked
version, use `lcProof` or other unsafe methods to produce the proof
witness.
Because this was the only `ByteArray -> String` conversion function, it
was used in several places in an unsound way (e.g. reading untrusted
input from IO and treating it as UTF-8). These have been replaced by
`fromUTF8?` or `fromUTF8!` as appropriate.
Adds a `lake lean` CLI command that builds the imports of a Lean file
and then elaborates it via `lean` with the workspace's configuration
(i.e., adding the `moreLeanArgs` / `leanOptions` of the root `package`
and Lake's environment).
Normalize the relative packages directory paths in the pre-rename check
to avoid renames if the difference in paths is only in the path
separators. Also adds a log message on rename.
Adds an alternative TOML configuration format to Lake.
* Uses TOML v1.0.0 and is fully specification compliant (tested via
[toml-test v1.4.0](https://github.com/toml-lang/toml-test/tree/v1.4.0)).
* Supports package configuration options, Lean libraries, Lean
executables, and dependencies.
* TOML configurations can be generated for new projects via `lake
new|init <pkg> <template>.toml`.
* Supported configurations can be converted to/from TOML via `lake
translate-config <lang>`.
This coercion caused difficult-to-diagnose bugs sometimes. Because there
are some situations where converting a string to a name should be done
by parsing the string, and others where it should not, an explicit
choice seems better here.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
On Windows, we now compile all core `.o`s twice, once with and without
`dllexport`, for use in the shipped dynamic and static libraries,
respectively. On other platforms, we export always as before to avoid
the duplicate work.
---------
Co-authored-by: tydeu <tydeu@hatpress.net>
If the `LEAN_GITHASH` environment variable is set, Lake will now use it
instead of the detected Lean's githash when computing traces for builds
and the elaborated Lake configuration. This override allows one to
replace the Lean version used by a library
(e.g., Mathlib) without completely rebuilding it, which is useful for
testing custom builds of Lean.
