Skip to content

Commit

Permalink
Fix angry module LSP diagnostic (#6086)
Browse files Browse the repository at this point in the history
### What was changed?
Improve LSP diagnostics, so instead of
<img width="278" alt="image"
src="https://github.com/user-attachments/assets/36977d46-a9e0-406c-af33-7a317426a767"
/>
the IDE shows
<img width="250" alt="image"
src="https://github.com/user-attachments/assets/87c9c5df-89a4-49ea-8882-8322881dad19"
/>

For the errors:
`not resolving module '_module' because there were errors in resolving
its nested module 'A'"`
`boolean literal used as if it had type int"`

### How has this been tested?
- Added an LSP test

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
keyboardDrummer authored Jan 30, 2025
1 parent 7db1e5f commit 5cd765a
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 1 deletion.
2 changes: 1 addition & 1 deletion Source/DafnyCore/AST/Modules/ModuleDefinition.cs
Original file line number Diff line number Diff line change
Expand Up @@ -467,7 +467,7 @@ public bool Resolve(ModuleSignature sig, ModuleResolver resolver, string exportS
if (!nestedModuleDecl.ModuleDef.SuccessfullyResolved) {
if (!IsEssentiallyEmptyModuleBody()) {
// say something only if this will cause any testing to be omitted
resolver.reporter.Error(MessageSource.Resolver, nestedModuleDecl,
resolver.reporter.Error(MessageSource.Resolver, nestedModuleDecl.NameNode,
"not resolving module '{0}' because there were errors in resolving its nested module '{1}'", Name,
nestedModuleDecl.Name);
}
Expand Down
20 changes: 20 additions & 0 deletions Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,26 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization {
public class DiagnosticsTest : ClientBasedLanguageServerTest {
private readonly string testFilesDirectory = Path.Combine(Directory.GetCurrentDirectory(), "Synchronization/TestFiles");

[Fact]
public async Task NestedModuleRange() {
var source = @"
module A {
function A(x: int): int {
true
}
function B(x: int): int {
1
}
}
method Main() {
}".TrimStart();
var documentItem = CreateAndOpenTestDocument(source);
var diagnostics1 = await GetLastDiagnostics(documentItem);
var startOrdered = diagnostics1.OrderBy(r => r.Range.Start).ToList();
Assert.Equal(new Range(0, 7, 0, 8), startOrdered[0].Range);
Assert.Equal(new Range(1, 2, 3, 3), startOrdered[1].Range);
}

[Fact]
public async Task ResolutionErrorMigration() {
var source = @"module ResolutionError {
Expand Down

0 comments on commit 5cd765a

Please sign in to comment.