Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: lake: ANSI monitor: only display progress + running job info #4232

Merged
merged 2 commits into from
May 20, 2024
Merged

feat: lake: ANSI monitor: only display progress + running job info #4232

merged 2 commits into from
May 20, 2024

Conversation

tydeu
Copy link
Member

@tydeu tydeu commented May 20, 2024

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.

@tydeu tydeu added this to the v4.8.0-rc2 milestone May 20, 2024
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label May 20, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 20, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#4232
e74167e
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 20, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#4232
e3baa05
@tydeu tydeu marked this pull request as ready for review May 20, 2024 18:41
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan full-ci labels May 20, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

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

Mathlib CI status (docs):

@tydeu tydeu enabled auto-merge May 20, 2024 19:56
@tydeu tydeu added this pull request to the merge queue May 20, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 20, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4232
f4fe4ed
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 20, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4232
4d3bf07
Merged via the queue into leanprover:master with commit 7ece5d5 May 20, 2024
21 checks passed
github-actions bot pushed a commit that referenced this pull request May 20, 2024
@tydeu @github-actions
feat: lake: ANSI monitor: only display progress + running job info (#…
b4c324e 
…4232)

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.

(cherry picked from commit 7ece5d5)
@github-actions github-actions bot mentioned this pull request May 20, 2024
Merged
tydeu added a commit that referenced this pull request May 20, 2024
@tydeu
feat: lake: ANSI monitor: only display progress + running job info (#…
e7714ec 
…4232)

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.

(cherry picked from commit 7ece5d5)
@tydeu tydeu deleted the lake/quiet-ansi-build branch May 20, 2024 21:59
kim-em pushed a commit that referenced this pull request May 21, 2024
@tydeu @kim-em
feat: lake: ANSI monitor: only display progress + running job info (#…
9ed8572 
…4232)

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.

(cherry picked from commit 7ece5d5)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
backport releases/v4.8.0 breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
v4.8.0-rc2
Development

Successfully merging this pull request may close these issues.
2 participants
@tydeu @leanprover-community-mathlib4-bot