Various fixes for project aware mode (#4299)

Depends on #4273

### Changes

1. Take URIs into account when handling manual verification run and
cancellation requests
1. Enable project aware mode option
1. Send compilation status updates for all documents owned by a project
1. Do not retrigger compilation of a project when opening an unchanged
document of that project

### Tests
1. Add test `RunWithMultipleSimilarDocuments`
1. No test needed
1. Add test `CompilationStatusNotificationTest.MultipleDocuments`
1. Performance, difficult to test without an existing framework

<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>

Source/DafnyCore/AST/Grammar/CustomDirectoryInfoWrapper.cs

@@ -1,6 +1,7 @@
 // Licensed to the .NET Foundation under one or more agreements.
 // The .NET Foundation licenses this file to you under the MIT license.
 
+#nullable enable
 using System;
 using System.Collections.Generic;
 using System.IO;
@@ -59,7 +60,7 @@ public override IEnumerable<FileSystemInfoBase> EnumerateFileSystemInfos() {
     /// </remarks>
     /// <param name="name">The directory name</param>
     /// <returns>The directory</returns>
-    public override DirectoryInfoBase GetDirectory(string name) {
+    public override DirectoryInfoBase? GetDirectory(string name) {
       bool isParentPath = string.Equals(name, "..", StringComparison.Ordinal);
 
       if (isParentPath) {

Source/DafnyLanguageServer.Test/ProjectFiles/CompetingProjectFilesTest.cs

@@ -1,35 +1,43 @@
+using System;
 using System.IO;
 using System.Threading.Tasks;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
 using Microsoft.Dafny.LanguageServer.Workspace;
-using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using Xunit;
 using Xunit.Abstractions;
+using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
 namespace Microsoft.Dafny.LanguageServer.IntegrationTest.ProjectFiles; 
 
 public class CompetingProjectFilesTest : ClientBasedLanguageServerTest {
 
+  protected override Task SetUp(Action<DafnyOptions> modifyOptions) {
+    return base.SetUp(o => {
+      o.Set(ServerCommand.ProjectMode, true);
+      modifyOptions?.Invoke(o);
+    });
+  }
+
+
   /// <summary>
   /// A project should only publish diagnostics for uris which it owns,
   /// We can have a function filterOwnership(IdeState -> IdeState)
   /// that adds the "an error occurred outside this project"
   /// </summary>
-  [Fact(Skip = "Not yet supported")]
+  [Fact]
   public async Task ProjectFileDoesNotOwnAllSourceFilesItUses() {
     var tempDirectory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
     var nestedDirectory = Path.Combine(tempDirectory, "nested");
     Directory.CreateDirectory(nestedDirectory);
     await File.WriteAllTextAsync(Path.Combine(nestedDirectory, "source.dfy"), "hasErrorInSyntax");
     await File.WriteAllTextAsync(Path.Combine(nestedDirectory, DafnyProject.FileName), "");
 
-    var outerProject = CreateTestDocument("", Path.Combine(tempDirectory, DafnyProject.FileName));
-    await client.OpenDocumentAndWaitAsync(outerProject, CancellationToken);
+    await CreateAndOpenTestDocument("", Path.Combine(tempDirectory, DafnyProject.FileName));
 
-    var diagnostics = await GetLastDiagnostics(outerProject, CancellationToken);
+    var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken);
     Assert.Single(diagnostics);
-    Assert.Contains("something about a file not owned by the project", diagnostics[0].Message);
+    Assert.Contains("the referenced file", diagnostics[0].Message);
   }
 
   public readonly string hasShadowingSource = @"
@@ -44,7 +52,7 @@ method Foo() {
   /// Here the outer project loses ownership of this document.
   /// At this point we simply need to apply the filterOwnership function on its last published IdeState again
   /// </summary>
-  [Fact(Skip = "Not yet supported")]
+  [Fact]
   public async Task NewProjectFileGrabsSourceFileOwnership() {
     var tempDirectory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
     var nestedDirectory = Path.Combine(tempDirectory, "nested");
@@ -66,6 +74,8 @@ public async Task NewProjectFileGrabsSourceFileOwnership() {
     Assert.Contains("Shadowed", diagnostics0[0].Message);
 
     await File.WriteAllTextAsync(Path.Combine(nestedDirectory, DafnyProject.FileName), "");
+    await Task.Delay(ProjectManagerDatabase.ProjectFileCacheExpiryTime);
+
     ApplyChange(ref sourceFile, new Range(0, 0, 0, 0), "//comment\n");
     var diagnostics1 = await GetLastDiagnostics(sourceFile, CancellationToken);
     Assert.Empty(diagnostics1);

Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesTest.cs

@@ -176,18 +176,16 @@ method Produces() {}
 
     var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
     Directory.CreateDirectory(directory);
-    await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName), projectFileSource);
+    var projectFilePath = Path.Combine(directory, DafnyProject.FileName);
+    await File.WriteAllTextAsync(projectFilePath, projectFileSource);
 
     var consumer = await CreateAndOpenTestDocument(consumerSource, Path.Combine(directory, "firstFile.dfy"));
     var secondFile = await CreateAndOpenTestDocument(producer, Path.Combine(directory, "secondFile.dfy"));
 
     var producesDefinition1 = await RequestDefinition(consumer, new Position(1, 3));
     Assert.Empty(producesDefinition1);
 
-    // Wait to prevent an IOException because the file is already in use.
-    await Task.Delay(100);
-    await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName),
-      @"includes = [""firstFile.dfy"", ""secondFile.dfy""]");
+    await FileTestExtensions.WriteWhenUnlocked(projectFilePath, @"includes = [""firstFile.dfy"", ""secondFile.dfy""]");
     await Task.Delay(ProjectManagerDatabase.ProjectFileCacheExpiryTime);
 
     var producesDefinition2 = await RequestDefinition(consumer, new Position(1, 3));
@@ -215,7 +213,7 @@ method Foo() {
 
 [options]
 warn-shadowing = true
-"; // includes must come before [options], even if there is a blank line
+".Trim(); // includes must come before [options], even if there is a blank line
     var directory = Path.GetRandomFileName();
     var projectFile = await CreateAndOpenTestDocument(projectFileSource, Path.Combine(directory, DafnyProject.FileName));
     var sourceFile = await CreateAndOpenTestDocument(source, Path.Combine(directory, "src/file.dfy"));
@@ -225,7 +223,7 @@ method Foo() {
     Assert.Contains(diagnostics1, s => s.Message.Contains("Shadowed"));
 
     await Task.Delay(ProjectManagerDatabase.ProjectFileCacheExpiryTime);
-    ApplyChange(ref projectFile, new Range(1, 17, 1, 21), "false");
+    ApplyChange(ref projectFile, new Range(3, 17, 3, 21), "false");
 
     var resolutionDiagnostics2 = await diagnosticsReceiver.AwaitNextWarningOrErrorDiagnosticsAsync(CancellationToken);
     // The shadowed warning is no longer produced, and the verification error is not migrated. 

Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs

@@ -11,6 +11,13 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest;
 
 public class ProjectFilesTest : ClientBasedLanguageServerTest {
 
+  [Fact]
+  public async Task ProjectFileByItselfHasNoDiagnostics() {
+    var tempDirectory = Path.GetRandomFileName();
+    await CreateAndOpenTestDocument("", Path.Combine(tempDirectory, DafnyProject.FileName));
+    await AssertNoDiagnosticsAreComing(CancellationToken);
+  }
+
   [Fact]
   public async Task ProjectFileChangesArePickedUpAfterCacheExpiration() {
     await SetUp(options => options.WarnShadowing = false);
@@ -29,13 +36,13 @@ method Foo() {
 ";
     var documentItem = CreateTestDocument(source, Path.Combine(tempDirectory, "source.dfy"));
     await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+    await AssertNoDiagnosticsAreComing(CancellationToken);
 
     var warnShadowingOn = @"
 [options]
 warn-shadowing = true";
-    // Wait to prevent an IOException because the file is already in use.
-    await Task.Delay(100);
-    await File.WriteAllTextAsync(projectFilePath, warnShadowingOn);
+
+    await FileTestExtensions.WriteWhenUnlocked(projectFilePath, warnShadowingOn);
     await Task.Delay(ProjectManagerDatabase.ProjectFileCacheExpiryTime);
     ApplyChange(ref documentItem, new Range(0, 0, 0, 0), "//touch comment\n");
     var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken);

Source/DafnyLanguageServer.Test/Synchronization/CloseDocumentTest.cs

@@ -46,7 +46,7 @@ function GetConstant(): int {
 }".Trim();
       var documentItem = CreateTestDocument(source);
       client.CloseDocument(documentItem);
-      Assert.Null(await Projects.GetResolvedDocumentAsync(documentItem.Uri));
+      Assert.Null(await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri));
     }
 
     public CloseDocumentTest(ITestOutputHelper output) : base(output) {

Source/DafnyLanguageServer.Test/Synchronization/DeclarationLocationMigrationTest.cs

@@ -52,7 +52,7 @@ await ApplyChangeAndWaitCompletionAsync(
         new Range((3, 0), (4, 1)),
         change
       );
-      var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri);
+      var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
       Assert.NotNull(document);
       Assert.True(TryFindSymbolDeclarationByName(document, "A", out var location));
       Assert.Equal(new Range((0, 6), (0, 7)), location.Name);
@@ -79,7 +79,7 @@ await ApplyChangeAndWaitCompletionAsync(
         new Range((3, 0), (4, 0)),
         change
       );
-      var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri);
+      var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
       Assert.NotNull(document);
       Assert.True(TryFindSymbolDeclarationByName(document, "A", out var location));
       Assert.Equal(new Range((0, 6), (0, 7)), location.Name);
@@ -112,7 +112,7 @@ await ApplyChangeAndWaitCompletionAsync(
         new Range((3, 0), (4, 1)),
         change
       );
-      var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri);
+      var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
       Assert.NotNull(document);
       Assert.True(TryFindSymbolDeclarationByName(document, "C", out var location));
       Assert.Equal(new Range((10, 6), (10, 7)), location.Name);
@@ -139,7 +139,7 @@ await ApplyChangeAndWaitCompletionAsync(
         new Range((3, 0), (4, 0)),
         change
       );
-      var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri);
+      var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
       Assert.NotNull(document);
       Assert.True(TryFindSymbolDeclarationByName(document, "C", out var location));
       Assert.Equal(new Range((5, 6), (5, 7)), location.Name);
@@ -166,7 +166,7 @@ await ApplyChangeAndWaitCompletionAsync(
         new Range((3, 19), (3, 22)),
         change
       );
-      var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri);
+      var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
       Assert.NotNull(document);
       Assert.True(TryFindSymbolDeclarationByName(document, "GetX", out var location));
       Assert.Equal(new Range((3, 11), (3, 15)), location.Name);
@@ -190,7 +190,7 @@ await ApplyChangeAndWaitCompletionAsync(
         new Range((1, 2), (1, 13)),
         change
       );
-      var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri);
+      var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
       Assert.NotNull(document);
       Assert.True(TryFindSymbolDeclarationByName(document, "A", out var location));
       Assert.Equal(new Range((0, 6), (0, 7)), location.Name);
@@ -208,7 +208,7 @@ await ApplyChangeAndWaitCompletionAsync(
         new Range((0, 10), (0, 21)),
         change
       );
-      var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri);
+      var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
       Assert.NotNull(document);
       Assert.True(TryFindSymbolDeclarationByName(document, "A", out var location));
       Assert.Equal(new Range((0, 6), (0, 7)), location.Name);
@@ -232,7 +232,7 @@ await ApplyChangeAndWaitCompletionAsync(
         new Range((1, 2), (1, 13)),
         change
       );
-      var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri);
+      var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
       Assert.NotNull(document);
       Assert.False(TryFindSymbolDeclarationByName(document, "x", out var _));
     }
@@ -264,7 +264,7 @@ var a
 }".TrimStart()
         }
       );
-      var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri);
+      var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
       Assert.NotNull(document);
       Assert.True(TryFindSymbolDeclarationByName(document, "B", out var bLocation));
       Assert.Equal(new Range((4, 6), (4, 7)), bLocation.Name);
@@ -280,22 +280,22 @@ public async Task PassingANullChangeRangeClearsSymbolsTable() {
       var documentItem = CreateTestDocument(source);
 
       await Client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
-      var state = await Projects.GetResolvedDocumentAsync(documentItem.Uri);
+      var state = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
       Assert.NotNull(state);
       Assert.True(TryFindSymbolDeclarationByName(state, "X", out var _));
 
       // First try a change that doesn't break resolution.
       // In this case all information is recomputed and no relocation happens.
       await ApplyChangeAndWaitCompletionAsync(ref documentItem, null, "class Y {}");
-      state = await Projects.GetResolvedDocumentAsync(documentItem);
+      state = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem);
       Assert.NotNull(state); // No relocation, since no resolution errors, so Y can be found
       Assert.False(TryFindSymbolDeclarationByName(state, "X", out var _));
       Assert.True(TryFindSymbolDeclarationByName(state, "Y", out var _));
 
       // Next try a change that breaks resolution.
       // In this case symbols are relocated.  Since the change range is `null` all symbols for "test.dfy" are lost.
       await ApplyChangeAndWaitCompletionAsync(ref documentItem, null, "; class Y {}");
-      state = await Projects.GetResolvedDocumentAsync(documentItem);
+      state = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem);
       Assert.NotNull(state);
       // Relocation happens due to the syntax error; range is null so table is cleared
       Assert.False(TryFindSymbolDeclarationByName(state, "X", out var _));
@@ -309,19 +309,19 @@ public async Task PassingANullChangeRangePreservesForeignSymbols() {
       var documentItem = CreateTestDocument(source, Path.Combine(Directory.GetCurrentDirectory(), "Lookup/TestFiles/test.dfy"));
 
       await Client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
-      var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri);
+      var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
       Assert.NotNull(document);
       Assert.True(TryFindSymbolDeclarationByName(document, "A", out var _));
 
       // Try a change that breaks resolution.  Symbols for `foreign.dfy` are kept.
       await ApplyChangeAndWaitCompletionAsync(ref documentItem, null, "; include \"foreign.dfy\"\nclass Y {}");
-      document = await Projects.GetResolvedDocumentAsync(documentItem);
+      document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem);
       Assert.NotNull(document);
       Assert.True(TryFindSymbolDeclarationByName(document, "A", out var _));
 
       // Finally we drop the reference to `foreign.dfy` and confirm that `A` is not accessible any more.
       await ApplyChangeAndWaitCompletionAsync(ref documentItem, null, "class Y {}");
-      document = await Projects.GetResolvedDocumentAsync(documentItem);
+      document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem);
       Assert.NotNull(document);
       Assert.False(TryFindSymbolDeclarationByName(document, "A", out var _));
     }

Source/DafnyLanguageServer.Test/Synchronization/IncludeFileTest.cs

@@ -26,7 +26,7 @@ method Test() {
 }";
     var documentItem = CreateTestDocument(source, TestFilePath);
     await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
-    var document = await Projects.GetResolvedDocumentAsync(documentItem.Uri);
+    var document = await Projects.GetResolvedDocumentAsyncNormalizeUri(documentItem.Uri);
     Assert.NotNull(document);
     Assert.All(document.GetDiagnostics(), a => Assert.Empty(a.Value));
   }
@@ -84,6 +84,7 @@ public async Task IndirectlyIncludedFileFailsSyntax() {
     var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken);
     Assert.Single(diagnostics);
     Assert.Contains("the referenced file", diagnostics[0].Message);
+    Assert.Contains("The first error is:\nrbrace expected", diagnostics[0].Message);
     Assert.Contains("syntaxError.dfy", diagnostics[0].Message);
   }