Zulip Chat Archive
Stream: general
Topic: Showing progress of mathlib builds
Eric Wieser (Oct 29 2020 at 11:43):
Would it be reasonable for the CI output of mathlib builds to log the file currently being built? It would be nice to have a feel for whether a 1 hour CI run is almost done or only half way there.
Johan Commelin (Oct 29 2020 at 11:53):
With Travis we used to have this. I have no idea whether it is easy to enable this with GH actions
Eric Wieser (Oct 29 2020 at 12:00):
Looks like the issue is that python swallows the output: https://github.com/leanprover-community/mathlib/blob/master/.github/workflows/build.yml#L69
Eric Wieser (Oct 29 2020 at 12:11):
Ah, combined with https://github.com/leanprover-community/lean/blob/d9997024f55dc756d47e2cacd12e8091ae37c9bf/src/shell/lean.cpp#L407
Eric Wieser (Oct 29 2020 at 12:21):
Opened lean#495
Last updated: Dec 20 2023 at 11:08 UTC