Extends Lean's incremental reporting and reuse between commands into
various steps inside declarations:
* headers and bodies of each (mutual) definition/theorem
* `theorem ... := by` for each contained tactic step, including
recursively inside supported combinators currently consisting of
* `·` (cdot), `case`, `next`
* `induction`, `cases`
* macros such as `next` unfolding to the above
*Incremental reuse* means not recomputing any such steps if they are not
affected by a document change. *Incremental reporting* includes the
parts seen in the recording above: the progress bar and messages. Other
language server features such as hover etc. are *not yet* supported
incrementally, i.e. they are shown only when the declaration has been
fully processed as before.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
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 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.
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 adds a `test_extern` command.
Usage:
```
import Lean.Util.TestExtern
test_extern Nat.add 17 37
```
This:
* Checks that the head symbol has an `@[extern]` attribute.
* Writes down `t == t'`, where `t` is the term provided, and `t'` is the
reference implementation (specifically, `t` with the head symbol
unfolded).
* Tries to reduce this to `true`, and complains if this fails.
Note that the type of the term must have a `BEq` instance for this to
work: there's a self-explanatory error message if it isn't available.
