Update documentation

dafny-lang · Oct 18, 2024 · b823a08 · b823a08
1 parent 8419a62
commit b823a08
Show file tree

Hide file tree

Showing 5 changed files with 9 additions and 6 deletions.
diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
@@ -14,9 +14,12 @@ public class CommonOptionBag {
 
   public static void EnsureStaticConstructorHasRun() { }
 
-  public enum ProgressLevel { None, Symbol, SymbolParts }
+  public enum ProgressLevel { None, Symbol, VerificationJobs }
   public static readonly Option<ProgressLevel> ProgressOption =
-    new("--progress", "While verifying, output information that helps track progress");
+    new("--progress", $"While verifying, output information that helps track progress. " +
+                      $"Use '{ProgressLevel.Symbol}' to show progress across symbols such as methods and functions. " +
+                      $"Verification of a symbol is usually split across several jobs. " +
+                      $"Use {ProgressLevel.VerificationJobs} to additionally show progress across jobs.");
 
   public static readonly Option<string> LogLocation =
     new("--log-location", "Sets the directory where to store log files") {

diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs
@@ -184,7 +184,7 @@ public async IAsyncEnumerable<CanVerifyResult> VerifyAllLazily(int? randomSeed)
         var canVerifyResult = canVerifyResults[boogieUpdate.CanVerify];
         canVerifyResult.CompletedParts.Enqueue((boogieUpdate.VerificationTask, completed));
 
-        if (Options.Get(CommonOptionBag.ProgressOption) == CommonOptionBag.ProgressLevel.SymbolParts) {
+        if (Options.Get(CommonOptionBag.ProgressOption) == CommonOptionBag.ProgressLevel.VerificationJobs) {
           var token = BoogieGenerator.ToDafnyToken(false, boogieUpdate.VerificationTask.Split.Token);
           var runResult = completed.Result;
           var timeString = runResult.RunTime.ToString("g");

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify --progress SymbolParts --cores=1 %s &> %t
+// RUN: %verify --progress VerificationJobs --cores=1 %s &> %t
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 // CHECK:Verified part #0, 1/2 of Foo, on line 9, verified successfully \(time: .*, resource count: .*\)
 // CHECK:Verified part #1, 2/2 of Foo, on line 10, verified successfully \(time: .*, resource count: .*\)

diff --git a/...rationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy b/...rationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy
@@ -1,4 +1,4 @@
-// RUN: ! %verify --isolate-assertions --cores=1 --progress SymbolParts "%s" &> "%t"
+// RUN: ! %verify --isolate-assertions --cores=1 --progress VerificationJobs "%s" &> "%t"
 // RUN: %OutputCheck --file-to-check "%t" "%S/Inputs/outOfResourceAndIsolateAssertions.check"
 
 

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify --progress SymbolParts --isolate-assertions --cores=1 %s > %t
+// RUN: %verify --progress VerificationJobs --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"