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

[eric-wieser]

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]

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]

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 https://github.com/leanprover-community/mathlib/pull/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.