Add incremental verification progress reporting in a Dafny-centric way

[atomb]

Summary

I propose adding a --progress flag to the verify command that prints out the status of each verification condition as it is initiated and completed.

This is one of the missing flags cited in #3468.

Background and Motivation

When performing a long-running verification from the command line, it's often useful to see how far along the process is, and identify when Dafny hits a verification condition that takes longer than you expect to verify. In the past, I've usually used the Boogie /trace option for this, but it's poorly-specified and not Dafny-centric. Having a more Dafny-oriented option for tracking progress would be better.

Proposed Feature

When the --progress option is specified, Dafny would print out when each verification run begins and ends, and provide time and resource count statistics for completed runs. I could imagine even having a dynamically updated output showing the status of all runs currently in progress (including runtime up to now), and how many of the total have been either scheduled or completed. Something similar to how cargo shows its build output could make sense. Example output, when running with 2 cores, might be something like:

PASSED   M.F (0.01s, 32498 RU)
PASSED   M.G (0.24s, 98347 RU)
RUNNING  M.Lemma1 (1.20s elapsed)
RUNNING  M.Lemma2 (4.53s elapsed)
[2 proved, 2 in progress, 4 remaining]

Lines like the first two would accumulate as it runs, whereas lines like the last three would be dynamically updated on a regular interval.

Alternatives

A simpler sequence of update lines, similar to /trace but in Dafny terms, without dynamic update, would be slightly simpler to implement.

It's currently possible to use /trace with Dafny, but when running with the new CLI it doesn't actually print out the results of each verification run, only all of the other output /trace provides, which isn't very useful.

[keyboardDrummer]

Thanks for writing this up! This is great.

Can you specify what would be the minimum required to replace the main use-case of /trace for you?

[atomb]

Thanks for writing this up! This is great.

Can you specify what would be the minimum required to replace the main use-case of /trace for you?

I think the static version of what I described, with a line printed when each run is started and another when it's finished, without dynamic update, would be the important thing. (And, I think, even if we had a dynamically updating version, we'd probably want to support the more static version for, e.g., saving to log files. So it probably makes sense to implement that first, and then perhaps make it fancier.)