Hover and gutter icon project support (dafny-lang#4337)

Depends on dafny-lang#4350

### Changes
- Enable complex hover messages and gutter icons when in project mode
- Do not publish gutter icons if the exact same icons have been
previously published.

### Testing
- Update hover and gutter icon tests so they have project mode turned on

<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/Options/DafnyProject.cs

@@ -19,13 +19,12 @@ public class DafnyProject : IEquatable<DafnyProject> {
 
   public string ProjectName => Uri.ToString();
 
-  public bool IsImplicitProject { get; set; }
-
   [IgnoreDataMember]
   public Uri Uri { get; set; }
   public string[] Includes { get; set; }
   public string[] Excludes { get; set; }
   public Dictionary<string, object> Options { get; set; }
+  public bool UsesProjectFile => Path.GetFileName(Uri.LocalPath) == FileName;
 
   public static async Task<DafnyProject> Open(IFileSystem fileSystem, Uri uri, TextWriter outputWriter, TextWriter errorWriter) {
     if (Path.GetFileName(uri.LocalPath) != FileName) {
@@ -173,7 +172,7 @@ public bool Equals(DafnyProject other) {
     var orderedOptions = Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty<KeyValuePair<string, object>>();
     var otherOrderedOptions = other.Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty<KeyValuePair<string, object>>();
 
-    return Equals(IsImplicitProject, other.IsImplicitProject) && Equals(Uri, other.Uri) &&
+    return Equals(Uri, other.Uri) &&
            NullableSetEqual(Includes?.ToHashSet(), other.Includes) &&
            NullableSetEqual(Excludes?.ToHashSet(), other.Excludes) &&
            orderedOptions.SequenceEqual(otherOrderedOptions, new LambdaEqualityComparer<KeyValuePair<string, object>>(
@@ -255,6 +254,6 @@ public override bool Equals(object obj) {
   }
 
   public override int GetHashCode() {
-    return HashCode.Combine(IsImplicitProject, Uri, Includes, Excludes, Options);
+    return HashCode.Combine(Uri, Includes, Excludes, Options);
   }
 }

Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs

@@ -5,6 +5,7 @@
 //
 //-----------------------------------------------------------------------------
 
+using System;
 using System.Collections.Generic;
 using System.Linq;
 using System.Diagnostics.Contracts;
@@ -1329,7 +1330,8 @@ void ResolveFrameExpression(FrameExpression fe, FrameExpressionUse use, ICodeCon
             FrameExpressionUse.Modifies =>
               $"a modifies-clause {expressionMustDenoteObject} or {collection} {instead}",
             FrameExpressionUse.Unchanged =>
-              $"an unchanged {expressionMustDenoteObject} or {collection} {instead}"
+              $"an unchanged {expressionMustDenoteObject} or {collection} {instead}",
+            _ => throw new ArgumentOutOfRangeException(nameof(use), use, null)
           };
           ReportError(fe.E.tok, errorMsgFormat, fe.E.PreType);
         }

Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs

@@ -128,7 +128,7 @@ protected static TextDocumentItem CreateTestDocument(string source, string fileP
       if (filePath == null) {
         filePath = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName(), $"testFile{fileIndex++}.dfy");
       }
-      if (Path.GetDirectoryName(filePath) == null) {
+      if (string.IsNullOrEmpty(Path.GetDirectoryName(filePath))) {
         filePath = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName(), filePath);
       }
       filePath = Path.GetFullPath(filePath);

Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs

@@ -28,7 +28,7 @@ await VerifyTrace(@"
  .  S  S  |  I  $  | :}", true);
   }
 
-  [Fact(Timeout = MaxTestExecutionTimeMs)]
+  [Fact]
   public async Task EnsureCachingDoesNotHideErrors() {
     await SetUp(options => {
       options.Set(BoogieOptionBag.Cores, 1U);

Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs

@@ -25,6 +25,7 @@ protected override async Task SetUp(Action<DafnyOptions> modifyOptions) {
 
     void ModifyOptions(DafnyOptions options) {
       options.Set(ServerCommand.LineVerificationStatus, true);
+      options.Set(ServerCommand.ProjectMode, true);
       modifyOptions?.Invoke(options);
     }
     await base.SetUp(ModifyOptions);
@@ -302,7 +303,7 @@ public async Task VerifyTrace(string codeAndTrace, bool explicitProject, string
     foreach (var changes in changesList) {
       ApplyChanges(ref documentItem, changes);
       traces.AddRange(await GetAllLineVerificationStatuses(documentItem, verificationStatusGutterReceiver, intermediates: intermediates));
-      await Projects.GetLastDocumentAsync(documentItem);
+      await Projects.GetLastDocumentAsync(documentItem).WaitAsync(CancellationToken);
     }
 
     if (testTrace) {

Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs

@@ -3,6 +3,7 @@
 using System.Text.RegularExpressions;
 using System.Threading.Tasks;
 using JetBrains.Annotations;
+using Microsoft.Boogie;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
@@ -19,6 +20,14 @@
 namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup {
   [Collection("Sequential Collection")] // Let slow tests run sequentially
   public class HoverVerificationTest : ClientBasedLanguageServerTest {
+
+    protected override Task SetUp(Action<DafnyOptions> modifyOptions) {
+      return base.SetUp(o => {
+        o.Set(ServerCommand.ProjectMode, true);
+        modifyOptions?.Invoke(o);
+      });
+    }
+
     private const int MaxTestExecutionTimeMs = 30000;
 
     [Fact(Timeout = MaxTestExecutionTimeMs)]
@@ -207,7 +216,7 @@ await AssertHoverMatches(documentItem, (0, 36),
       );
     }
 
-    [Fact(Timeout = MaxTestExecutionTimeMs)]
+    [Fact]
     public async Task MeaningfulMessageWhenMethodWithoutAssert() {
       var documentItem = await GetDocumentItem(@"
 method f(x: int) {
@@ -491,12 +500,13 @@ await AssertHoverMatches(documentItem, (0, 22),
     }
 
     private async Task<TextDocumentItem> GetDocumentItem(string source, string filename, bool includeProjectFile) {
+      var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
       source = source.TrimStart();
       if (includeProjectFile) {
-        var projectFile = CreateTestDocument("", Path.Combine(Path.GetDirectoryName(filename), DafnyProject.FileName));
+        var projectFile = CreateTestDocument("", Path.Combine(directory, DafnyProject.FileName));
         await client.OpenDocumentAndWaitAsync(projectFile, CancellationToken);
       }
-      var documentItem = CreateTestDocument(source, filename);
+      var documentItem = CreateTestDocument(source, Path.Combine(directory, filename));
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
       var document = await Projects.GetLastDocumentAsync(documentItem);
       Assert.True(document is CompilationAfterTranslation);

Source/DafnyLanguageServer/Handlers/DafnyCodeActionHandler.cs

@@ -155,5 +155,5 @@ public DafnyCodeActionInput(CompilationAfterParsing compilation, Uri uri) {
   public CompilationAfterParsing Compilation { get; }
 
   public IEnumerable<DafnyDiagnostic> Diagnostics => Compilation.GetDiagnostics(uri);
-  public VerificationTree? VerificationTree => Compilation.GetVerificationTree();
+  public VerificationTree? VerificationTree => Compilation.GetVerificationTree(uri);
 }

Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs

@@ -116,10 +116,12 @@ public int Compare(AssertionBatchIndex? key1, AssertionBatchIndex? key2) {
         return null;
       }
 
-      if (state.VerificationTree == null) {
+      var tree = state.VerificationTrees.GetValueOrDefault(uri);
+      if (tree == null) {
         return null;
       }
-      foreach (var node in state.VerificationTree.Children.OfType<TopLevelDeclMemberVerificationTree>()) {
+
+      foreach (var node in tree.Children.OfType<TopLevelDeclMemberVerificationTree>()) {
         if (!node.Range.Contains(position)) {
           continue;
         }
@@ -128,7 +130,8 @@ public int Compare(AssertionBatchIndex? key1, AssertionBatchIndex? key2) {
         var information = "";
         var orderedAssertionBatches =
           node.AssertionBatches
-            .OrderBy(keyValue => keyValue.Key, new AssertionBatchIndexComparer()).Select(keyValuePair => keyValuePair.Value)
+            .OrderBy(keyValue => keyValue.Key, new AssertionBatchIndexComparer())
+            .Select(keyValuePair => keyValuePair.Value)
             .ToList();
 
         foreach (var assertionBatch in orderedAssertionBatches) {
@@ -144,7 +147,9 @@ public int Compare(AssertionBatchIndex? key1, AssertionBatchIndex? key2) {
               if (information != "") {
                 information += "\n\n";
               }
-              information += GetAssertionInformation(state, position, assertionNode, assertionBatch, assertionIndex, assertionBatchCount, node);
+
+              information += GetAssertionInformation(state, position, assertionNode, assertionBatch,
+                assertionIndex, assertionBatchCount, node);
             }
 
             assertionIndex++;
@@ -154,8 +159,9 @@ public int Compare(AssertionBatchIndex? key1, AssertionBatchIndex? key2) {
         if (information != "") {
           return information;
         }
+
         // Ok no assertion here. Maybe a method?
-        if (node.Position.Line == position.Line && state.Compilation.Project.IsImplicitProject && node.Uri == state.Compilation.Project.Uri) {
+        if (node.Position.Line == position.Line) {
           areMethodStatistics = true;
           return GetTopLevelInformation(node, orderedAssertionBatches);
         }

Source/DafnyLanguageServer/Handlers/DafnyRenameHandler.cs

@@ -37,7 +37,7 @@ protected override RenameRegistrationOptions CreateRegistrationOptions(
       var requestUri = request.TextDocument.Uri.ToUri();
       // Reject rename requests in implicit projects, because we might not find all references within the codebase,
       // so a partial rename may result in breaking the codebase
-      if ((await projects.GetProject(requestUri)).IsImplicitProject) {
+      if (!(await projects.GetProject(requestUri)).UsesProjectFile) {
         throw new Exception("Renaming support requires --project-mode and a Dafny project file (dfyconfig.toml)");
       }
 

Source/DafnyLanguageServer/Handlers/DafnyTextDocumentHandler.cs

@@ -83,14 +83,14 @@ public override async Task<Unit> Handle(DidCloseTextDocumentParams notification,
       return Unit.Value;
     }
 
-    public override Task<Unit> Handle(DidChangeTextDocumentParams notification, CancellationToken cancellationToken) {
+    public override async Task<Unit> Handle(DidChangeTextDocumentParams notification, CancellationToken cancellationToken) {
       logger.LogDebug("received change notification {DocumentUri}", notification.TextDocument.Uri);
       try {
-        projects.UpdateDocument(notification);
+        await projects.UpdateDocument(notification);
       } catch (Exception e) {
         telemetryPublisher.PublishUnhandledException(e);
       }
-      return Unit.Task;
+      return Unit.Value;
     }
 
     public override Task<Unit> Handle(DidSaveTextDocumentParams notification, CancellationToken cancellationToken) {

Source/DafnyLanguageServer/Language/IVerificationProgressReporter.cs

@@ -1,19 +1,17 @@
-using System.Diagnostics;
+using System;
 using Microsoft.Boogie;
 using Microsoft.Dafny.LanguageServer.Workspace;
-using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
-using VC;
 
 namespace Microsoft.Dafny.LanguageServer.Language {
   /// <summary>
   /// A callback interface to report verification progress
   /// </summary>
   public interface IVerificationProgressReporter {
-    void RecomputeVerificationTree(CompilationAfterTranslation compilation);
-    void ReportRealtimeDiagnostics(CompilationAfterTranslation compilation, bool verificationStarted);
+    void RecomputeVerificationTrees(CompilationAfterTranslation compilation);
+    void ReportRealtimeDiagnostics(CompilationAfterTranslation compilation, Uri uri, bool verificationStarted);
 
     void ReportVerifyImplementationRunning(CompilationAfterTranslation compilation, Implementation implToken);
-    void ReportEndVerifyImplementation(CompilationAfterTranslation compilation, Implementation implToken, Boogie.VerificationResult verificationResult);
+    void ReportEndVerifyImplementation(CompilationAfterTranslation compilation, Implementation implToken, VerificationResult verificationResult);
     void ReportImplementationsBeforeVerification(CompilationAfterTranslation compilation, Implementation[] implementations);
     void ReportAssertionBatchResult(CompilationAfterTranslation compilation, AssertionBatchResult batchResult);
     void SetAllUnvisitedMethodsAsVerified(CompilationAfterTranslation compilation);

Source/DafnyLanguageServer/Workspace/CompilationManager.cs

@@ -20,7 +20,7 @@ public delegate CompilationManager CreateCompilationManager(
   DafnyOptions options,
   ExecutionEngine boogieEngine,
   Compilation compilation,
-  VerificationTree? migratedVerificationTree);
+  IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees);
 
 /// <summary>
 /// The compilation of a single document version.
@@ -41,7 +41,7 @@ public class CompilationManager {
   private readonly IVerificationProgressReporter verificationProgressReporter;
 
   // TODO CompilationManager shouldn't be aware of migration
-  private readonly VerificationTree? migratedVerificationTree;
+  private readonly IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees;
 
   private TaskCompletionSource started = new();
   private readonly IScheduler verificationUpdateScheduler = new EventLoopScheduler();
@@ -68,12 +68,12 @@ public CompilationManager(
     DafnyOptions options,
     ExecutionEngine boogieEngine,
     Compilation compilation,
-    VerificationTree? migratedVerificationTree
+    IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees
     ) {
     this.options = options;
     startingCompilation = compilation;
     this.boogieEngine = boogieEngine;
-    this.migratedVerificationTree = migratedVerificationTree;
+    this.migratedVerificationTrees = migratedVerificationTrees;
 
     this.documentLoader = documentLoader;
     this.logger = logger;
@@ -102,9 +102,12 @@ private async Task<CompilationAfterParsing> ResolveAsync() {
       // TODO, let gutter icon publications also used the published CompilationView.
       var state = documentAfterParsing.InitialIdeState(startingCompilation, options);
       state = state with {
-        VerificationTree = migratedVerificationTree ?? state.VerificationTree
+        VerificationTrees = documentAfterParsing.RootUris.ToDictionary(uri => uri,
+          uri => migratedVerificationTrees.GetValueOrDefault(uri) ?? new DocumentVerificationTree(documentAfterParsing.Program, uri))
       };
-      notificationPublisher.PublishGutterIcons(state, false);
+      foreach (var root in documentAfterParsing.RootUris) {
+        notificationPublisher.PublishGutterIcons(root, state, false);
+      }
 
       logger.LogDebug($"documentUpdates.HasObservers: {compilationUpdates.HasObservers}, threadId: {Thread.CurrentThread.ManagedThreadId}");
       compilationUpdates.OnNext(documentAfterParsing);
@@ -178,13 +181,16 @@ public async Task<CompilationAfterTranslation> PrepareVerificationTasksAsync(
       loaded.ResolutionDiagnostics, verificationTasks,
       new(),
       initialViews,
-      migratedVerificationTree ?? (loaded.Project.IsImplicitProject ? new DocumentVerificationTree(loaded.Program, loaded.Project.Uri) : null)
+      loaded.RootUris.ToDictionary(uri => uri,
+        uri => migratedVerificationTrees.GetValueOrDefault(uri) ?? new DocumentVerificationTree(loaded.Program, uri))
       );
 
-    verificationProgressReporter.RecomputeVerificationTree(translated);
+    verificationProgressReporter.RecomputeVerificationTrees(translated);
 
     if (ReportGutterStatus) {
-      verificationProgressReporter.ReportRealtimeDiagnostics(translated, false);
+      foreach (var uri in translated.RootUris) {
+        verificationProgressReporter.ReportRealtimeDiagnostics(translated, uri, true);
+      }
     }
     verificationProgressReporter.ReportImplementationsBeforeVerification(translated,
       verificationTasks.Select(t => t.Implementation).ToArray());
@@ -264,7 +270,9 @@ public void FinishedNotifications(CompilationAfterTranslation compilation) {
         SetAllUnvisitedMethodsAsVerified(compilation);
       }
 
-      verificationProgressReporter.ReportRealtimeDiagnostics(compilation, true);
+      foreach (var uri in compilation.RootUris) {
+        verificationProgressReporter.ReportRealtimeDiagnostics(compilation, uri, true);
+      }
     }
   }
 

Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs

@@ -36,12 +36,13 @@ public Compilation(int version, DafnyProject project, IReadOnlyList<Uri> rootUri
     public virtual IEnumerable<DafnyDiagnostic> GetDiagnostics(Uri uri) => Enumerable.Empty<DafnyDiagnostic>();
 
     public IdeState InitialIdeState(Compilation compilation, DafnyOptions options) {
-      return ToIdeState(new IdeState(compilation, new EmptyNode(),
+      var program = new EmptyNode();
+      return ToIdeState(new IdeState(compilation, program,
         ImmutableDictionary<Uri, IReadOnlyList<Diagnostic>>.Empty,
         SymbolTable.Empty(), SignatureAndCompletionTable.Empty(options, compilation.Project), new Dictionary<ImplementationId, IdeImplementationView>(),
         Array.Empty<Counterexample>(),
         false, ImmutableDictionary<Uri, IReadOnlyList<Range>>.Empty,
-       null
+        compilation.RootUris.ToDictionary(uri => uri, uri => (VerificationTree)new DocumentVerificationTree(program, uri))
       ));
     }
 

Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterParsing.cs

@@ -33,11 +33,11 @@ public override IdeState ToIdeState(IdeState previousState) {
       ResolutionDiagnostics = ResolutionDiagnostics.ToDictionary(
         kv => kv.Key,
         kv => (IReadOnlyList<Diagnostic>)kv.Value.Select(d => d.ToLspDiagnostic()).ToList()),
-      VerificationTree = baseResult.VerificationTree ?? GetVerificationTree()?.GetCopyForNotification()
+      VerificationTrees = baseResult.VerificationTrees
     };
   }
 
-  public virtual VerificationTree? GetVerificationTree() {
-    return Project.IsImplicitProject ? new DocumentVerificationTree(Program, Project.Uri) : null;
+  public virtual VerificationTree GetVerificationTree(Uri uri) {
+    return new DocumentVerificationTree(Program, uri);
   }
 }