refactor: lake: --wfail & track jobs & logs & simplify build monads

[tydeu]

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.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❌ Mathlib branch lean-pr-testing-3835 built against this PR, but lean4checker failed. (2024-04-05 06:16:19) View Log
• ❌ Mathlib branch lean-pr-testing-3835 built against this PR, but lean4checker failed. (2024-04-05 06:46:19) View Log
• 🟡 Mathlib branch lean-pr-testing-3835 build this PR didn't complete normally. (2024-04-05 23:33:11) View Log
• 🟡 Mathlib branch lean-pr-testing-3835 build this PR didn't complete normally. (2024-04-06 01:30:43) View Log
• ❌ Mathlib branch lean-pr-testing-3835 built against this PR, but lean4checker failed. (2024-04-06 03:34:26) View Log
• ❌ Mathlib branch lean-pr-testing-3835 built against this PR, but lean4checker failed. (2024-04-08 18:28:23) View Log
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b6d77be6a5ced7cbd7b6e051047158e7e07bee4e --onto d3e004932c1f5ac3946850692940512d381c7634. (2024-04-18 19:29:16)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b6d77be6a5ced7cbd7b6e051047158e7e07bee4e --onto d6474135baac39a271c301a17d6621691a48b80b. (2024-04-20 00:27:23)
• ❗ Std CI can not be attempted yet, as the nightly-testing-2024-04-19 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Std CI should run now. (2024-04-20 01:38:19)
• 🟡 Mathlib branch lean-pr-testing-3835 build this PR didn't complete normally. (2024-04-29 17:21:29) View Log
• 🟡 Mathlib branch lean-pr-testing-3835 build this PR didn't complete normally. (2024-04-29 18:26:26) View Log
• 🟡 Mathlib branch lean-pr-testing-3835 build this PR didn't complete normally. (2024-04-29 20:08:18) View Log
• 🟡 Mathlib branch lean-pr-testing-3835 build this PR didn't complete normally. (2024-04-29 21:09:59) View Log
• 🟡 Mathlib branch lean-pr-testing-3835 build this PR didn't complete normally. (2024-04-30 01:59:37) View Log

[tydeu]

!bench

[leanprover-bot]

Here are the benchmark results for commit 1c01757.
There were significant changes against commit d988849:

  Benchmark          Metric       Change
  ================================================
+ lake build no-op   task-clock    -9.4% (-17.5 σ)
- stdlib             maxrss        16.9% (871.0 σ)
- stdlib             wall-clock     2.2%  (12.7 σ)

[tydeu]

!bench

[leanprover-bot]

Here are the benchmark results for commit 49d59f9.
There were significant changes against commit 1630d9b:

  Benchmark   Metric   Change
  ======================================
- stdlib      maxrss    16.6% (1092.1 σ)