Fixed the rebase

dafny-lang · May 12, 2022 · fb4b98a · fb4b98a
1 parent 72419c6
commit fb4b98a
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 3 deletions.
diff --git a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs
@@ -12,6 +12,7 @@
 using Microsoft.Boogie;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
+using VerificationStatus = Microsoft.Dafny.LanguageServer.Workspace.Notifications.VerificationStatus;
 
 namespace Microsoft.Dafny.LanguageServer.Handlers {
  public class DafnyHoverHandler : HoverHandlerBase {

diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
@@ -195,7 +195,6 @@ public IObservable<DafnyDocument> Verify(DafnyDocument document, CancellationTok
  var outcomeError = result.GetOutcomeError(Options);
  if (outcomeError != null) {
  errorReporter.ReportBoogieError(outcomeError);
- methodTree.ResourceCount = 0;
  }
 
  var diagnostics = errorReporter.GetDiagnostics(document.Uri).OrderBy(d => d.Range.Start).ToList();

diff --git a/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs b/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs
@@ -202,6 +202,7 @@ public void ReportRealtimeDiagnostics(bool verificationStarted, DafnyDocument? d
  private void ReportMethodsBeingVerified(string extra = "") {
  var pending = document.VerificationTree.Children
  .Where(diagnostic => diagnostic.Started && !diagnostic.Finished)
+ .OrderBy(diagnostic => diagnostic.StartTime)
  .Select(diagnostic => diagnostic.DisplayName)
  .ToList();
  var total = document.VerificationTree.Children.Count();
@@ -259,6 +260,8 @@ public void ReportEndVerifyImplementation(Implementation implementation, Verific
  } else {
  lock (LockProcessing) {
  implementationNode.Stop();
+ implementationNode.ResourceCount = verificationResult.ResourceCount;
+ targetMethodNode.ResourceCount += verificationResult.ResourceCount;
  var finalOutcome = verificationResult.Outcome switch {
  ConditionGeneration.Outcome.Correct => VerificationStatus.Verified,
  _ => VerificationStatus.Error
@@ -307,7 +310,10 @@ public void ReportAssertionBatchResult(Split split,
  result.ComputePerAssertOutcomes(out var perAssertOutcome, out var perAssertCounterExample);
 
  var assertionBatchIndex = implementationNode.GetNewAssertionBatchCount();
- implementationNode.IncreaseNewAssertionBatchCount();
+ var assertionBatchTime = (int)result.runTime.TotalMilliseconds;
+ var assertionBatchResourceCount = result.resourceCount;
+ implementationNode.AddAssertionBatchTime(assertionBatchTime);
+ implementationNode.AddAssertionBatchResourceCount(assertionBatchResourceCount);
 
  // Attaches the trace
  void AddChildOutcome(Counterexample? counterexample, AssertCmd assertCmd, IToken token,
@@ -337,7 +343,8 @@ void AddChildOutcome(Counterexample? counterexample, AssertCmd assertCmd, IToken
  AssertionBatchIndex = assertionBatchIndex,
  Started = true,
  Finished = true
- }.WithAssertionAndCounterExample(assertCmd, counterexample);
+ }.WithDuration(implementationNode.StartTime, assertionBatchTime)
+ .WithAssertionAndCounterExample(assertCmd, counterexample);
  // Add this diagnostics as the new one to display once the implementation is fully verified
  implementationNode.AddNewChild(nodeDiagnostic);
  // Update any previous pending "verifying" diagnostic as well so that they are updated in real-time