Feat: Better format in hover messages #3687

MikaelMayer · 2023-03-03T21:11:09Z

Added the trace of proof even in successes
Replaced intermediate "Could not prove" and "Did prove" by "Inside " to indicate this is just a trace
Use backticks to indicate quoted code
Better error message instead of "error is impossible: This is the precondition that might not hold"
First-class support of {:error} in hover messages.
BONUS: Not described in the issue: Hover support for {:error} in failed postconditions.

Acts as a precursor to #3324 by harmonizing the change made in boogie "might not hold" => "could not be proved" in preconditions and postconditions

before: function precondition might not hold
after:  function precondition could not be proved

before: the calculation step between the previous line and this line might not hold
after:  the calculation step between the previous line and this line could not be proved

before: This postcondition might not hold on a return path.
after:  this postcondition could not be proved on a return path

The screenshots of the issue are now fixed w.r.t. the described errors.

With support for {:error} in postconditions

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

- Added the trace of proof even in successes - Replaced intermediate "Could not prove" and "Did prove" by "Inside " to indicate this is just a trace - Use backticks to indicate quoted code - Better error message instead of "error is impossible: This is the precondition that might not hold" - First-class support of {:error} in hover messages.

keyboardDrummer · 2023-03-06T10:29:10Z

Why do we show success messages? It seems like information the user doesn't need and that might be confusing because as a user I would expect failure messages, so I might interpret the success messages as such. Especially a message like "error is impossible" which has two bad sounding words in it, reads like an error.

keyboardDrummer · 2023-03-06T10:31:04Z

Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs

- (description?.SuccessDescription ?? "_no message_");
+ case GutterVerificationStatus.Verified: {
+ var successDescription = description?.SuccessDescription ?? "_no message_";
+ if (successDescription == "error is impossible: This is the precondition that might not hold.") {


Could you refer to the substrings from which this concatenated string originates?

Could you refer to the substrings from which this concatenated string originates?

I actually found a way to get rid of this if statement by adding one more proof obligation description that ought to be implemented.

keyboardDrummer · 2023-03-06T10:32:07Z

Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs

+ case GutterVerificationStatus.Verified: {
+ var successDescription = description?.SuccessDescription ?? "_no message_";
+ if (successDescription == "error is impossible: This is the precondition that might not hold.") {
+ successDescription = "the precondition always holds";


If we have the concept of success descriptions, shouldn't they be defined together with the failure descriptions? This seems difficult to maintain.

keyboardDrummer · 2023-03-06T10:35:09Z

Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs

+
+ if (!currentlyHoveringPostcondition &&
+ (failureDescription == new EnsuresDescription().FailureDescription)) {
+ failureDescription = "a postcondition could not be proven on this return path";


Why does this message need to be changed? Why can't the back-end emit the right message to begin with? I think it would be great if DafnyHoverHandler can be completely Dafny agnostic.

Why does this message need to be changed? Why can't the back-end emit the right message to begin with? I think it would be great if DafnyHoverHandler can be completely Dafny agnostic.

Agree.
I created a new EnsuresDescription in Dafny so that we don't need this work-around Boogie's EnsuresDescription

keyboardDrummer · 2023-03-06T10:38:05Z

Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs

@@ -259,7 +274,7 @@ class AssertionBatchIndexComparer : IComparer<AssertionBatchIndex> {
 // however, nested postconditions should be displayed
 if (errorToken is BoogieRangeToken rangeToken && !hoveringPostcondition) {
 var originalText = rangeToken.PrintOriginal();
- deltaInformation += " \n" + CouldProveOrNotPrefix + originalText;
+ deltaInformation += " \n" + (token == null ? CouldProveOrNotPrefix : "Inside ") + "`" + originalText + "`";


Here is as well, why can't the back-end emit the proper message? This seems like it's introducing inconsistency between IDE and CLI

Here is as well, why can't the back-end emit the proper message? This seems like it's introducing inconsistency between IDE and CLI

This error message is specialized for the language server, as it assumes that the reader has access to markdown capabilities, and it also quotes the code that was/was not proven.
To the contrary, in the CLI, we use the term "Related position:" and only offer positions by default. We don't show code snippets for related positions. I wish we can change that but we'll keep that for another PR, as it will be another substantial change.

MikaelMayer · 2023-03-06T15:17:50Z

Why do we show success messages? It seems like information the user doesn't need and that might be confusing because as a user I would expect failure messages, so I might interpret the success messages as such. Especially a message like "error is impossible" which has two bad sounding words in it, reads like an error.

I agree that "error is impossible: X" should be replaced by a positive message. For custom error messages however, this is not possible. If you have a better rephrasing suggesting it would be good.

To the question "Why do we show success messages", note that obviously, we only show them on hover. They serve multiple purpose.

Ensure users trust that Dafny is actually proving things: Dafny is proving a LOT of properties to prevent bugs. For software engineers, knowing what Dafny was able to prove helps establishing confidence that Dafny is not forgetting something. It might seem obvious for us, it's expected from any user using Dafny, but showing it confirms the belief.
Show what Dafny proved. This is especially important for implicit assertions.
Show how many resources each assertion costs, even if proved, and even display hints if verification is too costly.
Show where this assertion is located in the assertion batch, to determine where it could be heuristically good to split the batch
Users already don't expect error messages where there is no red/yellow underline, so this is informational. There already are plenty of cases when users don't expect error messages on hovering in regular IDEs, such as getting the signature of a method or docstring.

Here is how displaying success messages could be better:

Maybe group them. We don't need to display all proved sub-predicates, sometimes it's too long
We should ensure errors are on the top. I thought I fixed it but apparently not always.

…obligation descriptions.

keyboardDrummer · 2023-03-07T13:09:26Z

Source/DafnyCore/Verifier/ProofObligationDescription.cs

+ customErrMsg ?? "this postcondition might not hold on a return path";
+
+ public string FailureAtPathDescription =>
+ customErrMsg ?? "a postcondition could not be proven on this return path";


Isn't this second line similar to PostconditionDescription.FailureDescription ?

Isn't this second line similar to PostconditionDescription.FailureDescription ?

Yes, indeed, I added a redirection instead.

keyboardDrummer · 2023-03-07T13:10:14Z

Source/DafnyCore/Verifier/ProofObligationDescription.cs

+ public override string FailureDescription =>
+ customErrMsg ?? "this postcondition might not hold on a return path";
+
+ public string FailureAtPathDescription =>


I find the concept of having an at path and a regular failure description not immediately intuitive.

Conceptually I view the verification failure as a stack trace. For example in:

predicate P(x : int) { true } predicate Q(x : int) { x == 2 // Stack(0) } method Foo() return (x: int) ensures O(x) && Q(x) // Stack(1) { x := 1; assert Foo.ensures() // Stack(2) return; }

I think in a previous discussion about squiggly lines, you explained that any part of the stack trace that falls outside of the method definition should not be taken into account, so for failing postconditions that only leaves the bottom 2 stack elements as relevant, and then I see it makes sense to have a failure description for both of those.

Feel free to ignore this comment, just me doing rubber duck analysis.

Thanks for rubber duck analysis :-)
Your metaphor with stack trace is quite interesting, worth exploring from UX's perspective. And I think this PR is exploring it that way. Let me explain you why in the next paragraph.

The existence of "nested expressions" here is due only to the condition splitting at the Dafny level, that is, if we want to prove "A && B", it will prove "A" on one side and "A ==> B" (or just "B" where A is assumed actually) on the other side. If we want to prove P(x), we will prove each conjunct of P(x) -- that's also why sometimes it's worth making predicate opaque, because if P(x) has 100 conjuncts, proving P(y) when x == y can still be very costly -
This is why I chose to replace "Could not prove" (which was technically correct, If you can't prove A, you can't prove A && B) by "Inside", to better match the metaphor of the stack.

I think in a previous discussion about squiggly lines, you explained that any part of the stack trace that falls outside of the method definition should not be taken into account,

My point was that they should not be underlined permanently as errors because they are relevant only in the context of the failed assertion.

keyboardDrummer · 2023-03-07T13:11:44Z

Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs

- failureDescription = "this postcondition might not hold on a return path";
- }
-
- if (!currentlyHoveringPostcondition &&


Is it not possible to get the description that matches the diagnostic/related location of where the cursor is? Like, if you are hovering over the postcondition, can we not find the description that says "This is the postcondition that might not hold.", and if we hover of the return statement, the one that says "A postcondition might not hold on this return path." ?

Actually, if hovering a postcondition was saying "This is the postcondition that might not hold.", it would feel weird to me, because it feels like there was a sentence referring to the postcondition before this one that this sentence answers. Otherwise, the error message would just say "This postcondition might not hold".
And this is actually the case. The message "This is the postcondition that might not hold." was designed to appear as a relative error message in the diagnostics, just below "A postcondition might not hold on this return path".

This is why we have a different error message when hovering the postcondition by itself.

Now you could try to make a single error message for both cases, one that is relative to the error path, and the other one that is considering the postcondition only by itself. That message could be "This postcondition might not hold".
However, I'm considering the user's experience, I really liked "This is the postcondition that might not hold better" better, so that mean I had to specialize the other messagE.

keyboardDrummer · 2023-03-07T13:20:33Z

Source/DafnyCore/Verifier/ProofObligationDescription.cs

+ : $"error is impossible: {customErrMsg}";
+
+ public override string FailureDescription =>
+ customErrMsg ?? "this postcondition might not hold on a return path";


This text surely already occurs somewhere else in the code base right? Can you reuse that text?

It appears in Boogie. I would like to break the dependency for the error message.

keyboardDrummer · 2023-03-07T13:21:15Z

Source/DafnyCore/Verifier/ProofObligationDescription.cs

+ public override string SuccessDescription =>
+ customErrMsg is null
+ ? "this postcondition holds"
+ : $"error is impossible: {customErrMsg}";


Why not take a customSuccessMessage as well? error is impossible: sounds bad.

Why not take a customSuccessMessage as well? error is impossible: sounds bad.

It took me some time to implement but I thought it was a nice idea.
I implemented (and documented it) using the same attribute {:error <error message>[, <success message>}` and I dropped the string "error is impossible" entirely. I also refactored the code so that similar proof obligation descriptions use the same overriding mechanism.

keyboardDrummer · 2023-03-07T13:54:46Z

To the question "Why do we show success messages", note that obviously, we only show them on hover. They serve multiple purpose.

Ensure users trust that Dafny is actually proving things: Dafny is proving a LOT of properties to prevent bugs. For software engineers, knowing what Dafny was able to prove helps establishing confidence that Dafny is not forgetting something. It might seem obvious for us, it's expected from any user using Dafny, but showing it confirms the belief.

Show what Dafny proved. This is especially important for implicit assertions.

Show how many resources each assertion costs, even if proved, and even display hints if verification is too costly.

Show where this assertion is located in the assertion batch, to determine where it could be heuristically good to split the batch

Users already don't expect error messages where there is no red/yellow underline, so this is informational. There already are plenty of cases when users don't expect error messages on hovering in regular IDEs, such as getting the signature of a method or docstring.

I would like it if we had a document that discusses the UX design of this feature. Currently a user will often be presented with duplicate error messages when hovering, and success messages, like here:

while I think in most cases the user would just like to see the bottom part:

I trust that you've thought hard about this and that there's a good chance this is a great solution, at least at the moment, but I think it would be good to have in writing the thought process and considered alternatives, because this UI seems like it compromises on succinctness.

Would it help to only show the assertion for which we're displaying the resources? Why do we also need to display error/success messages there? If there is an assertion mentioned for which resources are computed, and there is no error for it, doesn't that sufficiently imply Dafny verified it? Did we also consider grouping by batch, so the resource usage of each batch is only shown once instead of for each assertion in the batch?

# Conflicts: # Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs

…t text Fixed CI tests

# Conflicts: # Source/DafnyLanguageServer/Language/DiagnosticErrorReporter.cs

… feat-better-error-messages # Conflicts: # Source/DafnyLanguageServer/Language/DiagnosticErrorReporter.cs

MikaelMayer requested a review from keyboardDrummer March 3, 2023 21:16

MikaelMayer enabled auto-merge (squash) March 3, 2023 21:17

Support for {:error} on hover also on postconditions

c3c5516

keyboardDrummer reviewed Mar 6, 2023

View reviewed changes

MikaelMayer and others added 3 commits March 6, 2023 10:01

Review comments

32cb31d

Review comments: Got rid of patches by integrating better with Proof …

05227f6

…obligation descriptions.

Merge branch 'master' into feat-better-error-messages

60ec8d9

keyboardDrummer reviewed Mar 7, 2023

View reviewed changes

keyboardDrummer previously approved these changes Mar 7, 2023

View reviewed changes

MikaelMayer and others added 4 commits March 7, 2023 10:52

Merge branch 'master' into feat-better-error-messages

0aac9fe

Merge branch 'master' into feat-better-error-messages

b136d48

Merge branch 'master' into feat-better-error-messages

8d2b241

# Conflicts: # Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs

Fixed CI

b831daa

MikaelMayer dismissed keyboardDrummer’s stale review via b831daa March 8, 2023 21:29

MikaelMayer and others added 12 commits March 8, 2023 16:23

Ensured EnsuresDescription and PostconditionDescription share relevan…

d7a32d3

…t text Fixed CI tests

Ensure test is deterministic

be50afe

Merge branch 'master' into feat-better-error-messages

8876a81

Merge branch 'master' into feat-better-error-messages

0cd8767

Merge branch 'master' into feat-better-error-messages

89daeb4

Merge branch 'master' into feat-better-error-messages

9d8d505

Merge branch 'master' into feat-better-error-messages

ab390c5

# Conflicts: # Source/DafnyLanguageServer/Language/DiagnosticErrorReporter.cs

Last review comment

62abf54

Merge remote-tracking branch 'origin/feat-better-error-messages' into…

fea8f29

… feat-better-error-messages # Conflicts: # Source/DafnyLanguageServer/Language/DiagnosticErrorReporter.cs

Fixed latest merge.

dcbd72f

Merge branch 'master' into feat-better-error-messages

a0b2b8d

Merge branch 'master' into feat-better-error-messages

5d53a3a

MikaelMayer and others added 18 commits March 17, 2023 16:13

Reverted premature rewording

38e14f7

Fixed another one

616490f

Merge branch 'master' into feat-better-error-messages

e05ee83

Fixed merge commit

d15cb17

Fixed documentation by running "make numbers"

5cef283

Fixed CI tests

15cefb6

Merge branch 'master' into feat-better-error-messages

df6077a

Fixed CI calculation step

dea8cb3

Fixed some test cases

039ba35

Fixed CI

2be2ff1

Fix error message

84e0e85

Fixed CI

518194d

Fixed doc

ba4099a

Merge branch 'master' into feat-better-error-messages

138d8eb

Fixed CI tests again

f4af82e

Fixed CI again

b582fb9

Fixed last CI error

985d4c8

Merge branch 'master' into feat-better-error-messages

938a17d

MikaelMayer disabled auto-merge June 14, 2023 19:16

MikaelMayer requested a review from keyboardDrummer June 14, 2023 19:16

Self-review

5e2f51e

keyboardDrummer approved these changes Jun 20, 2023

View reviewed changes

keyboardDrummer and others added 2 commits June 20, 2023 12:02

Merge branch 'master' into feat-better-error-messages

cdb2f77

Merge branch 'master' into feat-better-error-messages

815d80c

MikaelMayer enabled auto-merge (squash) June 20, 2023 18:04

Merge branch 'master' into feat-better-error-messages

76756c1

MikaelMayer merged commit bd7a1ef into master Jun 21, 2023
19 checks passed

MikaelMayer deleted the feat-better-error-messages branch June 21, 2023 10:08

MikaelMayer mentioned this pull request Jun 23, 2023

Identifiers with Underscores Cause Display Issues in Hover Information dafny-lang/ide-vscode#400

Closed

ZhongRuoyu mentioned this pull request Jul 20, 2023

dafny 4.2.0 Homebrew/homebrew-core#137130

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Feat: Better format in hover messages #3687

Feat: Better format in hover messages #3687

MikaelMayer commented Mar 3, 2023 •

edited

Loading

keyboardDrummer commented Mar 6, 2023

keyboardDrummer Mar 6, 2023

MikaelMayer Mar 6, 2023

keyboardDrummer Mar 6, 2023

keyboardDrummer Mar 6, 2023

MikaelMayer Mar 6, 2023

keyboardDrummer Mar 6, 2023

MikaelMayer Mar 6, 2023

MikaelMayer commented Mar 6, 2023

keyboardDrummer Mar 7, 2023

MikaelMayer Mar 13, 2023

keyboardDrummer Mar 7, 2023

MikaelMayer Mar 13, 2023

keyboardDrummer Mar 7, 2023

MikaelMayer Mar 13, 2023

keyboardDrummer Mar 7, 2023

MikaelMayer Mar 13, 2023

keyboardDrummer Mar 7, 2023

MikaelMayer Mar 14, 2023

keyboardDrummer commented Mar 7, 2023

Feat: Better format in hover messages #3687

Feat: Better format in hover messages #3687

Conversation

MikaelMayer commented Mar 3, 2023 • edited Loading

keyboardDrummer commented Mar 6, 2023

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

MikaelMayer commented Mar 6, 2023

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 commented Mar 7, 2023

MikaelMayer commented Mar 3, 2023 •

edited

Loading