From f8e5b87140d845ea38c7792be39276047d0183aa Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Fri, 24 Jan 2025 14:14:56 +0100
Subject: [PATCH 1/4] Tweak the --progress option and rename the --iterations
 option

---
 Source/DafnyCore/Options/CommonOptionBag.cs        |  6 +++---
 .../Commands/MeasureComplexityCommand.cs           | 14 +++++++-------
 .../LitTests/LitTest/logger/VerificationLogger.dfy |  2 +-
 .../outOfResourceAndIsolateAssertions.dfy          |  2 +-
 .../proofDivision/isolateAllAssertions.dfy         |  2 +-
 .../proofDivision/isolateAssertionOrJump.dfy       |  2 +-
 .../verification/proofDivision/isolatePaths.dfy    |  2 +-
 7 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
index 8ade67e6e07..979f0f9f4ee 100644
--- a/Source/DafnyCore/Options/CommonOptionBag.cs
+++ b/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") {
diff --git a/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs b/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs
index f02d8c7ded0..875476bf682 100644
--- a/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs
+++ b/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);
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/VerificationLogger.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/VerificationLogger.dfy
index 9d01a6aab96..998628f4b1a 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/VerificationLogger.dfy
+++ b/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\).*\>
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy
index 34ab6377f30..f904adca472 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy
+++ b/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 {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy
index 2363f8d4aca..22e797b366f 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAllAssertions.dfy
+++ b/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"
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAssertionOrJump.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAssertionOrJump.dfy
index fee71516a8e..75fa4fd0ad9 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolateAssertionOrJump.dfy
+++ b/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"
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolatePaths.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolatePaths.dfy
index 6fa6903cf5b..f99250e06cb 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/proofDivision/isolatePaths.dfy
+++ b/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"
 

From 1b1e48bc82d4c42bfee22b6820e4805314ee33be Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Fri, 24 Jan 2025 14:26:01 +0100
Subject: [PATCH 2/4] Fix oops

---
 Source/DafnyDriver/CliCompilation.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs
index 98fba2d30d1..b1af56b7ed5 100644
--- a/Source/DafnyDriver/CliCompilation.cs
+++ b/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$");

From 9b1afa236e8a91695f5ac2ed35c1ac7ca64edf38 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Fri, 24 Jan 2025 14:57:10 +0100
Subject: [PATCH 3/4] Update expect file

---
 Source/DafnyCore/Options/DeveloperOptionBag.cs                  | 1 +
 .../LitTests/LitTest/cli/measure-complexity.dfy.expect          | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/Source/DafnyCore/Options/DeveloperOptionBag.cs b/Source/DafnyCore/Options/DeveloperOptionBag.cs
index bff35feaa0b..7f9503f9d2c 100644
--- a/Source/DafnyCore/Options/DeveloperOptionBag.cs
+++ b/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);
     });
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy.expect
index 427b48d3a5b..6d85294ad54 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy.expect
+++ b/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:

From 44a662c3f1fd9b0acc5afc5aeffb3d73d40b7578 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Tue, 28 Jan 2025 11:19:38 +0100
Subject: [PATCH 4/4] Add release notes

---
 docs/dev/news/6078.feat | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 docs/dev/news/6078.feat

diff --git a/docs/dev/news/6078.feat b/docs/dev/news/6078.feat
new file mode 100644
index 00000000000..5f0c9fb54f2
--- /dev/null
+++ b/docs/dev/news/6078.feat
@@ -0,0 +1 @@
+The options --iterations from the command `measure-complexity`, has been renamed to `--mutations`. The option `--progress VerificationJob` has been renamed to `--progress Batch`.
\ No newline at end of file