Tweak the --progress option and rename the --iterations option

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -14,12 +14,12 @@ public class CommonOptionBag {
 
   public static void EnsureStaticConstructorHasRun() { }
 
-  public enum ProgressLevel { None, Symbol, VerificationJobs }
+  public enum ProgressLevel { None, Symbol, Batch }
   public static readonly Option<ProgressLevel> ProgressOption =
     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.");
+                      $"Verification of a symbol may be split across several assertion batches. " +
+                      $"Use {ProgressLevel.Batch} to additionally show progress across batches.");
 
   public static readonly Option<string> LogLocation =
     new("--log-location", "Sets the directory where to store log files") {

Source/DafnyCore/Options/DeveloperOptionBag.cs

@@ -78,6 +78,7 @@ static DeveloperOptionBag() {
 
     DafnyOptions.RegisterLegacyBinding(SplitPrint, (options, f) => {
       options.PrintSplitFile = f;
+      options.PrintSplitDeclarations = true;
       options.ExpandFilename(options.PrintSplitFile, x => options.PrintSplitFile = x, options.LogPrefix,
         options.FileTimestamp);
     });

Source/DafnyDriver/CliCompilation.cs

@@ -186,7 +186,7 @@ public async IAsyncEnumerable<CanVerifyResult> VerifyAllLazily(int? randomSeed =
         canVerifyResult.CompletedParts.Enqueue((boogieUpdate.VerificationTask, completed));
         var completedPartsCount = Interlocked.Increment(ref canVerifyResult.CompletedCount);
 
-        if (Options.Get(CommonOptionBag.ProgressOption) == CommonOptionBag.ProgressLevel.VerificationJobs) {
+        if (Options.Get(CommonOptionBag.ProgressOption) == CommonOptionBag.ProgressLevel.Batch) {
           var partOrigin = boogieUpdate.VerificationTask.Split.Token;
 
           var wellFormedness = boogieUpdate.VerificationTask.Split.Implementation.Name.Contains("CheckWellFormed$");

Source/DafnyDriver/Commands/MeasureComplexityCommand.cs

@@ -14,7 +14,7 @@ namespace Microsoft.Dafny;
 
 static class MeasureComplexityCommand {
   public static IEnumerable<Option> Options => new Option[] {
-    Iterations,
+    Mutations,
     RandomSeed,
     TopX,
     VerifyCommand.FilterSymbol,
@@ -24,10 +24,10 @@ static class MeasureComplexityCommand {
     Concat(DafnyCommands.ConsoleOutputOptions);
 
   static MeasureComplexityCommand() {
-    DafnyOptions.RegisterLegacyBinding(Iterations, (o, v) => o.RandomizeVcIterations = (int)v);
+    DafnyOptions.RegisterLegacyBinding(Mutations, (o, v) => o.RandomizeVcIterations = (int)v);
     DafnyOptions.RegisterLegacyBinding(RandomSeed, (o, v) => o.RandomSeed = (int)v);
 
-    OptionRegistry.RegisterOption(Iterations, OptionScope.Cli);
+    OptionRegistry.RegisterOption(Mutations, OptionScope.Cli);
     OptionRegistry.RegisterOption(RandomSeed, OptionScope.Cli);
     OptionRegistry.RegisterOption(TopX, OptionScope.Cli);
   }
@@ -38,7 +38,7 @@ static MeasureComplexityCommand() {
   private static readonly Option<uint> RandomSeed = new("--random-seed", () => 0U,
     $"Turn on randomization of the input that Dafny passes to the SMT solver and turn on randomization in the SMT solver itself. Certain Dafny proofs are complex in the sense that changes to the proof that preserve its meaning may cause its verification result to change. This option simulates meaning-preserving changes to the proofs without requiring the user to actually make those changes. The proof changes are renaming variables and reordering declarations in the SMT input passed to the solver, and setting solver options that have similar effects.");
 
-  private static readonly Option<uint> Iterations = new("--iterations", () => 1U,
+  private static readonly Option<uint> Mutations = new("--mutations", () => 1U,
     $"Attempt to verify each proof n times with n random seeds, each seed derived from the previous one. {RandomSeed.Name} can be used to specify the first seed, which will otherwise be 0.") {
     ArgumentHelpName = "n"
   };
@@ -121,10 +121,10 @@ private static async Task RunVerificationIterations(DafnyOptions options, CliCom
     IObserver<CanVerifyResult> verificationResultsObserver) {
     int iterationSeed = (int)options.Get(RandomSeed);
     var random = new Random(iterationSeed);
-    var iterations = (int)options.Get(Iterations);
-    foreach (var iteration in Enumerable.Range(0, iterations)) {
+    var iterations = (int)options.Get(Mutations);
+    foreach (var mutation in Enumerable.Range(0, iterations)) {
       await options.OutputWriter.WriteLineAsync(
-        $"Starting verification of iteration {iteration + 1}/{iterations} with seed {iterationSeed}");
+        $"Starting verification of mutation {mutation + 1}/{iterations} with seed {iterationSeed}");
       try {
         await foreach (var result in compilation.VerifyAllLazily(iterationSeed)) {
           verificationResultsObserver.OnNext(result);

Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy.expect

@@ -1,4 +1,4 @@
-Starting verification of iteration 1/1 with seed 0
+Starting verification of mutation 1/1 with seed 0
 measure-complexity.dfy(6,18): Error: assertion might not hold
 The total consumed resources are <redacted>
 The most demanding 100 verification tasks consumed these resources:

Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/VerificationLogger.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny measure-complexity --iterations=3 --random-seed=1 --log-format:trx";"LogFileName="%t.trx" "%s"
+// RUN: %exits-with 4 %baredafny measure-complexity --mutations=3 --random-seed=1 --log-format:trx";"LogFileName="%t.trx" "%s"
 // RUN: %OutputCheck --file-to-check "%t.trx" "%s"
 
 // CHECK: \<UnitTestResult.* testName="ExampleWithSplits \(correctness\) \(assertion batch 3\).*\>

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

@@ -1,4 +1,4 @@
-// RUN: ! %verify --isolate-assertions --cores=1 --progress VerificationJobs "%s" &> %t.raw
+// RUN: ! %verify --isolate-assertions --cores=1 --progress Batch "%s" &> %t.raw
 // RUN: %sed 's#\(time.*\)#<redacted>#g' %t.raw > %t
 // RUN: %diff "%s.expect" "%t"
 ghost function f(i:nat, j:nat):int {

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy

@@ -1,4 +1,4 @@
-// RUN: ! %verify --progress VerificationJobs --cores=1 %s &> %t.raw
+// RUN: ! %verify --progress Batch --cores=1 %s &> %t.raw
 // RUN: %sed 's#\(time.*\)#<redacted>#g' %t.raw > %t
 // RUN: %diff "%s.expect" "%t"
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAssertionOrJump.dfy

@@ -1,4 +1,4 @@
-// RUN: ! %verify --progress VerificationJobs --cores=1 %s &> %t.raw
+// RUN: ! %verify --progress Batch --cores=1 %s &> %t.raw
 // RUN: %sed 's#\(time.*\)#<redacted>#g' %t.raw > %t
 // RUN: %diff "%s.expect" "%t"
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolatePaths.dfy

@@ -1,4 +1,4 @@
-// RUN: ! %verify --progress VerificationJobs --cores=1 %s &> %t.raw
+// RUN: ! %verify --progress Batch --cores=1 %s &> %t.raw
 // RUN: %sed 's#\(time.*\)#<redacted>#g' %t.raw > %t
 // RUN: %diff "%s.expect" "%t"