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.

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

feat(*): Log progress messages to stderr even when using json output on stdout #495

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

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.

2 participants