Fix tests and an ordering bug

dafny-lang · Oct 15, 2024 · 63c93de · 63c93de
1 parent 7f9ca76
commit 63c93de
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 11 deletions.
diff --git 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
@@ -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
@@ -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/...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 "%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
@@ -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"