feat: lake: build monitor improvements #4127

tydeu · 2024-05-10T21:36:20Z

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.

leanprover-community-mathlib4-bot · 2024-05-11T03:54:16Z

Mathlib CI status (docs):

🟡 Mathlib branch lean-pr-testing-4127 build against this PR was cancelled. (2024-05-11 03:54:15) View Log
🟡 Mathlib branch lean-pr-testing-4127 build against this PR was cancelled. (2024-05-15 00:59:04) View Log
🟡 Mathlib branch lean-pr-testing-4127 build against this PR was cancelled. (2024-05-15 08:10:07) View Log
🟡 Mathlib branch lean-pr-testing-4127 build against this PR was cancelled. (2024-05-15 22:54:13) View Log
🟡 Mathlib branch lean-pr-testing-4127 build against this PR was cancelled. (2024-05-16 04:07:52) View Log
🟡 Mathlib branch lean-pr-testing-4127 build against this PR was cancelled. (2024-05-16 10:07:44) View Log
🟡 Mathlib branch lean-pr-testing-4127 build against this PR was cancelled. (2024-05-16 22:31:42) View Log
🟡 Mathlib branch lean-pr-testing-4127 build against this PR was cancelled. (2024-05-17 01:32:23) View Log
✅ Mathlib branch lean-pr-testing-4127 has successfully built against this PR. (2024-05-17 02:47:37) View Log
✅ Mathlib branch lean-pr-testing-4127 has successfully built against this PR. (2024-05-17 04:22:22) View Log
✅ Mathlib branch lean-pr-testing-4127 has successfully built against this PR. (2024-05-17 06:52:37) View Log
✅ Mathlib branch lean-pr-testing-4127 has successfully built against this PR. (2024-05-17 22:01:51) View Log

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. (cherry picked from commit 7648bf2)

tydeu added the backport releases/v4.8.0 label May 10, 2024

tydeu added this to the v4.8.0-rc2 milestone May 10, 2024

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label May 10, 2024

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 10, 2024

Update lean-toolchain for testing leanprover/lean4#4127

9cb844e

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 10, 2024

Update lean-toolchain for testing leanprover/lean4#4127

2eae1f5

feat: lake: polling build monitor

36554e7

tydeu force-pushed the lake/build-monitor+ branch from e29c178 to 36554e7 Compare May 14, 2024 18:40

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 14, 2024

Trigger CI for leanprover/lean4#4127

4d6b4f5

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 14, 2024

Trigger CI for leanprover/lean4#4127

5d26c42

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 15, 2024

Trigger CI for leanprover/lean4#4127

e9a217b

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 15, 2024

Trigger CI for leanprover/lean4#4127

3a6e80a

chore: ensure jobs have captions & fix fetch release

836e894

tydeu force-pushed the lake/build-monitor+ branch from 644e31b to 836e894 Compare May 15, 2024 16:35

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 15, 2024

Trigger CI for leanprover/lean4#4127

c6ea92f

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 15, 2024

Trigger CI for leanprover/lean4#4127

560aba6

kim-em mentioned this pull request May 15, 2024

[Merged by Bors] - feat: new noisy check leanprover-community/mathlib4#12886

Closed

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 15, 2024

Trigger CI for leanprover/lean4#4127

b9ea65e

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 15, 2024

Trigger CI for leanprover/lean4#4127

c75d080

feat: print jobs with significant builds & prettier progress

58242d8

tydeu force-pushed the lake/build-monitor+ branch from de41c50 to 58242d8 Compare May 16, 2024 03:42

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 16, 2024

Trigger CI for leanprover/lean4#4127

13195cb

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 16, 2024

Trigger CI for leanprover/lean4#4127

a1bfcd2

tydeu force-pushed the lake/build-monitor+ branch from a283417 to d3fef62 Compare May 16, 2024 18:32

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 16, 2024

Trigger CI for leanprover/lean4#4127

c78f28b

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 16, 2024

Trigger CI for leanprover/lean4#4127

50fc572

chore: fix tests & old mode + job actions

abb003d

tydeu force-pushed the lake/build-monitor+ branch from d3fef62 to abb003d Compare May 16, 2024 18:58

feat: CLI ANSI toggle & colored logs

41ff940

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 16, 2024

Trigger CI for leanprover/lean4#4127

086c1aa

refactor: update progress before and after poll

44e398a

tydeu force-pushed the lake/build-monitor+ branch from 87a5e63 to 44e398a Compare May 17, 2024 01:13

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 17, 2024

Trigger CI for leanprover/lean4#4127

9f02a62

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 17, 2024

Trigger CI for leanprover/lean4#4127

9c93d82

refactor: touchup log monad runners

1441313

leanprover-community-mathlib4-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label May 17, 2024

tydeu marked this pull request as ready for review May 17, 2024 02:51

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 17, 2024

Trigger CI for leanprover/lean4#4127

5bd68c3

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 17, 2024

Trigger CI for leanprover/lean4#4127

9112cea

tydeu added the full-ci label May 17, 2024

tydeu force-pushed the lake/build-monitor+ branch from bd02fb6 to 706ab5e Compare May 17, 2024 03:43

chore: fix old test flakiness

5094d0f

tydeu force-pushed the lake/build-monitor+ branch from 706ab5e to 5094d0f Compare May 17, 2024 04:18

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 17, 2024

Trigger CI for leanprover/lean4#4127

9ad1ba7

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 17, 2024

Trigger CI for leanprover/lean4#4127

e444582

tydeu added the will-merge-soon …unless someone speaks up label May 17, 2024

refactor: minor touchups & --iofail

d1e99dc

tydeu force-pushed the lake/build-monitor+ branch from bb2222d to d1e99dc Compare May 17, 2024 20:03

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 17, 2024

Trigger CI for leanprover/lean4#4127

36a6cd3

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 17, 2024

Trigger CI for leanprover/lean4#4127

1c46e70

tydeu added this pull request to the merge queue May 17, 2024

Merged via the queue into leanprover:master with commit 7648bf2 May 18, 2024
22 checks passed

github-actions bot mentioned this pull request May 18, 2024

[Backport releases/v4.8.0] feat: lake: build monitor improvements #4209

Merged

tydeu deleted the lake/build-monitor+ branch May 18, 2024 01:48

tydeu mentioned this pull request May 18, 2024

lake build --require-silence #4195

Closed

tydeu mentioned this pull request May 20, 2024

'Building X' diagnostic for every dependency when processing imports #4069

Closed

1 task

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: lake: build monitor improvements #4127

feat: lake: build monitor improvements #4127

tydeu commented May 10, 2024 •

edited

Loading

leanprover-community-mathlib4-bot commented May 11, 2024 •

edited

Loading

feat: lake: build monitor improvements #4127

feat: lake: build monitor improvements #4127

Conversation

tydeu commented May 10, 2024 • edited Loading

leanprover-community-mathlib4-bot commented May 11, 2024 • edited Loading

tydeu commented May 10, 2024 •

edited

Loading

leanprover-community-mathlib4-bot commented May 11, 2024 •

edited

Loading