Publish verification status notifications #2094

keyboardDrummer · 2022-05-04T13:57:03Z

Changes

Adds a push based API that sends verification task status information to the LSP client.
Solve a bug in SlowVerifier which caused HoverReturnsBeforeVerificationIsComplete and DefinitionReturnsBeforeVerificationIsComplete to sometimes fail.

Testing

New API is unit tested

…-lang#2004)" (dafny-lang#2092)" This reverts commit 954d495.

…solve

…agnostics are finished

…wAPI

MikaelMayer

I'm very happy with the solution you did to ensure we don't unnecessarily trigger translation if verification is not requested.
I have only a straightforward refactoring request and a discussion on the name of the push API to harmonize it with the others.

MikaelMayer · 2022-05-27T16:24:32Z

Source/Dafny/Util.cs

+
+    public static Task<U> Select<T, U>(this Task<T> task, Func<T, U> f) {
+      return task.ContinueWith(completedTask => f(completedTask.Result), TaskContinuationOptions.OnlyOnRanToCompletion);
+    }


Nice helper !

MikaelMayer · 2022-05-27T16:34:34Z

Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs

    }
  }

+  // TODO for backwards compatibility. No longer needed when the IDE switches to the textDocument/verificationStatus API


Are you saying the IDE would update the status bar based on the new API? I think that should work.

MikaelMayer · 2022-05-27T16:41:17Z

Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs

-        var diagnostics = errorReporter.GetDiagnostics(document.Uri).OrderBy(d => d.Range.Start).ToList();
-        concurrentDictionary.AddOrUpdate(id, diagnostics, (_, _) => diagnostics);
+      var result = implementationTasks.Select(implementationTask => implementationTask.ObservableStatus.Select(
+        async boogieStatus => {


Now is a good time to refactor the body of this closure so a named separated async method, else I find it hard to read.

MikaelMayer · 2022-05-27T16:52:11Z

Source/DafnyLanguageServer/Workspace/FileVerificationStatus.cs

+  Running = 2,  // Currently running
+  Error = 4,    // Finished and had errors
+  Correct = 5,  // Finished and was correct
+}


Good job for the comments and re-numbering !

MikaelMayer · 2022-05-27T17:03:56Z

Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs


-      var printer = new ModelCapturingOutputPrinter(logger, progressReporter, options.GutterStatus);
+      cancellationToken.ThrowIfCancellationRequested();


Great! This is what guarantees that typing multiple times will not result in verification to be started all the times.

MikaelMayer · 2022-05-27T17:11:43Z

Source/DafnyLanguageServer/Handlers/DafnySignatureHelpHandler.cs

@@ -52,13 +52,13 @@ private class SignatureHelpProcessor {
      }

      public SignatureHelp? Process() {
-        if (!symbolGuesser.TryGetSymbolBefore(document, GetOpenParenthesePosition(), cancellationToken, out var symbol)) {
+        if (!symbolGuesser.TryGetSymbolBefore(document, GetOpenParenthesesPosition(), cancellationToken, out var symbol)) {


Suggested change

if (!symbolGuesser.TryGetSymbolBefore(document, GetOpenParenthesesPosition(), cancellationToken, out var symbol)) {

if (!symbolGuesser.TryGetSymbolBefore(document, GetOpenParenthesisPosition(), cancellationToken, out var symbol)) {

Singular?

MikaelMayer · 2022-05-27T17:11:59Z

Source/DafnyLanguageServer/Handlers/DafnySignatureHelpHandler.cs

          return null;
        }
        return CreateSignatureHelp(symbol);
      }

-      private Position GetOpenParenthesePosition() {
+      private Position GetOpenParenthesesPosition() {


Suggested change

private Position GetOpenParenthesesPosition() {

private Position GetOpenParenthesisPosition() {

Idem?

MikaelMayer · 2022-05-27T17:20:51Z

Source/DafnyLanguageServer/DafnyRequestNames.cs

@@ -4,5 +4,6 @@ public static class DafnyRequestNames {
    public const string CompilationStatus = "dafny/compilation/status";
    public const string GhostDiagnostics = "dafny/ghost/diagnostics";
    public const string VerificationStatusGutter = "dafny/verification/status/gutter";
+    public const string VerificationStatusNotification = "dafny/textDocument/verificationStatus";


One more time on that, so far I've seen the APIs above look more like

"dafny/<pipeline context>/<result>

except for counter-examples where /verification is missing

I think it would make sense to choose a similar structure for new push APIs. Since there is also a precedent (dafny/compilation/status), I think it would make sense to have an API like one of the following:

dafny/verification/status/textDocument dafny/verification/status/tree dafny/verification/status/names dafny/verification/status/declarations dafny/verification/status/browsable

or maybe reverse the last two:

dafny/verification/textDocument/status dafny/verification/tree/status dafny/verification/names/status dafny/verification/declarations/status dafny/verification/browsable/status

Let me know what you think.

I've seen the APIs above look more like ...

To me it looks like the current code took the name of the variable and then replaced camel-casing with / separation to form the operation name, which I find strange. We can use camel-casing in the operation name without introducing additional /'s, just like LSP does.

LSP categorises the operations based on what they operate on in the IDE, the main ones are textDocument/<name>, workspace/<name and window/<name>. I think we should stick to that.

I think that APIs which don't relate to verification should already be in LSP, so dafny and verification always occur together and we might as well only mention dafny.

Given the above I would pick these names

public const string Counterexample = "textDocument/dafny/counterexample"; public const string GhostDiagnostics = "textDocument/dafny/ghostness"; public const string VerificationStatusGutter = "textDocument/dafny/lineStatus"; public const string VerificationStatusNotification = "textDocument/dafny/symbolStatus"; // Becomes obsolete by 'textDocument/dafny/symbolStatus' public const string CompilationStatus = "dafny/compilation/status";

But that would be out of scope for this PR. How about we ignore the operation names until we merge a PR that introduces a naming scheme for them?

MikaelMayer · 2022-05-27T18:11:56Z

Source/DafnyLanguageServer.Test/Completion/DotCompletionTest.cs

-    var y := x."
-        }
-      );
+      ApplyChange(ref documentItem, new Range((4, 21), (4, 21)), @"


Nice overload !

…dafny into verificationOverviewAPI

MikaelMayer

Fantastic work, can't wait to see the VSCode extension to deal with it !

keyboardDrummer added 12 commits May 6, 2022 10:05

Revert "Revert "Incrementally publish verification diagnostics (dafny…

f04bf05

…-lang#2004)" (dafny-lang#2092)" This reverts commit 954d495.

Add test to detect diagnostic flickering

3806407

Fix flickering of incremental diagnostics

00f9d4e

Correctly relocate method tied verification diagnostics

04d4a6c

Test refactoring

039706c

Cleanup

05fabed

Adapt to latest Boogie

eea8f2b

Run formatter and fix customBoogie.patch

2f8a49f

Order diagnostics to help with unit tests

057c018

Remove debug console write line

7401cc2

Bump Boogie version

8b9bde6

Add verification overview API

44b1faa

keyboardDrummer force-pushed the verificationOverviewAPI branch from 8d6c036 to 44b1faa Compare May 6, 2022 08:17

keyboardDrummer changed the base branch from master to fixFlickering May 6, 2022 08:20

keyboardDrummer added 2 commits May 6, 2022 10:22

Ran formatter

baca26f

Fix bug that caused translation to happen on a program that didn't re…

e349922

…solve

keyboardDrummer marked this pull request as ready for review May 6, 2022 08:44

keyboardDrummer changed the base branch from fixFlickering to master May 6, 2022 08:44

keyboardDrummer added 10 commits May 6, 2022 11:17

Add comment

4cac3ba

Some fixes

e7b6f6e

Add test that looks at diagnostics when updates are applied before di…

b0211c8

…agnostics are finished

Refactoring

ec67043

Tests pass

ae65c4e

Little cleanup

22df388

Merge branch 'fixFlickering' into verificationOverviewAPI

3f033fa

Tests pass

b6c2d9b

Merge branch 'master' into fixFlickering

f8e5b8c

Merge branch 'master' into verificationOverviewAPI

d9bee19

keyboardDrummer requested a review from MikaelMayer May 6, 2022 14:46

MikaelMayer marked this pull request as draft May 6, 2022 14:56

keyboardDrummer added 15 commits May 25, 2022 13:15

Remove test results

3b0422c

Update ignore file and skip index in verification status

3b6101e

Make DotCompletionTest more robust

128ea28

Merge branch 'master' into verificationOverviewAPI

91faf3e

Improve cancellation in translation step

9ce9c7a

Improve debug information

af10f79

Increase robustness of SifgnatureHelpTest

365b26f

Add locks to DocumentDatabase

3ada809

Refactor

ace63c4

Fix compilation error

8b940ab

Only run one unit test

eec65c6

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

e75a428

…wAPI

Fix exception

25ad1ea

Undo debug changes

f2a3316

Fix NotifyStatusAsync call

23fb624

keyboardDrummer force-pushed the verificationOverviewAPI branch from 05e6b99 to 23fb624 Compare May 26, 2022 22:29

keyboardDrummer added 2 commits May 27, 2022 00:40

Do not send outdated verifications

688ab2c

Merge branch 'master' into verificationOverviewAPI

68f6b52

keyboardDrummer enabled auto-merge (squash) May 26, 2022 22:55

MikaelMayer requested changes May 27, 2022

View reviewed changes

keyboardDrummer added 2 commits May 27, 2022 22:15

Code review refactoring

3ea21f4

Merge branch 'verificationOverviewAPI' of github.com:keyboardDrummer/…

d1102ff

…dafny into verificationOverviewAPI

keyboardDrummer requested a review from MikaelMayer May 27, 2022 20:16

Change operation name

854110c

MikaelMayer previously approved these changes May 27, 2022

View reviewed changes

Ran formatter

18c9d5b

keyboardDrummer dismissed MikaelMayer’s stale review via 18c9d5b May 27, 2022 20:32

MikaelMayer approved these changes May 27, 2022

View reviewed changes

keyboardDrummer merged commit c8598c8 into dafny-lang:master May 27, 2022

keyboardDrummer deleted the verificationOverviewAPI branch May 27, 2022 22:13

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Publish verification status notifications #2094

Publish verification status notifications #2094

keyboardDrummer commented May 4, 2022 •

edited

Loading

MikaelMayer left a comment

MikaelMayer May 27, 2022

MikaelMayer May 27, 2022

keyboardDrummer May 27, 2022

MikaelMayer May 27, 2022

MikaelMayer May 27, 2022

MikaelMayer May 27, 2022

MikaelMayer May 27, 2022

MikaelMayer May 27, 2022

MikaelMayer May 27, 2022

keyboardDrummer May 27, 2022 •

edited

Loading

MikaelMayer May 27, 2022

MikaelMayer left a comment


		var printer = new ModelCapturingOutputPrinter(logger, progressReporter, options.GutterStatus);
		cancellationToken.ThrowIfCancellationRequested();

	if (!symbolGuesser.TryGetSymbolBefore(document, GetOpenParenthesesPosition(), cancellationToken, out var symbol)) {
	if (!symbolGuesser.TryGetSymbolBefore(document, GetOpenParenthesisPosition(), cancellationToken, out var symbol)) {

	private Position GetOpenParenthesesPosition() {
	private Position GetOpenParenthesisPosition() {

Publish verification status notifications #2094

Publish verification status notifications #2094

Conversation

keyboardDrummer commented May 4, 2022 • edited Loading

Changes

Testing

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

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 May 27, 2022 • edited Loading

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 May 4, 2022 •

edited

Loading

keyboardDrummer May 27, 2022 •

edited

Loading