From 63c93def02332b0f8eb16774f578840fdf4a6a47 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Tue, 15 Oct 2024 16:35:46 +0200
Subject: [PATCH] Fix tests and an ordering bug

---
 Source/DafnyDriver/CliCompilation.cs              | 15 ++++++++-------
 .../LitTests/LitTest/logger/VerboseName.dfy       |  2 +-
 .../LitTest/verification/isolate-assertions.dfy   |  2 +-
 .../outOfResourceAndIsolateAssertions.dfy         |  2 +-
 .../LitTests/LitTest/verification/progress.dfy    |  2 +-
 5 files changed, 12 insertions(+), 11 deletions(-)

diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs
index fd4ea92454..c0f551aab7 100644
--- a/Source/DafnyDriver/CliCompilation.cs
+++ b/Source/DafnyDriver/CliCompilation.cs
@@ -218,10 +218,11 @@ public async IAsyncEnumerable<CanVerifyResult> VerifyAllLazily(int? randomSeed)
 
     int done = 0;
 
-    var orderedCanVerifies = canVerifies.OrderBy(v => v.Tok.pos).ToList();
-    var canVerifiesPerModule = orderedCanVerifies.GroupBy(c => c.ContainingModule).ToList();
-    foreach (var canVerifiesForModule in canVerifiesPerModule) {
-      foreach (var canVerify in canVerifiesForModule) {
+    var canVerifiesPerModule = canVerifies.ToList().GroupBy(c => c.ContainingModule).ToList();
+    foreach (var canVerifiesForModule in canVerifiesPerModule.
+               OrderBy(v => v.Key.Tok.pos)) {
+      var orderedCanVerifies = canVerifiesForModule.OrderBy(v => v.Tok.pos).ToList();
+      foreach (var canVerify in orderedCanVerifies) {
         var results = new CliCanVerifyState();
         canVerifyResults[canVerify] = results;
         if (line != null) {
@@ -230,16 +231,16 @@ public async IAsyncEnumerable<CanVerifyResult> VerifyAllLazily(int? randomSeed)
 
         var shouldVerify = await Compilation.VerifyCanVerify(canVerify, results.TaskFilter, randomSeed);
         if (!shouldVerify) {
-          orderedCanVerifies.Remove(canVerify);
+          canVerifies.ToList().Remove(canVerify);
         }
       }
 
-      foreach (var canVerify in canVerifiesForModule) {
+      foreach (var canVerify in orderedCanVerifies) {
         var results = canVerifyResults[canVerify];
         try {
           if (Options.Get(CommonOptionBag.ProgressOption) > CommonOptionBag.ProgressLevel.None) {
             await Options.OutputWriter.WriteLineAsync(
-              $"Verified {done}/{orderedCanVerifies.Count} symbols. Waiting for {canVerify.FullDafnyName} to verify.");
+              $"Verified {done}/{canVerifies.ToList().Count} symbols. Waiting for {canVerify.FullDafnyName} to verify.");
           }
 
           await results.Finished.Task;
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/VerboseName.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/VerboseName.dfy
index 8567235715..4ea12ecb8d 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/VerboseName.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/VerboseName.dfy
@@ -1,4 +1,4 @@
-// RUN: %verify --progress --cores 1 "%s" > "%t"
+// RUN: %verify --progress Symbol --cores 1 "%s" > "%t"
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 // CHECK-L:Verified 0/5 symbols. Waiting for smallPrime to verify.
 // CHECK-L:Verified 2/5 symbols. Waiting for posIdMeth to verify.
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy
index 9fdfcd621b..5c406f380a 100644
--- 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 --cores=1 %s &> %t
+// RUN: %verify --progress SymbolParts --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/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy
index 89b2e46ac9..d61c6f2395 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 "%s" &> "%t"
+// RUN: ! %verify --isolate-assertions --cores=1 --progress SymbolParts "%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
index dc479d31aa..c4248078a9 100644
--- 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 --isolate-assertions --cores=1 %s > %t
+// RUN: %verify --progress SymbolParts --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"