feat: Better LSP related location error messages #2434
Conversation
Display what postcondition is failing Explicit what related locations are failing.
RELEASE_NOTES.md
Outdated
| @@ -1,3 +1,7 @@ | |||
| # Upcoming | |||
|
|
|||
| - feat: Snippet in the error messages of the language server. (https://github.com/dafny-lang/dafny/pull/2434) | |||
There was a problem hiding this comment.
This description isn't entirely clear to me, and could probably do more to show how nice this is to have.
There was a problem hiding this comment.
What about the new description?
| if (tokenForMessage is RangeToken range) { | ||
| var rangeLength = range.EndToken.pos + range.EndToken.val.Length - range.StartToken.pos; | ||
| if (message == PostConditionFailingMessage) { | ||
| var postcondition = entryDocumentsource.Substring(range.StartToken.pos, rangeLength); |
There was a problem hiding this comment.
Ah, nice, so you get the exact text from the document!
| var postcondition = entryDocumentsource.Substring(range.StartToken.pos, rangeLength); | ||
| message = $"This postcondition might not hold: {postcondition}"; | ||
| } else if (message == "Related location") { | ||
| // We can do better than that. |
| var (tokenForMessage, inner) = token is NestedToken nestedToken ? (nestedToken.Outer, nestedToken.Inner) : (token, null); | ||
| if (tokenForMessage is RangeToken range) { | ||
| var rangeLength = range.EndToken.pos + range.EndToken.val.Length - range.StartToken.pos; | ||
| if (message == PostConditionFailingMessage) { |
There was a problem hiding this comment.
I'm not thrilled with this way of detecting the type of message, but I suspect it may be necessary for now, and that we'd have to do a lot of refactoring to be able to do it in a nicer way.
There was a problem hiding this comment.
I had the same feeling.
| var tokenUriSystemPath = tokenUri.GetFileSystemPath(); | ||
| var entryDocumentUriSystemPath = entryDocumentUri.GetFileSystemPath(); | ||
| if (tokenUri == entryDocumentUri || tokenUriSystemPath == entryDocumentUriSystemPath || | ||
| tokenUriSystemPath == "/" + entryDocumentUriSystemPath) { |
There was a problem hiding this comment.
Oof. Is there a way we can normalize the system path to avoid having to check all of these cases?
There was a problem hiding this comment.
Oh right. I had been fighting to enable a simpler code but I forgot this case. Let me fix it.
| var entryDocumentUriSystemPath = entryDocumentUri.GetFileSystemPath(); | ||
| if (tokenUri == entryDocumentUri || tokenUriSystemPath == entryDocumentUriSystemPath || | ||
| tokenUriSystemPath == "/" + entryDocumentUriSystemPath) { | ||
| if (tokenUri == entryDocumentUri) { |
| @@ -1,6 +1,6 @@ | |||
| # Upcoming | |||
|
|
|||
| - feat: Snippet in the error messages of the language server. (https://github.com/dafny-lang/dafny/pull/2434) | |||
| - feat: *Less code navigation when verifying code*: In the IDE, failing postconditions and preconditions error messages now immediately display the sub-conditions that Dafny could not prove. Both on hover and in the Problems window. (https://github.com/dafny-lang/dafny/pull/2434) | |||
Improvement: instead of "Related location", explicit what these related locations are about:
Fixes dafny-lang/ide-vscode#211
On hovering a postcondition, the main message is now "This postcondition might not hold on a return path". #2433 takes cares of changing "related location" to "return path".
Fixes dafny-lang/ide-vscode#197 by changing all Uri to string conversion to the standard
Uri.toString() / DocumentUri.Parse()so that there is no loss of conversion, and we don't assume a valid file name. Except for includes.Fixes dafny-lang/ide-vscode#193 by providing which postconditions are failing explicitely
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.