Change the format of output produced by --progress (#5341)

### Description

The previous implementation had two issues:
* It displayed only the milliseconds portion of the duration, so would
be incorrect for any verification lasting longer than a second.
* The use of exponential notation for resource count made it more
difficult to compare values, and impossible to identify small
differences.

This also changes the overall format of the message slightly.

### How has this been tested?

Existing tests have been updated to reflect the changes in formatting.

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

Source/DafnyDriver/CliCompilation.cs

@@ -189,12 +189,12 @@ public class CliCompilation {
  if (Options.Get(CommonOptionBag.ProgressOption)) {
  var token = BoogieGenerator.ToDafnyToken(false, boogieUpdate.VerificationTask.Split.Token);
  var runResult = completed.Result;
- var resourcesUsed = runResult.ResourceCount.ToString("E1", CultureInfo.InvariantCulture);
+ var timeString = runResult.RunTime.ToString("g");
  Options.OutputWriter.WriteLine(
  $"Verification part {canVerifyResult.CompletedParts.Count}/{canVerifyResult.Tasks.Count} of {boogieUpdate.CanVerify.FullDafnyName}" +
  $", on line {token.line}, " +
  $"{DescribeOutcome(Compilation.GetOutcome(runResult.Outcome))}" +
- $", taking {runResult.RunTime.Milliseconds}ms and consuming {resourcesUsed} resources");
+ $" (time: {timeString}, resource count: {runResult.ResourceCount})");
  }
  if (canVerifyResult.CompletedParts.Count == canVerifyResult.Tasks.Count) {
  canVerifyResult.Finished.TrySetResult();
@@ -317,4 +317,4 @@ record VerificationStatistics {
  public int OutOfResourceCount;
  public int OutOfMemoryCount;
  public int SolverExceptionCount;
-}
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/outOfResourceAndIsolateAssertions.check

@@ -0,0 +1,26 @@
+CHECK: Verified 0/2 symbols. Waiting for f to verify.
+CHECK: Verification part 1/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 2/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 3/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 4/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 5/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 6/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 7/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 8/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 9/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 10/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 11/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verified 1/2 symbols. Waiting for L to verify.
+CHECK: Verification part 1/9 of L, on line 7, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 2/9 of L, on line 9, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 3/9 of L, on line 10, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 4/9 of L, on line 10, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 5/9 of L, on line 10, ran out of resources \(time: .*, resource count: .*\)
+CHECK: Verification part 6/9 of L, on line 11, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 7/9 of L, on line 12, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 8/9 of L, on line 12, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 9/9 of L, on line 12, ran out of resources
+outOfResourceAndIsolateAssertions.dfy\(10,18\): Error: Verification out of resource \(L\)
+outOfResourceAndIsolateAssertions.dfy\(12,18\): Error: Verification out of resource \(L\)
+
+Dafny program verifier finished with 18 verified, 0 errors, 2 out of resource

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check

@@ -1,12 +1,12 @@
-// CHECK-L:Verification part 1/3 of Foo, on line 6, verified successfully, redacted and consuming 8.7E+002 resources
-// CHECK-L:Verification part 2/3 of Foo, on line 8, verified successfully, redacted and consuming 3.1E+003 resources
-// CHECK-L:Verification part 3/3 of Foo, on line 9, verified successfully, redacted and consuming 2.8E+003 resources
-// CHECK-L:Verification part 1/2 of Faz, on line 12, verified successfully, redacted and consuming 8.7E+002 resources
-// CHECK-L:Verification part 2/2 of Faz, on line 12, verified successfully, redacted and consuming 3.1E+003 resources
-// CHECK-L:Verification part 1/2 of Fopple, on line 14, verified successfully, redacted and consuming 8.7E+002 resources
-// CHECK-L:Verification part 2/2 of Fopple, on line 14, verified successfully, redacted and consuming 3.1E+003 resources
-// CHECK-L:Verification part 1/3 of Burp, on line 16, verified successfully, redacted and consuming 8.7E+002 resources
-// CHECK-L:Verification part 2/3 of Burp, on line 18, verified successfully, redacted and consuming 3.1E+003 resources
-// CHECK-L:Verification part 3/3 of Burp, on line 19, verified successfully, redacted and consuming 2.8E+003 resources
-// CHECK-L:Verification part 1/2 of Blanc, on line 22, verified successfully, redacted and consuming 8.7E+002 resources
-// CHECK-L:Verification part 2/2 of Blanc, on line 22, verified successfully, redacted and consuming 3.1E+003 resources
+// CHECK:Verification part 1/3 of Foo, on line 6, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 2/3 of Foo, on line 8, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 3/3 of Foo, on line 9, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 1/2 of Faz, on line 12, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 2/2 of Faz, on line 12, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 1/2 of Fopple, on line 14, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 2/2 of Fopple, on line 14, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 1/3 of Burp, on line 16, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 2/3 of Burp, on line 18, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 3/3 of Burp, on line 19, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 1/2 of Blanc, on line 22, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 2/2 of Blanc, on line 22, verified successfully \(time: .*, resource count: .*\)

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy

@@ -1,11 +1,11 @@
-// RUN: %verify --progress --cores=1 %s &> %t.raw
-// RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t
+// RUN: %verify --progress --cores=1 %s &> %t
 // RUN: %OutputCheck --file-to-check "%t" "%s"
-// CHECK-L:Verification part 1/3 of Foo, on line 10, verified successfully, redacted and consuming 8.7E+002 resources
-// CHECK-L:Verification part 2/3 of Foo, on line 11, verified successfully, redacted and consuming 3.1E+003 resources
-// CHECK-L:Verification part 3/3 of Foo, on line 12, verified successfully, redacted and consuming 2.8E+003 resources
-// CHECK-L:Verified 1/2 symbols. Waiting for Bar to verify.
-// CHECK-L:Verification part 1/1 of Bar, on line 15, verified successfully, redacted and consuming 3.1E+003 resources
+// CHECK:Verification part 1/3 of Foo, on line 10, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 2/3 of Foo, on line 11, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 3/3 of Foo, on line 12, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified 1/2 symbols. Waiting for Bar to verify.
+// CHECK:Verification part 1/1 of Bar, on line 15, verified successfully \(time: .*, resource count: .*\)
+
 
 method {:isolate_assertions} Foo() {
  assert true;
@@ -15,4 +15,4 @@ method {:isolate_assertions} Foo() {
 method Bar() {
  assert true;
  assert true;
-}
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy

@@ -1,6 +1,6 @@
-// RUN: ! %verify --isolate-assertions --cores=1 --progress "%s" &> %t.raw
-// RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t
-// RUN: %diff "%s.expect" %t
+// RUN: ! %verify --isolate-assertions --cores=1 --progress "%s" &> "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%S/Inputs/outOfResourceAndIsolateAssertions.check"
+
 
 ghost function f(i:nat, j:nat):int {if i == 0 then 0 else f(i - 1, i * j + 1) + f(i - 1, 2 * i * j)}
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy

@@ -1,8 +1,8 @@
-// RUN: %verify --progress --isolate-assertions --cores=1 %s > %t.raw
-// RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t
+// RUN: %verify --progress --isolate-assertions --cores=1 %s > %t
 // RUN: %OutputCheck --file-to-check %t "%S/Inputs/progressFirstSequence.check"
 // RUN: %OutputCheck --file-to-check %t "%S/Inputs/progressSecondSequence.check"
 
+
 method Foo() 
 {
  assert true;
@@ -19,4 +19,4 @@ method Burp()
  assert true;
 }
 
-method Blanc() ensures true { }
+method Blanc() ensures true { }