IDE performance improvements (dafny-lang#5415)

Includes changes from dafny-lang#5394

### Description
- `ProgramParser.ParseFiles` already was an asynchronous operation, but
the parse caching mechanism did not take this into account, so it could
start pruning the caching before a parsing run was completed, causing
cache entries to be incorrectly pruned, leading to less caching of
parsing. The resolution cache depends on GUIDs from the parsing cache to
determine cache keys for modules, so this also broke resolution caching.
- `PruneIfNotUsedSinceLastPruneCache` was not thread-safe, so doing two
use+prune operations concurrently could serialize to a
use+use+prune+prune operation, which would incorrectly prune things.
- Fix a bug in `ProjectManager` that cause one compilation in a sequence
of a compilations for a particular project, to have a crash.
- A profiling session showed lots of time going into computing `Count`
on `ConcatReadOnlyList`, so that property is now computed just once for
such a list. However, this problem really requires more IDE performance
tests.
- Update included files message

### How has this been tested?
- Added a test `ConcurrentCompilationDoesNotBreakCaching` to check that
caching work swell when concurrent operations occur
- Added a test `DocumentAddedToExistingProjectDoesNotCrash` that checks
whether adding documents to an existing project does not cause a
compilation to crash.

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

---------

Co-authored-by: Robin Salkeld <[email protected]>

Source/DafnyCore/DafnyFile.cs

@@ -29,7 +29,7 @@ public class DafnyFile {
   private static readonly Dictionary<Uri, Uri> ExternallyVisibleEmbeddedFiles = new();
 
   static DafnyFile() {
-    DooFile.RegisterLibraryCheck(DoNotVerifyDependencies, OptionCompatibility.OptionLibraryImpliesLocalError);
+    DooFile.RegisterLibraryCheck(UnsafeDependencies, OptionCompatibility.OptionLibraryImpliesLocalError);
   }
 
   public static Uri ExposeInternalUri(string externalName, Uri internalUri) {
@@ -108,7 +108,7 @@ public static async IAsyncEnumerable<DafnyFile> CreateAndValidate(IFileSystem fi
     }
   }
 
-  public static readonly Option<bool> DoNotVerifyDependencies = new("--dont-verify-dependencies",
+  public static readonly Option<bool> UnsafeDependencies = new("--dont-verify-dependencies",
     "Allows Dafny to accept dependencies that may not have been previously verified, which can be useful during development.");
 
   public static DafnyFile? HandleDafnyFile(IFileSystem fileSystem,
@@ -141,7 +141,7 @@ public static async IAsyncEnumerable<DafnyFile> CreateAndValidate(IFileSystem fi
       return null;
     }
 
-    if (!options.Get(DoNotVerifyDependencies) && asLibrary && warnLibrary) {
+    if (!options.Get(UnsafeDependencies) && asLibrary && warnLibrary) {
       reporter.Warning(MessageSource.Project, "", origin,
         $"The file '{options.GetPrintPath(filePath)}' was passed to --library. " +
         $"Verification for that file might have used options incompatible with the current ones, or might have been skipped entirely. " +

Source/DafnyCore/Generic/Lists.cs

@@ -14,6 +14,7 @@ public class ConcatReadOnlyLists<T> : IReadOnlyList<T> {
   public ConcatReadOnlyLists(IReadOnlyList<T> left, IReadOnlyList<T> right) {
     Left = left;
     Right = right;
+    Count = left.Count + right.Count;
   }
 
   public IReadOnlyList<T> Left { get; }
@@ -26,7 +27,7 @@ IEnumerator IEnumerable.GetEnumerator() {
     return GetEnumerator();
   }
 
-  public int Count => Left.Count + Right.Count;
+  public int Count { get; private set; }
 
   public T this[int index] => index < Left.Count ? Left[index] : Right[index - Left.Count];
 }

Source/DafnyCore/Options/DafnyProject.cs

@@ -31,7 +31,7 @@ public class DafnyProject : IEquatable<DafnyProject> {
   public ISet<string> Excludes { get; }
   public IDictionary<string, object> Options { get; }
 
-  public bool UsesProjectFile => Path.GetFileName(Uri.LocalPath) == FileName;
+  public bool UsesProjectFile => Path.GetFileName(Uri.LocalPath).EndsWith(FileName);
   public bool ImplicitFromCli;
 
   public IToken StartingToken => ImplicitFromCli ? Token.Cli : new Token {

Source/DafnyCore/Pipeline/Compilation.cs

@@ -134,11 +134,12 @@ private async Task<IReadOnlyList<DafnyFile>> DetermineRootFiles() {
     await started.Task;
 
     var result = new List<DafnyFile>();
-
+    var includedFiles = new List<DafnyFile>();
     foreach (var uri in Input.Project.GetRootSourceUris(fileSystem)) {
       await foreach (var file in DafnyFile.CreateAndValidate(fileSystem, errorReporter, Options, uri,
                        Project.StartingToken)) {
         result.Add(file);
+        includedFiles.Add(file);
       }
     }
 
@@ -179,20 +180,22 @@ private async Task<IReadOnlyList<DafnyFile>> DetermineRootFiles() {
       }
     }
 
-    var libraryFiles = CommonOptionBag.SplitOptionValueIntoFiles(Options.Get(CommonOptionBag.Libraries).Select(f => f.FullName));
-    foreach (var library in libraryFiles) {
+    var libraryDafnyFiles = new List<DafnyFile>();
+    var libraryPaths = CommonOptionBag.SplitOptionValueIntoFiles(Options.Get(CommonOptionBag.Libraries).Select(f => f.FullName));
+    foreach (var library in libraryPaths) {
       await foreach (var file in DafnyFile.CreateAndValidate(fileSystem, errorReporter, Options, new Uri(library), Project.StartingToken, true)) {
         result.Add(file);
+        libraryDafnyFiles.Add(file);
       }
     }
 
-    var projectPath = Project.Uri.LocalPath;
-    if (projectPath.EndsWith(DafnyProject.FileName)) {
-      var projectDirectory = Path.GetDirectoryName(projectPath)!;
-      var filesMessage = string.Join("\n", result.Select(uri => Path.GetRelativePath(projectDirectory, uri.Uri.LocalPath)));
-      if (filesMessage.Any()) {
-        errorReporter.Info(MessageSource.Project, Project.StartingToken, "Files referenced by project are:" + Environment.NewLine + filesMessage);
+    if (Project.UsesProjectFile) {
+      var projectDirectory = Path.GetDirectoryName(Project.Uri.LocalPath)!;
+      var includedRootsMessage = string.Join("\n", includedFiles.Select(dafnyFile => Path.GetRelativePath(projectDirectory, dafnyFile.Uri.LocalPath)));
+      if (includedRootsMessage == "") {
+        includedRootsMessage = "none";
       }
+      errorReporter.Info(MessageSource.Project, Project.StartingToken, "Files included by project are:" + Environment.NewLine + includedRootsMessage);
     }
 
     // Allow specifying the same file twice on the CLI

Source/DafnyCore/Pipeline/ISymbolResolver.cs

@@ -1,9 +1,10 @@
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using System.Threading;
+using System.Threading.Tasks;
 using Microsoft.Dafny.LanguageServer.Workspace;
 
 namespace Microsoft.Dafny {
   public interface ISymbolResolver {
-    void ResolveSymbols(Compilation compilation, Program program, CancellationToken cancellationToken);
+    Task ResolveSymbols(Compilation compilation, Program program, CancellationToken cancellationToken);
   }
 }

Source/DafnyCore/Pipeline/TextDocumentLoader.cs

@@ -41,16 +41,16 @@ public async Task<Program> ParseAsync(Compilation compilation, CancellationToken
       CancellationToken cancellationToken) {
 #pragma warning disable CS1998
       return await await DafnyMain.LargeStackFactory.StartNew(
-        async () => ResolveInternal(compilation, program, cancellationToken), cancellationToken);
+        () => ResolveInternal(compilation, program, cancellationToken), cancellationToken);
 #pragma warning restore CS1998
     }
 
-    private ResolutionResult? ResolveInternal(Compilation compilation, Program program, CancellationToken cancellationToken) {
+    private async Task<ResolutionResult?> ResolveInternal(Compilation compilation, Program program, CancellationToken cancellationToken) {
       if (program.HasParseErrors) {
         return null;
       }
 
-      symbolResolver.ResolveSymbols(compilation, program, cancellationToken);
+      await symbolResolver.ResolveSymbols(compilation, program, cancellationToken);
 
       compilation.Options.ProcessSolverOptions(compilation.Reporter, compilation.Options.DafnyProject.StartingToken);
 

Source/DafnyCore/Resolver/ProgramResolver.cs

@@ -3,6 +3,7 @@
 using System.Diagnostics.Contracts;
 using System.Linq;
 using System.Threading;
+using System.Threading.Tasks;
 using Microsoft.Dafny.Compilers;
 
 namespace Microsoft.Dafny;
@@ -28,7 +29,7 @@ public Dictionary<string, MemberDecl> GetClassMembers(TopLevelDeclWithMembers ke
     return null;
   }
 
-  public virtual void Resolve(CancellationToken cancellationToken) {
+  public virtual Task Resolve(CancellationToken cancellationToken) {
     Type.ResetScopes();
 
     Type.EnableScopes();
@@ -43,7 +44,7 @@ public virtual void Resolve(CancellationToken cancellationToken) {
     ComputeModuleDependencyGraph(Program, out var moduleDeclarationPointers);
 
     if (Reporter.ErrorCount != startingErrorCount) {
-      return;
+      return Task.CompletedTask;
     }
 
     var sortedDecls = dependencies.TopologicallySortedComponents();
@@ -71,7 +72,7 @@ public virtual void Resolve(CancellationToken cancellationToken) {
     }
 
     if (Reporter.ErrorCount != startingErrorCount) {
-      return;
+      return Task.CompletedTask;
     }
 
     Type.DisableScopes();
@@ -83,6 +84,7 @@ public virtual void Resolve(CancellationToken cancellationToken) {
       cancellationToken.ThrowIfCancellationRequested();
       rewriter.PostResolve(Program);
     }
+    return Task.CompletedTask;
   }
 
   public void AddSystemClass(TopLevelDeclWithMembers topLevelDeclWithMembers, Dictionary<string, MemberDecl> memberDictionary) {

Source/DafnyDriver/Commands/ResolveCommand.cs

@@ -13,7 +13,7 @@ public static Command Create() {
       result.AddOption(option);
     }
     DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, async (options, _) => {
-      options.Set(DafnyFile.DoNotVerifyDependencies, true);
+      options.Set(DafnyFile.UnsafeDependencies, true);
       var compilation = CliCompilation.Create(options);
       compilation.Start();
       await compilation.Resolution;

Source/DafnyDriver/Commands/ServerCommand.cs

@@ -32,7 +32,7 @@ private static Command Create() {
       result.Add(option);
     }
     DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, async (options, context) => {
-      options.Set(DafnyFile.DoNotVerifyDependencies, true);
+      options.Set(DafnyFile.UnsafeDependencies, true);
       LanguageServer.ConfigureDafnyOptionsForServer(options);
       await LanguageServer.Start(options);
       return 0;

Source/DafnyDriver/Commands/VerifyCommand.cs

@@ -42,7 +42,7 @@ public static Command Create() {
     new Option[] {
         FilterSymbol,
         FilterPosition,
-        DafnyFile.DoNotVerifyDependencies
+        DafnyFile.UnsafeDependencies
       }.Concat(DafnyCommands.VerificationOptions).
       Concat(DafnyCommands.ConsoleOutputOptions).
       Concat(DafnyCommands.ResolverOptions);

Source/DafnyDriver/DafnyNewCli.cs

@@ -277,7 +277,7 @@ private static async IAsyncEnumerable<DafnyFile> HandleDafnyProject(IFileSystem
           { CommonOptionBag.Libraries, OptionCompatibility.NoOpOptionCheck }
         });
     if (dependencyOptions != null) {
-      if (options.Get(DafnyFile.DoNotVerifyDependencies) || !options.Verify) {
+      if (options.Get(DafnyFile.UnsafeDependencies) || !options.Verify) {
         foreach (var libraryRootSetFile in dependencyProject.GetRootSourceUris(fileSystem)) {
           var file = DafnyFile.HandleDafnyFile(fileSystem, reporter, dependencyOptions, libraryRootSetFile,
             dependencyProject.StartingToken, true, false);

Source/DafnyLanguageServer.Test/Diagnostics/ProjectFileDiagnosticsTest.cs

@@ -32,10 +32,11 @@ public async Task ProjectFileErrorIsShownFromDafnyFile() {
     var projectFilePath = Path.Combine(directory, DafnyProject.FileName);
     await File.WriteAllTextAsync(projectFilePath, projectFileSource);
     await CreateOpenAndWaitForResolve("method Foo() { }", Path.Combine(directory, "ProjectFileErrorIsShownFromDafnyFile.dfy"));
-    var diagnostics = await diagnosticsReceiver.AwaitNextNotificationAsync(CancellationToken);
+    var diagnostics = (await diagnosticsReceiver.AwaitNextNotificationAsync(CancellationToken));
+    var errors = diagnostics.Diagnostics.Where(d => d.Severity == DiagnosticSeverity.Error).ToList();
     Assert.Equal(DocumentUri.File(projectFilePath), diagnostics.Uri.GetFileSystemPath());
-    Assert.Single(diagnostics.Diagnostics);
-    Assert.Contains(diagnostics.Diagnostics, d => d.Message.Contains("Unexpected token"));
+    Assert.Single(errors);
+    Assert.Contains(errors, d => d.Message.Contains("Unexpected token"));
   }
 
   [Fact]

Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs

@@ -82,8 +82,9 @@ public async Task ProjectFileByItselfDiagnostics() {
     var tempDirectory = Path.GetRandomFileName();
     var projectFile = await CreateOpenAndWaitForResolve("", Path.Combine(tempDirectory, DafnyProject.FileName));
     var diagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken);
-    Assert.Single(diagnostics);
-    Assert.Equal("no Dafny source files were specified as input", diagnostics.First().Message);
+    var errors = diagnostics.Where(d => d.Severity == DiagnosticSeverity.Error).ToList();
+    Assert.Single(errors);
+    Assert.Equal("no Dafny source files were specified as input", errors.First().Message);
   }
 
   [Fact]