Skip to content

Conversation

@eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Oct 29, 2020

I haven't actually tested this, but it seems plausible that it would work.

Motivated by https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Showing.20progress.20of.20mathlib.20builds/near/214955317

@gebner
Copy link
Member

gebner commented Oct 29, 2020

Does this actually help us with mathlib CI? Does this produce too much output for the CI log? Should it rather print progress messages as JSON, so that we can postprocess them (more easily)?

@eric-wieser
Copy link
Member Author

eric-wieser commented Oct 29, 2020

Does this actually help us with mathlib CI?

What's the easiest way to find out? Can I make a mathlib PR pointing lean to this branch?

Edit: Done in leanprover-community/mathlib3#4817 I think Nope, I need a tag

Does this produce too much output for the CI log? Should it rather print progress messages as JSON, so that we can postprocess them (more easily)?

That's probably a good idea, especially if this approach overloads the CI log. It was more work though since I'd need to modify the python script in mathlib too, and I figured this might be good enough.

eric-wieser added a commit to leanprover-community/mathlib3 that referenced this pull request Oct 29, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants