Add more information (#5218)

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`

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -11,6 +11,11 @@ public class CommonOptionBag {
 
   public static void EnsureStaticConstructorHasRun() { }
 
+  public static readonly Option<bool> ProgressOption =
+    new("--progress", "While verifying, output information that helps track progress") {
+      IsHidden = true
+    };
+
   public static readonly Option<string> LogLocation =
     new("--log-location", "Sets the directory where to store log files") {
       IsHidden = true
@@ -572,6 +577,7 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
       }
     );
     DooFile.RegisterNoChecksNeeded(
+      ProgressOption,
       LogLocation,
       LogLevelOption,
       ManualTriggerOption,

Source/DafnyCore/Options/DafnyCommands.cs

@@ -25,6 +25,7 @@ static DafnyCommands() {
   }.Concat(ParserOptions);
 
   public static IReadOnlyList<Option> VerificationOptions = new Option[] {
+    CommonOptionBag.ProgressOption,
     CommonOptionBag.RelaxDefiniteAssignment,
     BoogieOptionBag.VerificationTimeLimit,
     CommonOptionBag.VerifyIncludedFiles,

Source/DafnyDriver/CliCompilation.cs

@@ -2,6 +2,7 @@
 using System;
 using System.Collections.Concurrent;
 using System.Collections.Generic;
+using System.Globalization;
 using System.IO;
 using System.Linq;
 using System.Text.RegularExpressions;
@@ -162,6 +163,13 @@ public async IAsyncEnumerable<CanVerifyResult> VerifyAllLazily(int? randomSeed)
         var canVerifyResult = canVerifyResults[boogieUpdate.CanVerify];
         canVerifyResult.CompletedParts.Enqueue((boogieUpdate.VerificationTask, completed));
 
+        if (Options.Get(CommonOptionBag.ProgressOption)) {
+          var token = BoogieGenerator.ToDafnyToken(false, boogieUpdate.VerificationTask.Split.Token);
+          Options.OutputWriter.WriteLine(
+            $"Verified part {canVerifyResult.CompletedParts.Count}/{canVerifyResult.Tasks.Count} of {boogieUpdate.CanVerify.FullDafnyName}" +
+            $", on line {token.line} (time: {completed.Result.RunTime.Milliseconds}ms, " +
+            $"resource count: {completed.Result.ResourceCount.ToString("E1", CultureInfo.InvariantCulture)})");
+        }
         if (canVerifyResult.CompletedParts.Count == canVerifyResult.Tasks.Count) {
           canVerifyResult.Finished.TrySetResult();
         }
@@ -198,6 +206,7 @@ public async IAsyncEnumerable<CanVerifyResult> VerifyAllLazily(int? randomSeed)
       }
     }
 
+    int done = 0;
     foreach (var canVerify in orderedCanVerifies) {
       var results = canVerifyResults[canVerify];
       try {
@@ -207,7 +216,11 @@ public async IAsyncEnumerable<CanVerifyResult> VerifyAllLazily(int? randomSeed)
           tasks.Add(Task.Delay(timeLimitSeconds));
         }
 
+        if (Options.Get(CommonOptionBag.ProgressOption)) {
+          await Options.OutputWriter.WriteLineAsync($"Verified {done}/{orderedCanVerifies.Count} symbols. Waiting for {canVerify.FullDafnyName} to verify.");
+        }
         await Task.WhenAny(tasks);
+        done++;
         if (!results.Finished.Task.IsCompleted) {
           Compilation.Reporter.Error(MessageSource.Verifier, canVerify.Tok,
             "Dafny encountered an internal error while waiting for this symbol to verify. Please report it at <https://github.com/dafny-lang/dafny/issues>.\n");

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

@@ -0,0 +1,21 @@
+// RUN: %verify --progress --isolate-assertions --cores=1 %s > %t.raw
+// RUN: %sed 's/time: \d*ms/redacted/g' "%t".raw > %t
+// RUN: %diff "%s.expect" "%t"
+
+method Foo() 
+{
+  assert true;
+  assert true; 
+}
+
+method Faz() ensures true { }
+
+method Fopple() ensures true { }
+
+method Burp() 
+{
+  assert true; 
+  assert true;
+}
+
+method Blanc() ensures true { }

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

@@ -0,0 +1,19 @@
+Verified 0/5 symbols. Waiting for Foo to verify.
+Verified part 1/3 of Foo, on line 5 (redacted, resource count: 8.7E+002)
+Verified part 2/3 of Foo, on line 7 (redacted, resource count: 3.1E+003)
+Verified part 3/3 of Foo, on line 8 (redacted, resource count: 2.8E+003)
+Verified 1/5 symbols. Waiting for Faz to verify.
+Verified part 1/2 of Faz, on line 11 (redacted, resource count: 8.7E+002)
+Verified part 2/2 of Faz, on line 11 (redacted, resource count: 3.1E+003)
+Verified 2/5 symbols. Waiting for Fopple to verify.
+Verified part 1/2 of Fopple, on line 13 (redacted, resource count: 8.7E+002)
+Verified part 2/2 of Fopple, on line 13 (redacted, resource count: 3.1E+003)
+Verified 3/5 symbols. Waiting for Burp to verify.
+Verified part 1/3 of Burp, on line 15 (redacted, resource count: 8.7E+002)
+Verified part 2/3 of Burp, on line 17 (redacted, resource count: 3.1E+003)
+Verified part 3/3 of Burp, on line 18 (redacted, resource count: 2.8E+003)
+Verified 4/5 symbols. Waiting for Blanc to verify.
+Verified part 1/2 of Blanc, on line 21 (redacted, resource count: 8.7E+002)
+Verified part 2/2 of Blanc, on line 21 (redacted, resource count: 3.1E+003)
+
+Dafny program verifier finished with 12 verified, 0 errors

docs/dev/news/5150.feat

@@ -0,0 +1 @@
+Add an option --progress that can be used to track the progress of verification.