Use async main methods to avoid waiting for tasks at the top level #4585

keyboardDrummer · 2023-09-26T15:03:59Z

Changes

Update the legacy Dafny server code so it does not refer Console.Out/Error/In, so its can be run in parallel next to other Dafny tests.
Change the CoverageReport code so it does not depend on a static counter, which could cause issues when running multiple Dafny instances in parallel.
Change the legacy parser code so it does not print error message to Console.Error, which causes issues when running multiple Dafny instances in parallel.
Add a timeout to individual littish tests of 5 minutes. Currently a stuck littish test will cause the entire test suite to hang until it times out at the Github actions level, which we've configured to 120 minutes, after which we get no indication of which test it was stuck on !!
Refactoring of littish testing code
Remove two occurrences of #pragma warning disable VSTHRD002 by relying on async Main methods. An effect of this change might be that Dafny will use fewer threads. I was triggered to make this change when I was debugging Dafny and noticed some threads always waiting at the locations where this PR removes the Wait.

Testing

This is a refactoring which is covered by existing tests.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

…TheTop

robin-aws · 2024-01-18T23:51:47Z

Comment as a spin-off from #4798 - can we also add a link to an issue on the remaining pragmas this PR doesn't end up resolving?

…TheTop

…r/dafny into doNotWaitForTasksAtTheTop

This reverts commit 5268729.

…TheTop

MikaelMayer

Looks good!

MikaelMayer · 2024-02-12T12:39:04Z

Source/DafnyCore/CoverageReport/CoverageReport.cs

+    var path = attempt + "." + extension;
+    while (File.Exists(path)) {
+      suffix++;
+      path = attempt + "_" + suffix + "." + extension;


Sounds good.

MikaelMayer · 2024-02-12T12:39:43Z

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -8,6 +8,8 @@ namespace Microsoft.Dafny;

 public class CommonOptionBag {

+  public static void EnsureStaticConstructorHasRun() { }


What is this method doing?

What the name says it does. If you call a method in a class, dotnet will first ensure the class's static constructor was run.

MikaelMayer · 2024-02-12T12:40:52Z

Source/Dafny/Dafny.cs

 using Microsoft.Dafny;

 namespace Dafny;

 public class Dafny {
-  public static int Main(string[] args) {
+  public static Task<int> Main(string[] args) {


I did not know you could do that. Interesting. I understand it's to be able to test this method directly; but how is it compiled? It will await for that task?

No idea ! I'm pretty sure it won't exit before the Task is done though :-D

MikaelMayer · 2024-02-12T13:16:37Z

Source/DafnyCore/DafnyOptions.cs

+        }
+      }
+      if (state.EncounteredErrors) {
+        ErrorWriter.WriteLine("Use /help for available options");


Suggested change

ErrorWriter.WriteLine("Use /help for available options");

ErrorWriter.WriteLine("Use --help for available options");

Since we can now customize this error message, I thought we could as well support the new CLI by default.

I'm not sure we should do that. This is printed when you're already using the old CLI.

MikaelMayer · 2024-02-12T13:17:20Z

Source/DafnyDriver/Commands/TestCommand.cs

@@ -50,4 +50,6 @@ static class TestCommand {
    });
    return result;
  }
+
+  public static void EnsureStaticConstructorHasRun() { }


Wait, is it possible the static constructor to not run if you don't call this method?

If you don't use a class, then its static constructor is not run.

MikaelMayer · 2024-02-12T13:18:11Z

Source/DafnyDriver/CoverageReporter.cs

+      var withoutExtension = Path.GetFileNameWithoutExtension(desiredPath);
+      var actualPath = desiredPath;
+      while (File.Exists(actualPath)) {
+        actualPath = withoutExtension + "_" + index + extension;


This looks like duplicate code from https://github.com/dafny-lang/dafny/pull/4585/files#diff-8f346d4cacb8d208b553e6e51abc34de1f262354c3901eff9416e148f0c6e19bR25
could you perhaps consolidate and define this code only once?

MikaelMayer · 2024-02-12T13:21:18Z

...ntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined.html.expect

@@ -10,7 +10,7 @@
 <body onload="window['PR_TAB_WIDTH']=4">
 <div class="menu" id="menu">
    <a href="./index_combined.html">Index</a>
-    <a href="ProofDependencies.dfy_tests_expected_2.html" class="el_report">Expected Test Coverage (coverage_testing)</a><a href="ProofDependencies.dfy_verification_3.html" class="el_report">Verification coverage (coverage_verification)</a>
+    <a href="ProofDependencies.dfy_tests_expected.html" class="el_report">Expected Test Coverage (coverage_testing)</a><a href="ProofDependencies.dfy_verification.html" class="el_report">Verification coverage (coverage_verification)</a>


Oh nice, avoiding the global counter makes sure files with a different name don't get a useless suffice. Great!

…TheTop

MikaelMayer

I was not expecting to delete the duplicate code, rather put it at the same place, but it looks like you figured out it was not necessary.

Use async main methods to avoid waiting for tasks at the top level

05584cf

keyboardDrummer requested a review from robin-aws September 26, 2023 15:03

keyboardDrummer enabled auto-merge (squash) September 26, 2023 15:04

keyboardDrummer added 4 commits September 27, 2023 11:26

Fixes

b90aae4

More tasks

238359a

Merge remote-tracking branch 'origin/master' into doNotWaitForTasksAt…

60c5a1d

…TheTop

Merge branch 'master' into doNotWaitForTasksAtTheTop

5015f9a

keyboardDrummer mentioned this pull request Jan 11, 2024

Separate UI code and business logic for the resolve and verify commands #4798

Merged

keyboardDrummer added 21 commits February 5, 2024 17:22

Add timeout for tests

ee338e5

Merge remote-tracking branch 'origin/master' into doNotWaitForTasksAt…

d7f407d

…TheTop

Console. related fixes

fd44360

Refactoring

c81f913

Remove duplication

5f1b846

Fix diffCommand bug

648ceb7

Add comments

a238311

Two renames

2730a2b

Refactoring

25bad3f

Merge remote-tracking branch 'origin/master' into doNotWaitForTasksAt…

1e81a78

…TheTop

Fixes for coverage report

32f27be

Coverage report changes

823932a

Remove timeout

388e650

Do not switch contexts while waiting for a test to finish

7135d8e

Merge branch 'master' into doNotWaitForTasksAtTheTop

467a576

Attempt to let the build pass

824e108

Merge branch 'doNotWaitForTasksAtTheTop' of github.com:keyboardDrumme…

4e77b19

…r/dafny into doNotWaitForTasksAtTheTop

Switch it up

5268729

Revert "Switch it up"

e9f0b7a

This reverts commit 5268729.

Swithc to catch aggregate exception and rethrow skipException

f99b74e

Merge branch 'master' into doNotWaitForTasksAtTheTop

36f6fd4

Merge remote-tracking branch 'origin/master' into doNotWaitForTasksAt…

152d63c

…TheTop

keyboardDrummer requested review from MikaelMayer and fabiomadge and removed request for robin-aws and MikaelMayer February 8, 2024 21:40

Code review

50fb9c7

keyboardDrummer requested review from MikaelMayer and removed request for fabiomadge February 12, 2024 10:48

MikaelMayer reviewed Feb 12, 2024

View reviewed changes

Remove obsolete code

4d366a0

keyboardDrummer requested a review from MikaelMayer February 12, 2024 18:05

Merge remote-tracking branch 'origin/master' into doNotWaitForTasksAt…

b8c603d

…TheTop

MikaelMayer approved these changes Feb 13, 2024

View reviewed changes

Merge branch 'master' into doNotWaitForTasksAtTheTop

905313a

keyboardDrummer merged commit 9604175 into dafny-lang:master Feb 13, 2024
20 checks passed

keyboardDrummer deleted the doNotWaitForTasksAtTheTop branch February 13, 2024 17:58

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Use async main methods to avoid waiting for tasks at the top level #4585

Use async main methods to avoid waiting for tasks at the top level #4585

keyboardDrummer commented Sep 26, 2023 •

edited

Loading

robin-aws commented Jan 18, 2024

MikaelMayer left a comment

MikaelMayer Feb 12, 2024

MikaelMayer Feb 12, 2024

keyboardDrummer Feb 12, 2024

MikaelMayer Feb 12, 2024

keyboardDrummer Feb 12, 2024 •

edited

Loading

MikaelMayer Feb 12, 2024

keyboardDrummer Feb 12, 2024 •

edited

Loading

MikaelMayer Feb 12, 2024

keyboardDrummer Feb 12, 2024 •

edited

Loading

MikaelMayer Feb 12, 2024

MikaelMayer Feb 12, 2024

MikaelMayer left a comment

		@@ -8,6 +8,8 @@ namespace Microsoft.Dafny;

		public class CommonOptionBag {

		public static void EnsureStaticConstructorHasRun() { }

	ErrorWriter.WriteLine("Use /help for available options");
	ErrorWriter.WriteLine("Use --help for available options");

Use async main methods to avoid waiting for tasks at the top level #4585

Use async main methods to avoid waiting for tasks at the top level #4585

Conversation

keyboardDrummer commented Sep 26, 2023 • edited Loading

Changes

Testing

robin-aws commented Jan 18, 2024

MikaelMayer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Feb 12, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Feb 12, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Feb 12, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment

keyboardDrummer commented Sep 26, 2023 •

edited

Loading

keyboardDrummer Feb 12, 2024 •

edited

Loading

keyboardDrummer Feb 12, 2024 •

edited

Loading

keyboardDrummer Feb 12, 2024 •

edited

Loading