Add progress option

[keyboardDrummer]

Fixes #5150

Description

Add a --progress option to Dafny, that displays output like the following:

Verified 0/5 symbols. Waiting for Foo to verify.
Verified part 1/3 of Foo, located at line 4, using 8,7E+002 resources
Verified part 2/3 of Foo, located at line 6, using 3,1E+003 resources
Verified part 3/3 of Foo, located at line 7, using 2,8E+003 resources
Verified 1/5 symbols. Waiting for Faz to verify.
Verified part 1/2 of Faz, located at line 10, using 8,7E+002 resources
Verified part 2/2 of Faz, located at line 10, using 3,1E+003 resources
Verified 2/5 symbols. Waiting for Fopple to verify.
Verified part 1/2 of Fopple, located at line 12, using 8,7E+002 resources
Verified part 2/2 of Fopple, located at line 12, using 3,1E+003 resources
Verified 3/5 symbols. Waiting for Burp to verify.
Verified part 1/3 of Burp, located at line 14, using 8,7E+002 resources
Verified part 2/3 of Burp, located at line 16, using 3,1E+003 resources
Verified part 3/3 of Burp, located at line 17, using 2,8E+003 resources
Verified 4/5 symbols. Waiting for Blanc to verify.
Verified part 1/2 of Blanc, located at line 20, using 8,7E+002 resources
Verified part 2/2 of Blanc, located at line 20, using 3,1E+003 resources

Dafny program verifier finished with 12 verified, 0 errors

Note that when --cores is more than 1, which is the default, the output will get more messy because "Verify x/y symbols" will be interspersed with "Verified part a/b of X"

The locations of parts can be confusing, sometimes they point to the header of the symbol being verified, such as when verifying wellformedness of the symbol contract, or correctness when no --isolate-assertions is used. When --isolate-assertions is used, they may also point to lines containing assertions.

How has this been tested?

Add a littish test, progress.dfy

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[atomb]

Thanks for implementing this! I have a couple of very small suggestions.

[atomb]

This seems like it may be locale-specific output, using commas in some locales and decimal points in others, so I imagine this test may fail in CI. Or does the E1 style specify commas?

[keyboardDrummer]

I imagine this test may fail in CI

Is that based on previous experience? Is there a locale difference between the platforms? Seems like it would be better if we avoid this issue for all tests, instead of me adding some feature or test specific fix.

[keyboardDrummer]

Update: changed the feature to ignore the locale

[atomb]

Oh, yeah, that's all I was suggesting: ignoring the locale. :)

[keyboardDrummer]

@atomb, could you help me understand why the line coverage rate for DafnyCore dropped by this PR (below the allowed threshold), even though the new code is being covered by the added littish test?

[atomb]

@atomb, could you help me understand why the line coverage rate for DafnyCore dropped by this PR (below the allowed threshold), even though the new code is being covered by the added littish test?

I noticed this yesterday evening, and I'm similarly mystified. The test you added really should cover every single line of the code you added.

One thing I notice is that it's exactly at the threshold. It says 86% line coverage achieved, and the lower bound is 86%. I'm guessing that it's rounding up from 85.something. It's possible that it was just barely at the threshold before your commit and something like rounding error was enough to make it switch from one side to the other?

[atomb]

One thing I notice is that it's exactly at the threshold. It says 86% line coverage achieved, and the lower bound is 86%. I'm guessing that it's rounding up from 85.something. It's possible that it was just barely at the threshold before your commit and something like rounding error was enough to make it switch from one side to the other?

Yeah, I just did the actual division and it's 85.6%. The last merged PR had test coverage results of 86.4%, with a larger overall numerator but only a very slightly smaller denominator. I have a suspicion that just merging with master may be enough to fix it, so I've just done that.

[keyboardDrummer]

One thing I notice is that it's exactly at the threshold. It says 86% line coverage achieved, and the lower bound is 86%. I'm guessing that it's rounding up from 85.something. It's possible that it was just barely at the threshold before your commit and something like rounding error was enough to make it switch from one side to the other?

Yeah, I just did the actual division and it's 85.6%. The last merged PR had test coverage results of 86.4%, with a larger overall numerator but only a very slightly smaller denominator. I have a suspicion that just merging with master may be enough to fix it, so I've just done that.

That worked, thanks!