Improve performance for large projects (dafny-lang#4419)

### Changes
- Sample sending notifications to the IDE, so at most one is sent every
100ms. Relatedly, `IdeState` is computed lazily, so it not computed for
notifications that are not sent to the IDE.
- Cancel ongoing compilation work and notification publishing
immediately when UpdateDocument is entered
- Start a new compilation slightly earlier, before computing the most
recently changed ranges
- Fix migration of recently changed ranges, so it properly accounts for
Uri differences.
- Make sure only one (correct) version of `WriterFromOutputHelper` is
used in all test projects, to help in debugging non-deterministic
failures
- Small changes to `IncrementalVerificationDiagnosticsBetweenMethods` to
help in debugging non-deterministic failures

### Testing
- Add a test `QuickEditsInLargeFile` with a 1000 line and method file,
that instantly makes a 100 small edits to that file, and asserts that
the language server can process these changes in at most three times as
much time as it takes to open the file.

<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.Test/NodeTests.cs

@@ -1,7 +1,7 @@
 using System.Collections.Concurrent;
 using Microsoft.Dafny;
 
-namespace DafnyCore.Test; 
+namespace DafnyCore.Test;
 
 public class NodeTests {
 

Source/DafnyTestGeneration.Test/WriterFromOutputHelper.cs → Source/DafnyCore.Test/WriterFromOutputHelper.cs

@@ -1,13 +1,8 @@
-// Copyright by the contributors to the Dafny Project
-// SPDX-License-Identifier: MIT
-
-#nullable disable
-using System.IO;
+#nullable enable
 using System.Text;
-using Microsoft.Extensions.Primitives;
 using Xunit.Abstractions;
 
-namespace DafnyTestGeneration.Test;
+namespace DafnyCore.Test;
 
 public class WriterFromOutputHelper : TextWriter {
  private readonly StringBuilder buffer = new();
@@ -17,7 +12,7 @@ public WriterFromOutputHelper(ITestOutputHelper output) {
  this.output = output;
  }
 
- public override void Write(string value) {
+ public override void Write(string? value) {
  if (value != null) {
  buffer.Append(value);
  }
@@ -29,12 +24,12 @@ public override void Write(char value) {
 
  public override Encoding Encoding => Encoding.Default;
 
- public override void WriteLine(string value) {
+ public override void WriteLine(string? value) {
  output.WriteLine(buffer + value);
  buffer.Clear();
  }
 
- public override void WriteLine(string format, params object[] arg) {
+ public override void WriteLine(string format, params object?[] arg) {
  output.WriteLine(buffer + format, arg);
  buffer.Clear();
  }

Source/DafnyCore/DafnyFile.cs

@@ -1,7 +1,6 @@
 using System;
 using System.Collections.Generic;
 using System.IO;
-using System.Linq;
 using System.Reflection.Metadata;
 using System.Reflection.PortableExecutable;
 using DafnyCore;

Source/DafnyCore/Options/DafnyProject.cs

@@ -56,37 +56,67 @@ public IEnumerable<Uri> GetRootSourceUris(IFileSystem fileSystem) {
  if (!Uri.IsFile) {
  return new[] { Uri };
  }
+ var matcher = GetMatcher(out var searchRoot);
 
- var matcher = GetMatcher();
-
- var diskRoot = Path.GetPathRoot(Uri.LocalPath);
- var result = matcher.Execute(fileSystem.GetDirectoryInfoBase(diskRoot));
- var files = result.Files.Select(f => Path.Combine(diskRoot, f.Path));
+ var result = matcher.Execute(fileSystem.GetDirectoryInfoBase(searchRoot));
+ var files = result.Files.Select(f => Path.Combine(searchRoot, f.Path));
  return files.Select(file => new Uri(Path.GetFullPath(file)));
  }
 
  public bool ContainsSourceFile(Uri uri) {
- var fileSystemWithSourceFile = new InMemoryDirectoryInfoFromDotNet8(Path.GetPathRoot(uri.LocalPath)!, new[] { uri.LocalPath });
- return GetMatcher().Execute(fileSystemWithSourceFile).HasMatches;
+ var matcher = GetMatcher(out var searchRoot);
+ var fileSystemWithSourceFile = new InMemoryDirectoryInfoFromDotNet8(searchRoot, new[] { uri.LocalPath });
+ return matcher.Execute(fileSystemWithSourceFile).HasMatches;
  }
 
- private Matcher GetMatcher() {
+ private Matcher GetMatcher(out string commonRoot) {
  var projectRoot = Path.GetDirectoryName(Uri.LocalPath)!;
- var root = Path.GetPathRoot(Uri.LocalPath)!;
+ var diskRoot = Path.GetPathRoot(Uri.LocalPath)!;
+
+ var includes = Includes ?? new[] { "**/*.dfy" };
+ var excludes = Excludes ?? Array.Empty<string>();
+ var fullPaths = includes.Concat(excludes).Select(p => Path.GetFullPath(p, projectRoot)).ToList();
+ commonRoot = GetCommonParentDirectory(fullPaths) ?? diskRoot;
  var matcher = new Matcher();
- foreach (var includeGlob in Includes ?? new[] { "**/*.dfy" }) {
- var fullPath = Path.GetFullPath(includeGlob, projectRoot);
- matcher.AddInclude(Path.GetRelativePath(root, fullPath));
+ foreach (var includeGlob in includes) {
+ matcher.AddInclude(Path.GetRelativePath(commonRoot, Path.GetFullPath(includeGlob, projectRoot)));
  }
 
- foreach (var includeGlob in Excludes ?? Enumerable.Empty<string>()) {
- var fullPath = Path.GetFullPath(includeGlob, projectRoot);
- matcher.AddExclude(Path.GetRelativePath(root, fullPath));
+ foreach (var excludeGlob in excludes) {
+ matcher.AddExclude(Path.GetRelativePath(commonRoot, Path.GetFullPath(excludeGlob, projectRoot)));
  }
 
  return matcher;
  }
 
+ string GetCommonParentDirectory(IReadOnlyList<string> strings) {
+ if (!strings.Any()) {
+ return null;
+ }
+ var commonPrefix = strings.FirstOrDefault() ?? "";
+
+ foreach (var newString in strings) {
+ var potentialMatchLength = Math.Min(newString.Length, commonPrefix.Length);
+
+ if (potentialMatchLength < commonPrefix.Length) {
+ commonPrefix = commonPrefix.Substring(0, potentialMatchLength);
+ }
+
+ for (var i = 0; i < potentialMatchLength; i++) {
+ if (newString[i] == '*' || newString[i] != commonPrefix[i]) {
+ commonPrefix = commonPrefix.Substring(0, i);
+ break;
+ }
+ }
+ }
+
+ if (!Path.EndsInDirectorySeparator(commonPrefix)) {
+ commonPrefix = Path.GetDirectoryName(commonPrefix);
+ }
+
+ return commonPrefix;
+ }
+
  public void Validate(TextWriter outputWriter, IEnumerable<Option> possibleOptions) {
  if (Options == null) {
  return;

Source/DafnyDriver/DafnyDoc.cs

@@ -50,8 +50,6 @@ public static DafnyDriver.ExitValue DoDocumenting(IReadOnlyList<DafnyFile> dafny
  outputdir = DefaultOutputDir;
  }
 
-
-
  // Collect all the dafny files; dafnyFiles already includes files from a .toml project file
  var exitValue = DafnyDriver.ExitValue.SUCCESS;
  dafnyFiles = dafnyFiles.Concat(dafnyFolders.SelectMany(folderPath => {

Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj

@@ -10,7 +10,7 @@
  <PackageReference Include="DiffPlex" Version="1.7.0" />
  <PackageReference Include="Microsoft.CodeAnalysis.CSharp" Version="3.7.0" />
  <PackageReference Include="Microsoft.Extensions.Logging.Console" Version="5.0.0" />
- <PackageReference Include="Microsoft.NET.Test.Sdk" Version="16.11.0" />
+ <PackageReference Include="Microsoft.NET.Test.Sdk" Version="17.1.0" />
  <PackageReference Include="Moq" Version="4.16.1" />
  <PackageReference Include="Serilog.Sinks.InMemory" Version="0.11.0" />
  <PackageReference Include="xunit" Version="2.4.2" />
@@ -25,6 +25,7 @@
  </ItemGroup>
 
  <ItemGroup>
+ <ProjectReference Include="..\DafnyCore.Test\DafnyCore.Test.csproj" />
  <ProjectReference Include="..\DafnyLanguageServer\DafnyLanguageServer.csproj" />
  </ItemGroup>
 

Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs

@@ -16,6 +16,7 @@
 using System.Linq;
 using System.Threading;
 using System.Threading.Tasks;
+using DafnyCore.Test;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Various;
 using Microsoft.Dafny.LanguageServer.Language;
 using OmniSharp.Extensions.LanguageServer.Client;
@@ -94,6 +95,7 @@ public AnonymousDisposable(Action action) {
 
  private Action<LanguageServerOptions> GetServerOptionsAction(Action<DafnyOptions> modifyOptions) {
  var dafnyOptions = DafnyOptions.Create(output);
+ dafnyOptions.Set(ServerCommand.UpdateThrottling, 0);
  modifyOptions?.Invoke(dafnyOptions);
  ServerCommand.ConfigureDafnyOptionsForServer(dafnyOptions);
  ApplyDefaultOptionValues(dafnyOptions);

Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs

@@ -0,0 +1,111 @@
+using System;
+using System.Text;
+using System.Threading;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Xunit;
+using Xunit.Abstractions;
+using Xunit.Sdk;
+using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Performance;
+
+public class LargeFilesTest : ClientBasedLanguageServerTest {
+ protected override Task SetUp(Action<DafnyOptions> modifyOptions) {
+ return base.SetUp(options => {
+ modifyOptions?.Invoke(options);
+ options.Set(ServerCommand.UpdateThrottling, ServerCommand.DefaultThrottleTime);
+ });
+ }
+
+ /// <summary>
+ /// This test should complete in less than a second, because it opens a moderately sized file
+ /// on which it makes edits so quickly that the edits should all be processed in a single compilation.
+ /// And a single compilation should complete in less than 200ms.
+ ///
+ /// Right now the test still takes more than 5 seconds.
+ /// To reduce runtime of this test,
+ /// remove ReportRealtimeDiagnostics (since it is called 10 times for each update,
+ /// and calls InitialIdeState, which often calls CompilationAfterResolution.ToIdeState (expensive))
+ /// </summary>
+ [Fact]
+ public async Task QuickEditsInLargeFile() {
+ string GetLineContent(int index) => $"method Foo{index}() {{ assume false; }}";
+ var contentBuilder = new StringBuilder();
+ for (int lineNumber = 0; lineNumber < 1000; lineNumber++) {
+ contentBuilder.AppendLine(GetLineContent(lineNumber));
+ }
+ var source = contentBuilder.ToString();
+
+ double lowest = double.MaxValue;
+ Exception lastException = null;
+ try {
+ for (int attempt = 0; attempt < 10; attempt++) {
+ var cancelSource = new CancellationTokenSource();
+ var measurementTask = AssertThreadPoolIsAvailable(cancelSource.Token);
+ var beforeOpen = DateTime.Now;
+ var documentItem = await CreateAndOpenTestDocument(source, "ManyFastEditsUsingLargeFiles.dfy",
+ cancellationToken: CancellationTokenWithHighTimeout);
+ var afterOpen = DateTime.Now;
+ var openMilliseconds = (afterOpen - beforeOpen).TotalMilliseconds;
+ for (int i = 0; i < 100; i++) {
+ ApplyChange(ref documentItem, new Range(0, 0, 0, 0), "// added this comment\n");
+ }
+
+ await client.WaitForNotificationCompletionAsync(documentItem.Uri, CancellationTokenWithHighTimeout);
+ var afterChange = DateTime.Now;
+ var changeMilliseconds = (afterChange - afterOpen).TotalMilliseconds;
+ await AssertNoDiagnosticsAreComing(CancellationTokenWithHighTimeout);
+ cancelSource.Cancel();
+ var averageTimeToSchedule = await measurementTask;
+ var division = changeMilliseconds / openMilliseconds;
+ lowest = Math.Min(lowest, division);
+
+ // Commented code left in intentionally
+ // await output.WriteLineAsync("openMilliseconds: " + openMilliseconds);
+ // await output.WriteLineAsync("changeMilliseconds: " + changeMilliseconds);
+ // await output.WriteLineAsync("division: " + division);
+ try {
+ Assert.True(averageTimeToSchedule < 100);
+ // Migration should be constant time, which would allow this number to be about 1.
+ // Right now migration is still slow so this has been set to 10 so the test can pass.
+ var changeTimeMultiplier = 15;
+ Assert.True(division < changeTimeMultiplier,
+ $"changeMilliseconds {changeMilliseconds}, openMilliseconds {openMilliseconds}");
+
+ return;
+ } catch (AssertActualExpectedException e) {
+ lastException = e;
+ }
+ }
+ } catch (OperationCanceledException) {
+ }
+
+ await output.WriteLineAsync("lowest division " + lowest);
+ throw lastException!;
+ }
+
+ private async Task<double> AssertThreadPoolIsAvailable(CancellationToken durationToken) {
+ int ticks = 0;
+ var waitTime = 100;
+ var start = DateTime.Now;
+ while (!durationToken.IsCancellationRequested) {
+ await Task.Run(() => {
+ Thread.Sleep(waitTime);
+ });
+ ticks++;
+ }
+
+ var end = DateTime.Now;
+ var span = end - start;
+ var totalSleepTime = ticks * waitTime;
+ var totalSchedulingTime = span.TotalMilliseconds - totalSleepTime;
+ var averageTimeToSchedule = totalSchedulingTime / ticks;
+ // await output.WriteLineAsync($"averageTimeToSchedule: {averageTimeToSchedule:0.##}");
+ return averageTimeToSchedule;
+ }
+
+ public LargeFilesTest(ITestOutputHelper output) : base(output) {
+ }
+}

Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs

@@ -99,23 +99,30 @@ method Foo() {
  }
 
  [Fact]
- public async Task FileOnlyAttachedToProjectFileThatAppliesToIt() {
+ public async Task FileOnlyAttachedToProjectFileThatIncludesIt() {
  await SetUp(options => options.WarnShadowing = false);
 
- var projectFileSource = @"
+ var outerSource = @"
 [options]
 warn-shadowing = true
 ";
  var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
- var outerProjectFile = CreateTestDocument(projectFileSource, Path.Combine(directory, DafnyProject.FileName));
+ var outerProjectFile = CreateTestDocument(outerSource, Path.Combine(directory, DafnyProject.FileName));
  await client.OpenDocumentAndWaitAsync(outerProjectFile, CancellationToken);
 
- var innerProjectFile = CreateTestDocument("includes = []", Path.Combine(directory, "nested", DafnyProject.FileName));
+ var innerDirectory = Path.Combine(directory, "nested");
+ var innerProjectFile = CreateTestDocument("includes = []", Path.Combine(innerDirectory, DafnyProject.FileName));
  await client.OpenDocumentAndWaitAsync(innerProjectFile, CancellationToken);
 
- var filePath = Path.Combine(Directory.GetCurrentDirectory(), "ProjectFiles/TestFiles/noWarnShadowing.dfy");
- var source = await File.ReadAllTextAsync(filePath);
- var documentItem = CreateTestDocument(source, Path.Combine(directory, "nested/A.dfy"));
+ var source = @"
+method Foo() {
+ var x := 3;
+ if (true) {
+ var x := 4;
+ }
+}
+";
+ var documentItem = CreateTestDocument(source, Path.Combine(innerDirectory, "A.dfy"));
  await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
  var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken);
  Assert.Single(diagnostics);

Source/DafnyLanguageServer.Test/StandaloneServerTest.cs

@@ -1,6 +1,7 @@
 using System;
 using System.IO;
 using System.Text;
+using DafnyCore.Test;
 using Microsoft.Dafny.LanguageServer.Workspace;
 using Xunit.Abstractions;
 using Xunit;
@@ -21,29 +22,3 @@ public void OptionParsing() {
  Assert.Equal(VerifyOnMode.Save, options.Get(ServerCommand.Verification));
  }
 }
-
-public class WriterFromOutputHelper : TextWriter {
- private readonly ITestOutputHelper output;
- private bool failed = false;
-
- public WriterFromOutputHelper(ITestOutputHelper output) {
- this.output = output;
- }
-
- public override void Write(char value) {
- if (!failed) {
- failed = true;
- WriteLine("Error: tried to write a single character, which WriterFromOutputHelper does not support.");
- }
- }
-
- public override Encoding Encoding => Encoding.Default;
-
- public override void WriteLine(string value) {
- output.WriteLine(value);
- }
-
- public override void WriteLine(string format, params object[] arg) {
- output.WriteLine(format, arg);
- }
-}

Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs

@@ -924,16 +924,17 @@ method test() {
 ".TrimStart();
  var documentItem = CreateTestDocument(source, "IncrementalVerificationDiagnosticsBetweenMethods.dfy");
  client.OpenDocument(documentItem);
- var firstVerificationDiagnostics = await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem);
+ var firstVerificationDiagnostics = await diagnosticsReceiver.AwaitNextNotificationAsync(CancellationToken);
  try {
  var secondVerificationDiagnostics =
  await diagnosticsReceiver.AwaitNextDiagnosticsAsync(CancellationToken, documentItem);
 
- Assert.Single(firstVerificationDiagnostics);
+ Assert.Single(firstVerificationDiagnostics.Diagnostics);
  // Second diagnostic is a timeout exception from SlowToVerify
  Assert.Equal(2, secondVerificationDiagnostics.Length);
  } catch (OperationCanceledException) {
  await output.WriteLineAsync($"firstVerificationDiagnostics: {firstVerificationDiagnostics.Stringify()}");
+ WriteVerificationHistory();
  }
  await AssertNoDiagnosticsAreComing(CancellationToken);
  }