Should solver log be written already on -v2 or even -v?

[phadej]

Especially in very long solving situations (like in #7466 ) it might be nice to see that something is happening. -v3 is too verbose to see that solver does something.

[Mikolaj]

How to avoid spamming the console? Is there a succinct version of the solver progress bar? It's probably hard to predict how long the log is going to be and so how much to compress the printout?

[phadej]

Normal people don't use -v2. And it's not the log is not that spammy, at least in addition to what -v2 outputs as well.

I could also look into refactoring logging such that logging "level" can be specified by component, trying to squeeze everything into single number is difficult to balance. (And we end up with isVerboseNoWarn things).

[phadej]

E.g. Agda has benchmark/logs/20110822-09.36-dhcp-190251/polyfunctor:../src/main/dist/build/agda/agda -v0 -v profile:100

Which means don't log anything (-v0) except about everything about profile.

[fgaz]

It's probably hard to predict how long the log is going to be and so how much to compress the printout?

Many tools that don't have a known run time but still have a notion of "step" solve this by just printing a single character (eg. a dot) in unbuffered mode every step, so that the user knows something is happening