-
Notifications
You must be signed in to change notification settings - Fork 261
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
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
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? |
…r/dafny into doNotWaitForTasksAtTheTop
This reverts commit 5268729.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good!
var path = attempt + "." + extension; | ||
while (File.Exists(path)) { | ||
suffix++; | ||
path = attempt + "_" + suffix + "." + extension; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sounds good.
@@ -8,6 +8,8 @@ namespace Microsoft.Dafny; | |||
|
|||
public class CommonOptionBag { | |||
|
|||
public static void EnsureStaticConstructorHasRun() { } |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What is this method doing?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
using Microsoft.Dafny; | ||
|
||
namespace Dafny; | ||
|
||
public class Dafny { | ||
public static int Main(string[] args) { | ||
public static Task<int> Main(string[] args) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No idea ! I'm pretty sure it won't exit before the Task is done though :-D
} | ||
} | ||
if (state.EncounteredErrors) { | ||
ErrorWriter.WriteLine("Use /help for available options"); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure we should do that. This is printed when you're already using the old CLI.
@@ -50,4 +50,6 @@ static class TestCommand { | |||
}); | |||
return result; | |||
} | |||
|
|||
public static void EnsureStaticConstructorHasRun() { } |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Wait, is it possible the static constructor to not run if you don't call this method?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If you don't use a class, then its static constructor is not run.
var withoutExtension = Path.GetFileNameWithoutExtension(desiredPath); | ||
var actualPath = desiredPath; | ||
while (File.Exists(actualPath)) { | ||
actualPath = withoutExtension + "_" + index + extension; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
@@ -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> |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh nice, avoiding the global counter makes sure files with a different name don't get a useless suffice. Great!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Changes
Console.Out/Error/In
, so its can be run in parallel next to other Dafny tests.CoverageReport
code so it does not depend on a static counter, which could cause issues when running multiple Dafny instances in parallel.Console.Error
, which causes issues when running multiple Dafny instances in parallel.#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.