From c5473368539d494e35ed5c06d0597d37ecdde3c9 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Thu, 24 Aug 2023 16:06:36 +0200
Subject: [PATCH] Improve performance for large projects (#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            |   2 +-
 .../WriterFromOutputHelper.cs                 |  15 +--
 Source/DafnyCore/DafnyFile.cs                 |   1 -
 Source/DafnyCore/Options/DafnyProject.cs      |  60 +++++++---
 Source/DafnyDriver/DafnyDoc.cs                |   2 -
 .../DafnyLanguageServer.Test.csproj           |   3 +-
 .../DafnyLanguageServerTestBase.cs            |   2 +
 .../Performance/LargeFilesTest.cs             | 111 ++++++++++++++++++
 .../ProjectFiles/ProjectFilesTest.cs          |  21 ++--
 .../StandaloneServerTest.cs                   |  27 +----
 .../Synchronization/DiagnosticsTest.cs        |   5 +-
 .../Unit/GhostStateDiagnosticCollectorTest.cs |   3 +-
 .../Unit/TextDocumentLoaderTest.cs            |   5 +-
 .../Util/ClientBasedLanguageServerTest.cs     |   6 +-
 .../Util/Stringify.cs                         |   1 +
 .../Util/TestNotificationReceiver.cs          |   2 +-
 .../Various/ExceptionTests.cs                 |   6 +-
 .../DafnyLanguageServer.cs                    |   3 -
 .../Language/CachingParser.cs                 |   1 -
 .../Language/IVerificationProgressReporter.cs |   2 +-
 .../Language/LanguageServerExtensions.cs      |   1 -
 Source/DafnyLanguageServer/ServerCommand.cs   |  10 +-
 .../Workspace/CompilationManager.cs           |  21 +++-
 .../Workspace/Documents/Compilation.cs        |   2 +-
 .../Documents/CompilationAfterParsing.cs      |   4 +-
 .../Documents/CompilationAfterResolution.cs   |   5 +-
 .../Workspace/ITextDocumentLoader.cs          |   4 +-
 .../DafnyLanguageServer/Workspace/IdeState.cs |  42 ++++++-
 .../Workspace/IdeStateObserver.cs             |  73 +++---------
 .../Workspace/ProjectManager.cs               |  58 +++++----
 .../Workspace/TextDocumentLoader.cs           |  13 +-
 .../Workspace/VerificationProgressReporter.cs |  18 ++-
 .../DafnyPipeline.Test.csproj                 |   3 +-
 Source/DafnyPipeline.Test/DocstringTest.cs    |   4 +-
 .../DafnyPipeline.Test/FormatterBaseTest.cs   |   1 +
 .../IntraMethodVerificationStability.cs       |   9 +-
 Source/DafnyPipeline.Test/Issue1355.cs        |   1 +
 Source/DafnyPipeline.Test/PluginsTest.cs      |   1 +
 Source/DafnyPipeline.Test/RelativePaths.cs    |   1 +
 Source/DafnyPipeline.Test/Trivia.cs           |   1 +
 .../WriterFromOutputHelper.cs                 |  30 -----
 Source/DafnyTestGeneration.Test/BasicTypes.cs |   1 +
 .../DafnyTestGeneration.Test/Collections.cs   |   1 +
 .../DafnyTestGeneration.Test.csproj           |   3 +-
 .../ShortCircuitRemoval.cs                    |   1 +
 Source/DafnyTestGeneration.Test/Various.cs    |   1 +
 46 files changed, 359 insertions(+), 228 deletions(-)
 rename Source/{DafnyTestGeneration.Test => DafnyCore.Test}/WriterFromOutputHelper.cs (66%)
 create mode 100644 Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs
 delete mode 100644 Source/DafnyPipeline.Test/WriterFromOutputHelper.cs

diff --git a/Source/DafnyCore.Test/NodeTests.cs b/Source/DafnyCore.Test/NodeTests.cs
index e4a52d860f1..3e376b0b253 100644
--- a/Source/DafnyCore.Test/NodeTests.cs
+++ b/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 {
 
diff --git a/Source/DafnyTestGeneration.Test/WriterFromOutputHelper.cs b/Source/DafnyCore.Test/WriterFromOutputHelper.cs
similarity index 66%
rename from Source/DafnyTestGeneration.Test/WriterFromOutputHelper.cs
rename to Source/DafnyCore.Test/WriterFromOutputHelper.cs
index 8448d66eb33..dcc5aed0027 100644
--- a/Source/DafnyTestGeneration.Test/WriterFromOutputHelper.cs
+++ b/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();
   }
diff --git a/Source/DafnyCore/DafnyFile.cs b/Source/DafnyCore/DafnyFile.cs
index 47800c4ae4d..af67b09e0f5 100644
--- a/Source/DafnyCore/DafnyFile.cs
+++ b/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;
diff --git a/Source/DafnyCore/Options/DafnyProject.cs b/Source/DafnyCore/Options/DafnyProject.cs
index f1ad8784bc3..8576c45e229 100644
--- a/Source/DafnyCore/Options/DafnyProject.cs
+++ b/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;
diff --git a/Source/DafnyDriver/DafnyDoc.cs b/Source/DafnyDriver/DafnyDoc.cs
index 443b9272e9b..2632b14102f 100644
--- a/Source/DafnyDriver/DafnyDoc.cs
+++ b/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 => {
diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj
index 392fa360a6c..a21d680f516 100644
--- a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj
+++ b/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>
 
diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs
index e75822dca20..674cc84af66 100644
--- a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs
+++ b/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);
diff --git a/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs b/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs
new file mode 100644
index 00000000000..f86ec852db6
--- /dev/null
+++ b/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) {
+  }
+}
\ No newline at end of file
diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs
index 5a57a327cec..0da11b10df7 100644
--- a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs
+++ b/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);
diff --git a/Source/DafnyLanguageServer.Test/StandaloneServerTest.cs b/Source/DafnyLanguageServer.Test/StandaloneServerTest.cs
index f5c8f9b8021..7d7bbdc0f14 100644
--- a/Source/DafnyLanguageServer.Test/StandaloneServerTest.cs
+++ b/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);
-  }
-}
diff --git a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs
index 26d41264810..1e127fe5326 100644
--- a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs
+++ b/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);
     }
diff --git a/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs b/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs
index 92ca320393f..b8f3441f1f2 100644
--- a/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs
+++ b/Source/DafnyLanguageServer.Test/Unit/GhostStateDiagnosticCollectorTest.cs
@@ -4,6 +4,7 @@
 using System.IO;
 using System.Linq;
 using System.Threading;
+using DafnyCore.Test;
 using IntervalTree;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
@@ -32,7 +33,7 @@ public IDisposable BeginScope<TState>(TState state) {
   }
 
   public GhostStateDiagnosticCollectorTest(ITestOutputHelper output) {
-    var options = new DafnyOptions(TextReader.Null, new WriterFromOutputHelper(output), new WriterFromOutputHelper(output));
+    var options = new DafnyOptions(TextReader.Null, (TextWriter)new WriterFromOutputHelper(output), (TextWriter)new WriterFromOutputHelper(output));
     options.Set(ServerCommand.GhostIndicators, true);
     ghostStateDiagnosticCollector = new GhostStateDiagnosticCollector(
       options,
diff --git a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs
index c18ccd95afa..354348a5db1 100644
--- a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs
+++ b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs
@@ -8,6 +8,7 @@
 using System.IO;
 using System.Threading;
 using System.Threading.Tasks;
+using DafnyCore.Test;
 using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol;
@@ -67,7 +68,7 @@ public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() {
           It.IsAny<ErrorReporter>(),
           It.IsAny<CancellationToken>())).Callback(() => source.Cancel())
         .Throws<TaskCanceledException>();
-      var task = textDocumentLoader.ParseAsync(DafnyOptions.Default, GetCompilation(), ImmutableDictionary<Uri, VerificationTree>.Empty, source.Token);
+      var task = textDocumentLoader.ParseAsync(DafnyOptions.Default, GetCompilation(), ImmutableDictionary<Uri, DocumentVerificationTree>.Empty, source.Token);
       try {
         await task;
         Assert.Fail("document load was not cancelled");
@@ -90,7 +91,7 @@ public async Task LoadReturnsFaultedTaskIfAnyExceptionOccured() {
           It.IsAny<ErrorReporter>(),
           It.IsAny<CancellationToken>()))
         .Throws<InvalidOperationException>();
-      var task = textDocumentLoader.ParseAsync(DafnyOptions.Default, GetCompilation(), ImmutableDictionary<Uri, VerificationTree>.Empty, default);
+      var task = textDocumentLoader.ParseAsync(DafnyOptions.Default, GetCompilation(), ImmutableDictionary<Uri, DocumentVerificationTree>.Empty, default);
       try {
         await task;
         Assert.Fail("document load did not fail");
diff --git a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs
index 13c7c976aa9..377d22b14bd 100644
--- a/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs
+++ b/Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs
@@ -47,9 +47,9 @@ protected ClientBasedLanguageServerTest(ITestOutputHelper output, LogLevel dafny
   }
 
   protected async Task<TextDocumentItem> CreateAndOpenTestDocument(string source, string filePath = null,
-    int version = 1) {
+    int version = 1, CancellationToken? cancellationToken = null) {
     var document = CreateTestDocument(source, filePath, version);
-    await client.OpenDocumentAndWaitAsync(document, CancellationToken);
+    await client.OpenDocumentAndWaitAsync(document, cancellationToken ?? CancellationToken);
     return document;
   }
 
@@ -298,7 +298,7 @@ public async Task AssertNoDiagnosticsAreComing(CancellationToken cancellationTok
       }
     }
     var verificationDocumentItem = CreateTestDocument("class X {does not parse", $"AssertNoDiagnosticsAreComing{fileIndex++}.dfy");
-    await client.OpenDocumentAndWaitAsync(verificationDocumentItem, CancellationToken);
+    await client.OpenDocumentAndWaitAsync(verificationDocumentItem, cancellationToken);
     var resolutionReport = await diagnosticsReceiver.AwaitNextNotificationAsync(cancellationToken);
     AssertM.Equal(verificationDocumentItem.Uri, resolutionReport.Uri,
       "1) Unexpected diagnostics were received whereas none were expected:\n" +
diff --git a/Source/DafnyLanguageServer.Test/Util/Stringify.cs b/Source/DafnyLanguageServer.Test/Util/Stringify.cs
index ab123ea7a96..073e65b9d40 100644
--- a/Source/DafnyLanguageServer.Test/Util/Stringify.cs
+++ b/Source/DafnyLanguageServer.Test/Util/Stringify.cs
@@ -80,6 +80,7 @@ void Helper(ImmutableHashSet<object> visited, object? value, int indentation) {
     }
 
     Helper(ImmutableHashSet.Create<object>(), root, 0);
+    writer.Flush();
   }
 
   public static string Stringify(this object root, bool showNullChildren = false) {
diff --git a/Source/DafnyLanguageServer.Test/Util/TestNotificationReceiver.cs b/Source/DafnyLanguageServer.Test/Util/TestNotificationReceiver.cs
index 1e9fe25f081..a9e966bfa4d 100644
--- a/Source/DafnyLanguageServer.Test/Util/TestNotificationReceiver.cs
+++ b/Source/DafnyLanguageServer.Test/Util/TestNotificationReceiver.cs
@@ -15,6 +15,7 @@ public class TestNotificationReceiver<TNotification> {
 
     public void NotificationReceived(TNotification request) {
       notifications.Enqueue(request);
+      notificationHistory.Add(request);
       availableNotifications.Release();
     }
 
@@ -29,7 +30,6 @@ public void ClearHistory() {
     public async Task<TNotification> AwaitNextNotificationAsync(CancellationToken cancellationToken) {
       await availableNotifications.WaitAsync(cancellationToken);
       if (notifications.TryDequeue(out var notification)) {
-        notificationHistory.Add(notification);
         return notification;
       }
       throw new System.InvalidOperationException("got a signal for a received notification but it was not present in the queue");
diff --git a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs
index 0bd90df8ebb..15c290ccf61 100644
--- a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs
+++ b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs
@@ -119,12 +119,12 @@ public IdeState CreateUnloaded(Compilation compilation) {
     }
 
     public Task<CompilationAfterParsing> ParseAsync(DafnyOptions options, Compilation compilation,
-      IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees, CancellationToken cancellationToken) {
-      return loader.ParseAsync(options, compilation, ImmutableDictionary<Uri, VerificationTree>.Empty, cancellationToken);
+      IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees, CancellationToken cancellationToken) {
+      return loader.ParseAsync(options, compilation, ImmutableDictionary<Uri, DocumentVerificationTree>.Empty, cancellationToken);
     }
 
     public Task<CompilationAfterResolution> ResolveAsync(DafnyOptions options, CompilationAfterParsing compilation,
-      IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees, CancellationToken cancellationToken) {
+      IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees, CancellationToken cancellationToken) {
       if (tests.CrashOnLoad) {
         throw new IOException("testing crash");
       }
diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.cs b/Source/DafnyLanguageServer/DafnyLanguageServer.cs
index 9d9c50304a8..5c7162911aa 100644
--- a/Source/DafnyLanguageServer/DafnyLanguageServer.cs
+++ b/Source/DafnyLanguageServer/DafnyLanguageServer.cs
@@ -1,11 +1,9 @@
 using System;
-using System.Collections.Generic;
 using System.Diagnostics;
 using System.Text.RegularExpressions;
 using Microsoft.Dafny.LanguageServer.Handlers;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Workspace;
-using Microsoft.Extensions.Configuration;
 using Microsoft.Extensions.DependencyInjection;
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
@@ -14,7 +12,6 @@
 using System.Threading;
 using System.Threading.Tasks;
 using Microsoft.Boogie.SMTLib;
-using Microsoft.Extensions.Options;
 using Action = System.Action;
 
 namespace Microsoft.Dafny.LanguageServer {
diff --git a/Source/DafnyLanguageServer/Language/CachingParser.cs b/Source/DafnyLanguageServer/Language/CachingParser.cs
index d89aa103164..74397d15705 100644
--- a/Source/DafnyLanguageServer/Language/CachingParser.cs
+++ b/Source/DafnyLanguageServer/Language/CachingParser.cs
@@ -28,7 +28,6 @@ public override Program ParseFiles(string programName, IReadOnlyList<DafnyFile>
 
   protected override DfyParseResult ParseFile(DafnyOptions options, Func<TextReader> getReader,
     Uri uri, CancellationToken cancellationToken) {
-
     using var reader = getReader();
     var (newReader, hash) = ComputeHashFromReader(uri, reader, HashAlgorithm.Create("SHA256")!);
     if (!parseCache.TryGet(hash, out var result)) {
diff --git a/Source/DafnyLanguageServer/Language/IVerificationProgressReporter.cs b/Source/DafnyLanguageServer/Language/IVerificationProgressReporter.cs
index b0f13d032ac..0e253f5c81d 100644
--- a/Source/DafnyLanguageServer/Language/IVerificationProgressReporter.cs
+++ b/Source/DafnyLanguageServer/Language/IVerificationProgressReporter.cs
@@ -7,7 +7,7 @@ namespace Microsoft.Dafny.LanguageServer.Language {
   /// A callback interface to report verification progress
   /// </summary>
   public interface IVerificationProgressReporter {
-    void RecomputeVerificationTrees(CompilationAfterResolution compilation);
+    void RecomputeVerificationTrees(CompilationAfterParsing compilation);
     void ReportRealtimeDiagnostics(CompilationAfterParsing compilation, Uri uri, bool verificationStarted);
 
     void ReportImplementationsBeforeVerification(CompilationAfterResolution compilation, ICanVerify canVerify, Implementation[] implementations);
diff --git a/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs b/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs
index 007daa89941..8ab2b9c92c2 100644
--- a/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs
+++ b/Source/DafnyLanguageServer/Language/LanguageServerExtensions.cs
@@ -38,7 +38,6 @@ private static IServiceCollection WithDafnyLanguage(this IServiceCollection serv
           new IdeStateObserver(serviceProvider.GetRequiredService<ILogger<IdeStateObserver>>(),
             serviceProvider.GetRequiredService<ITelemetryPublisher>(),
             serviceProvider.GetRequiredService<INotificationPublisher>(),
-            serviceProvider.GetRequiredService<ITextDocumentLoader>(),
             compilation))
         .AddSingleton<IVerificationProgressReporter, VerificationProgressReporter>()
         .AddSingleton(CreateVerifier)
diff --git a/Source/DafnyLanguageServer/ServerCommand.cs b/Source/DafnyLanguageServer/ServerCommand.cs
index cb32f591ac0..96fb33032aa 100644
--- a/Source/DafnyLanguageServer/ServerCommand.cs
+++ b/Source/DafnyLanguageServer/ServerCommand.cs
@@ -7,6 +7,7 @@
 namespace Microsoft.Dafny.LanguageServer;
 
 public class ServerCommand : ICommandSpec {
+  public const int DefaultThrottleTime = 100;
   public static readonly ServerCommand Instance = new();
 
   private ServerCommand() {
@@ -20,7 +21,8 @@ static ServerCommand() {
       GhostIndicators,
       LineVerificationStatus,
       VerifySnapshots,
-      UseCaching
+      UseCaching,
+      UpdateThrottling
     );
   }
 
@@ -29,6 +31,11 @@ static ServerCommand() {
     IsHidden = true
   };
 
+  public static readonly Option<int> UpdateThrottling = new("--update-throttling", () => DefaultThrottleTime,
+    @"How many milliseconds the server will wait before sending new document updates to the client. Higher values reduce bandwidth at the cost of responsiveness".TrimStart()) {
+    IsHidden = true
+  };
+
   public static readonly Option<bool> GhostIndicators = new("--notify-ghostness",
     @"
 (experimental, API will change)
@@ -64,6 +71,7 @@ related locations
     LineVerificationStatus,
     VerifySnapshots,
     UseCaching,
+    UpdateThrottling,
     DeveloperOptionBag.BoogiePrint,
     CommonOptionBag.EnforceDeterminism,
     CommonOptionBag.UseJavadocLikeDocstringRewriterOption
diff --git a/Source/DafnyLanguageServer/Workspace/CompilationManager.cs b/Source/DafnyLanguageServer/Workspace/CompilationManager.cs
index 68fe980d4c0..f7d9e0bcaa3 100644
--- a/Source/DafnyLanguageServer/Workspace/CompilationManager.cs
+++ b/Source/DafnyLanguageServer/Workspace/CompilationManager.cs
@@ -22,7 +22,7 @@ public delegate CompilationManager CreateCompilationManager(
   DafnyOptions options,
   ExecutionEngine boogieEngine,
   Compilation compilation,
-  IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees);
+  IReadOnlyDictionary<Uri, DocumentVerificationTree> 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 IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees;
+  private readonly IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees;
 
   private TaskCompletionSource started = new();
   private readonly IScheduler verificationUpdateScheduler = new EventLoopScheduler();
@@ -66,7 +66,7 @@ public CompilationManager(
     DafnyOptions options,
     ExecutionEngine boogieEngine,
     Compilation compilation,
-    IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees
+    IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees
     ) {
     this.options = options;
     startingCompilation = compilation;
@@ -93,14 +93,20 @@ public void Start() {
   private async Task<CompilationAfterParsing> ParseAsync() {
     try {
       await started.Task;
-      var parsedCompilation = await documentLoader.ParseAsync(options, startingCompilation, migratedVerificationTrees, cancellationSource.Token);
+      var parsedCompilation = await documentLoader.ParseAsync(options, startingCompilation, migratedVerificationTrees,
+        cancellationSource.Token);
+      verificationProgressReporter.RecomputeVerificationTrees(parsedCompilation);
       foreach (var root in parsedCompilation.RootUris) {
         verificationProgressReporter.ReportRealtimeDiagnostics(parsedCompilation, root, false);
       }
+
       compilationUpdates.OnNext(parsedCompilation);
-      logger.LogDebug($"Passed parsedCompilation to documentUpdates.OnNext, resolving ParsedCompilation task for version {parsedCompilation.Version}.");
+      logger.LogDebug(
+        $"Passed parsedCompilation to documentUpdates.OnNext, resolving ParsedCompilation task for version {parsedCompilation.Version}.");
       return parsedCompilation;
 
+    } catch (OperationCanceledException) {
+      throw;
     } catch (Exception e) {
       compilationUpdates.OnError(e);
       throw;
@@ -123,6 +129,8 @@ private async Task<CompilationAfterResolution> ResolveAsync() {
       logger.LogDebug($"Passed resolvedCompilation to documentUpdates.OnNext, resolving ResolvedCompilation task for version {resolvedCompilation.Version}.");
       return resolvedCompilation;
 
+    } catch (OperationCanceledException) {
+      throw;
     } catch (Exception e) {
       compilationUpdates.OnError(e);
       throw;
@@ -178,6 +186,9 @@ public async Task<bool> VerifySymbol(FilePosition verifiableLocation, bool actua
           g => g.Key,
           g => (IReadOnlyList<IImplementationTask>)g.ToList());
       });
+    } catch (OperationCanceledException) {
+      verificationCompleted.TrySetCanceled();
+      throw;
     } catch (Exception e) {
       verificationCompleted.TrySetException(e);
       compilationUpdates.OnError(e);
diff --git a/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs b/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs
index 8ad86d8a4b4..00f68856315 100644
--- a/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs
+++ b/Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs
@@ -46,7 +46,7 @@ public IdeState InitialIdeState(Compilation initialCompilation, DafnyOptions opt
         SymbolTable.Empty(), LegacySignatureAndCompletionTable.Empty(options, initialCompilation.Project), new(),
         Array.Empty<Counterexample>(),
         ImmutableDictionary<Uri, IReadOnlyList<Range>>.Empty,
-        initialCompilation.RootUris.ToDictionary(uri => uri, uri => (VerificationTree)new DocumentVerificationTree(program, uri))
+        initialCompilation.RootUris.ToDictionary(uri => uri, uri => new DocumentVerificationTree(program, uri))
       ));
     }
 
diff --git a/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterParsing.cs b/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterParsing.cs
index 8ddddbcb47f..4758b5294b5 100644
--- a/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterParsing.cs
+++ b/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterParsing.cs
@@ -11,12 +11,12 @@ namespace Microsoft.Dafny.LanguageServer.Workspace;
 
 public class CompilationAfterParsing : Compilation {
   public IReadOnlyDictionary<Uri, List<DafnyDiagnostic>> ResolutionDiagnostics { get; set; }
-  public Dictionary<Uri, VerificationTree> VerificationTrees { get; }
+  public Dictionary<Uri, DocumentVerificationTree> VerificationTrees { get; }
 
   public CompilationAfterParsing(Compilation compilation,
     Program program,
     IReadOnlyDictionary<Uri, List<DafnyDiagnostic>> diagnostics,
-    Dictionary<Uri, VerificationTree> verificationTrees)
+    Dictionary<Uri, DocumentVerificationTree> verificationTrees)
     : base(compilation.Version, compilation.Project, compilation.RootUris) {
     ResolutionDiagnostics = diagnostics;
     VerificationTrees = verificationTrees;
diff --git a/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterResolution.cs b/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterResolution.cs
index 34f6b3fec61..f6b8df0c6d4 100644
--- a/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterResolution.cs
+++ b/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterResolution.cs
@@ -7,6 +7,8 @@
 using Microsoft.Boogie;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
+using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
+using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
@@ -72,7 +74,6 @@ IdeVerificationResult MergeResults(IEnumerable<IdeVerificationResult> results) {
   }
 
   public override IdeState ToIdeState(IdeState previousState) {
-
     IdeVerificationResult MergeVerifiable(ICanVerify canVerify) {
       var range = canVerify.NameToken.GetLspRange();
       var previousForCanVerify = previousState.GetVerificationResults(canVerify.NameToken.Uri).GetValueOrDefault(range) ??
@@ -108,7 +109,7 @@ IdeVerificationResult MergeVerifiable(ICanVerify canVerify) {
       SignatureAndCompletionTable = SignatureAndCompletionTable.Resolved ? SignatureAndCompletionTable : previousState.SignatureAndCompletionTable,
       GhostRanges = GhostDiagnostics,
       Counterexamples = new List<Counterexample>(Counterexamples),
-      VerificationTrees = VerificationTrees.ToDictionary(kv => kv.Key, kv => kv.Value.GetCopyForNotification()),
+      VerificationTrees = VerificationTrees.ToDictionary(kv => kv.Key, kv => (DocumentVerificationTree)kv.Value.GetCopyForNotification()),
       VerificationResults = Verifiables.GroupBy(l => l.NameToken.Uri).ToDictionary(k => k.Key,
         k => k.GroupBy(l => l.NameToken.GetLspRange()).ToDictionary(
           l => l.Key,
diff --git a/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs
index efa5c29dd79..734dfce71fc 100644
--- a/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs
+++ b/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs
@@ -22,10 +22,10 @@ public interface ITextDocumentLoader {
     IdeState CreateUnloaded(Compilation compilation);
 
     Task<CompilationAfterParsing> ParseAsync(DafnyOptions options, Compilation compilation,
-      IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees, CancellationToken cancellationToken);
+      IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees, CancellationToken cancellationToken);
 
     Task<CompilationAfterResolution> ResolveAsync(DafnyOptions options, CompilationAfterParsing compilation,
-      IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees,
+      IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees,
       CancellationToken cancellationToken);
   }
 }
diff --git a/Source/DafnyLanguageServer/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs
index 7b6bfffe19d..ed44d59fca0 100644
--- a/Source/DafnyLanguageServer/Workspace/IdeState.cs
+++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs
@@ -5,6 +5,7 @@
 using Microsoft.Boogie;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
+using Microsoft.Dafny.LanguageServer.Workspace.ChangeProcessors;
 using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
 using OmniSharp.Extensions.LanguageServer.Protocol;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
@@ -32,9 +33,48 @@ public record IdeState(
   Dictionary<Uri, Dictionary<Range, IdeVerificationResult>> VerificationResults,
   IReadOnlyList<Counterexample> Counterexamples,
   IReadOnlyDictionary<Uri, IReadOnlyList<Range>> GhostRanges,
-  IReadOnlyDictionary<Uri, VerificationTree> VerificationTrees
+  IReadOnlyDictionary<Uri, DocumentVerificationTree> VerificationTrees
 ) {
 
+  public IdeState Migrate(Migrator migrator, int version) {
+    var migratedVerificationTrees = VerificationTrees.ToDictionary(
+      kv => kv.Key, kv =>
+        (DocumentVerificationTree)migrator.RelocateVerificationTree(kv.Value));
+    return this with {
+      Version = version,
+      VerificationResults = MigrateImplementationViews(migrator, VerificationResults),
+      SignatureAndCompletionTable = migrator.MigrateSymbolTable(SignatureAndCompletionTable),
+      VerificationTrees = migratedVerificationTrees
+    };
+  }
+
+  private Dictionary<Uri, Dictionary<Range, IdeVerificationResult>> MigrateImplementationViews(Migrator migrator,
+    Dictionary<Uri, Dictionary<Range, IdeVerificationResult>> oldVerificationDiagnostics) {
+    return oldVerificationDiagnostics.ToDictionary(kv => kv.Key, kv => {
+      var result = new Dictionary<Range, IdeVerificationResult>();
+      foreach (var entry in kv.Value) {
+        var newOuterRange = migrator.MigrateRange(entry.Key);
+        if (newOuterRange == null) {
+          continue;
+        }
+
+        var newValue = new Dictionary<string, IdeImplementationView>();
+        foreach (var innerEntry in entry.Value.Implementations) {
+          var newInnerRange = migrator.MigrateRange(innerEntry.Value.Range);
+          if (newInnerRange != null) {
+            newValue.Add(innerEntry.Key, innerEntry.Value with {
+              Range = newInnerRange,
+              Diagnostics = migrator.MigrateDiagnostics(innerEntry.Value.Diagnostics)
+            });
+          }
+        }
+
+        result.Add(newOuterRange, entry.Value with { Implementations = newValue });
+      }
+
+      return result;
+    });
+  }
 
   public IReadOnlyDictionary<Range, IdeVerificationResult> GetVerificationResults(Uri uri) {
     return VerificationResults.GetValueOrDefault(uri) ??
diff --git a/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs b/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs
index 2fd77fb5817..3edbbe09dd6 100644
--- a/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs
+++ b/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs
@@ -2,9 +2,7 @@
 using System;
 using System.Collections.Generic;
 using System.Collections.Immutable;
-using System.Linq;
-using System.Threading;
-using Microsoft.Boogie;
+using System.Reactive;
 using Microsoft.Dafny.LanguageServer.Workspace.ChangeProcessors;
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
@@ -12,35 +10,33 @@
 
 namespace Microsoft.Dafny.LanguageServer.Workspace;
 
-public delegate IdeStateObserver CreateIdeStateObserver(Compilation compilation);
+public delegate IdeStateObserver CreateIdeStateObserver(IdeState initialState);
 
-public class IdeStateObserver : IObserver<IdeState> {
+public class IdeStateObserver : IObserver<IdeState> { // Inheriting from ObserverBase prevents this observer from recovering after a problem
   private readonly ILogger logger;
   private readonly ITelemetryPublisher telemetryPublisher;
   private readonly INotificationPublisher notificationPublisher;
-  private readonly ITextDocumentLoader loader;
-  private readonly Compilation compilation;
 
   private readonly object lastPublishedStateLock = new();
+  private readonly IdeState initialState;
 
   public IdeState LastPublishedState { get; private set; }
 
   public IdeStateObserver(ILogger logger,
     ITelemetryPublisher telemetryPublisher,
     INotificationPublisher notificationPublisher,
-    ITextDocumentLoader loader,
-    Compilation compilation) {
-    LastPublishedState = loader.CreateUnloaded(compilation);
+    IdeState initialState) {
+    this.initialState = initialState;
+    LastPublishedState = initialState;
     this.logger = logger;
     this.telemetryPublisher = telemetryPublisher;
     this.notificationPublisher = notificationPublisher;
-    this.loader = loader;
-    this.compilation = compilation;
   }
 
   public void OnCompleted() {
-    var initialCompilation = new Compilation(LastPublishedState.Version + 1, LastPublishedState.Compilation.Project, compilation.RootUris);
-    var ideState = loader.CreateUnloaded(initialCompilation);
+    var ideState = initialState with {
+      Version = LastPublishedState.Version + 1
+    };
 #pragma warning disable VSTHRD002
     notificationPublisher.PublishNotifications(LastPublishedState, ideState).Wait();
 #pragma warning restore VSTHRD002
@@ -48,11 +44,6 @@ public void OnCompleted() {
   }
 
   public void OnError(Exception exception) {
-    if (exception is OperationCanceledException) {
-      logger.LogDebug("document processing cancelled.");
-      return;
-    }
-
     var internalErrorDiagnostic = new Diagnostic {
       Message =
         "Dafny encountered an internal error. Please report it at <https://github.com/dafny-lang/dafny/issues>.\n" +
@@ -61,7 +52,7 @@ public void OnError(Exception exception) {
       Range = new Range(0, 0, 0, 1)
     };
     var documentToPublish = LastPublishedState with {
-      ResolutionDiagnostics = ImmutableDictionary<Uri, IReadOnlyList<Diagnostic>>.Empty.Add(compilation.Project.Uri, new[] { internalErrorDiagnostic })
+      ResolutionDiagnostics = ImmutableDictionary<Uri, IReadOnlyList<Diagnostic>>.Empty.Add(initialState.Compilation.Uri.ToUri(), new[] { internalErrorDiagnostic })
     };
 
     OnNext(documentToPublish);
@@ -82,50 +73,14 @@ public void OnNext(IdeState snapshot) {
       notificationPublisher.PublishNotifications(LastPublishedState, snapshot).Wait();
 #pragma warning restore VSTHRD002
       LastPublishedState = snapshot;
-      logger.LogDebug($"Updated LastPublishedState to version {snapshot.Version}, uri {compilation.Uri}");
+      logger.LogDebug($"Updated LastPublishedState to version {snapshot.Version}, uri {initialState.Compilation.Uri.ToUri()}");
     }
   }
 
   public void Migrate(Migrator migrator, int version) {
     lock (lastPublishedStateLock) {
-      var migratedVerificationTrees = LastPublishedState.VerificationTrees.ToDictionary(
-        kv => kv.Key, kv =>
-          migrator.RelocateVerificationTree(kv.Value));
-      LastPublishedState = LastPublishedState with {
-        Version = version,
-        VerificationResults = MigrateImplementationViews(migrator, LastPublishedState.VerificationResults),
-        SignatureAndCompletionTable = migrator.MigrateSymbolTable(LastPublishedState.SignatureAndCompletionTable),
-        VerificationTrees = migratedVerificationTrees
-      };
-      logger.LogDebug($"Migrated LastPublishedState to version {version}, uri {compilation.Uri}");
+      LastPublishedState = LastPublishedState.Migrate(migrator, version);
+      logger.LogDebug($"Migrated LastPublishedState to version {version}, uri {initialState.Compilation.Uri.ToUri()}");
     }
   }
-
-  private Dictionary<Uri, Dictionary<Range, IdeVerificationResult>> MigrateImplementationViews(Migrator migrator,
-      Dictionary<Uri, Dictionary<Range, IdeVerificationResult>> oldVerificationDiagnostics) {
-    return oldVerificationDiagnostics.ToDictionary(kv => kv.Key, kv => {
-      var result = new Dictionary<Range, IdeVerificationResult>();
-      foreach (var entry in kv.Value) {
-        var newOuterRange = migrator.MigrateRange(entry.Key);
-        if (newOuterRange == null) {
-          continue;
-        }
-
-        var newValue = new Dictionary<string, IdeImplementationView>();
-        foreach (var innerEntry in entry.Value.Implementations) {
-          var newInnerRange = migrator.MigrateRange(innerEntry.Value.Range);
-          if (newInnerRange != null) {
-            newValue.Add(innerEntry.Key, innerEntry.Value with {
-              Range = newInnerRange,
-              Diagnostics = migrator.MigrateDiagnostics(innerEntry.Value.Diagnostics)
-            });
-          }
-        }
-
-        result.Add(newOuterRange, entry.Value with { Implementations = newValue });
-      }
-
-      return result;
-    });
-  }
 }
diff --git a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs
index 9f2e39308c7..aca88cf7681 100644
--- a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs
+++ b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs
@@ -4,6 +4,7 @@
 using System.IO;
 using System.Linq;
 using System.Numerics;
+using System.Reactive;
 using System.Reactive.Disposables;
 using System.Reactive.Linq;
 using System.Threading;
@@ -60,6 +61,7 @@ public class ProjectManager : IDisposable {
   private readonly CreateCompilationManager createCompilationManager;
   private readonly ExecutionEngine boogieEngine;
   private readonly IFileSystem fileSystem;
+  private Lazy<IdeState> latestIdeState;
 
   public ProjectManager(
     DafnyOptions serverOptions,
@@ -84,11 +86,13 @@ public ProjectManager(
 
     options = DetermineProjectOptions(project, serverOptions);
     options.Printer = new OutputLogger(logger);
-
     var initialCompilation = CreateInitialCompilation();
-    observer = createIdeStateObserver(initialCompilation);
+    var initialIdeState = initialCompilation.InitialIdeState(initialCompilation, options);
+    latestIdeState = new Lazy<IdeState>(initialIdeState);
+
+    observer = createIdeStateObserver(initialIdeState);
     CompilationManager = createCompilationManager(
-        options, boogieEngine, initialCompilation, ImmutableDictionary<Uri, VerificationTree>.Empty
+        options, boogieEngine, initialCompilation, ImmutableDictionary<Uri, DocumentVerificationTree>.Empty
     );
 
     observerSubscription = Disposable.Empty;
@@ -103,10 +107,14 @@ private Compilation CreateInitialCompilation() {
   private const int MaxRememberedChangedVerifiables = 5;
 
   public void UpdateDocument(DidChangeTextDocumentParams documentChange) {
-    var changeProcessor = createMigrator(documentChange, CancellationToken.None);
-    observer.Migrate(changeProcessor, version + 1);
-    var lastPublishedState = observer.LastPublishedState;
-    var migratedVerificationTrees = lastPublishedState.VerificationTrees;
+    var migrator = createMigrator(documentChange, CancellationToken.None);
+    Lazy<IdeState> lazyPreviousCompilationLastIdeState = latestIdeState;
+    latestIdeState = new Lazy<IdeState>(() => {
+      // If we migrate the observer before accessing latestIdeState, we can be sure it's migrated before it receives new events.
+      observer.Migrate(migrator, version + 1);
+      return lazyPreviousCompilationLastIdeState.Value.Migrate(migrator, version + 1);
+    });
+    StartNewCompilation();
 
     lock (RecentChanges) {
       var newChanges = documentChange.ContentChanges.Where(c => c.Range != null).
@@ -115,7 +123,7 @@ public void UpdateDocument(DidChangeTextDocumentParams documentChange) {
           Uri = documentChange.TextDocument.Uri
         });
       var migratedChanges = RecentChanges.Select(location => {
-        var newRange = changeProcessor.MigrateRange(location.Range);
+        var newRange = migrator.MigrateRange(location.Range);
         if (newRange == null) {
           return null;
         }
@@ -126,32 +134,34 @@ public void UpdateDocument(DidChangeTextDocumentParams documentChange) {
       }).Where(r => r != null);
       RecentChanges = newChanges.Concat(migratedChanges).Take(MaxRememberedChanges).ToList()!;
     }
-
-    StartNewCompilation(migratedVerificationTrees, lastPublishedState);
     TriggerVerificationForFile(documentChange.TextDocument.Uri.ToUri());
   }
 
-  private void StartNewCompilation(IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees,
-    IdeState lastPublishedState) {
+  private void StartNewCompilation() {
     version++;
     logger.LogDebug("Clearing result for workCompletedForCurrentVersion");
 
+    Lazy<IdeState> migratedLazyPreviousCompilationLastIdeState = latestIdeState;
+    observerSubscription.Dispose();
+
     CompilationManager.CancelPendingUpdates();
     CompilationManager = createCompilationManager(
       options,
       boogieEngine,
       CreateInitialCompilation(),
-      migratedVerificationTrees);
+      latestIdeState.Value.VerificationTrees);
 
-    observerSubscription.Dispose();
     var migratedUpdates = CompilationManager.CompilationUpdates.Select(document =>
-      document.ToIdeState(lastPublishedState));
-    observerSubscription = migratedUpdates.Subscribe(observer);
+      latestIdeState = new Lazy<IdeState>(() => document.ToIdeState(migratedLazyPreviousCompilationLastIdeState.Value)));
+    var throttleTime = options.Get(ServerCommand.UpdateThrottling);
+    var throttledUpdates = throttleTime == 0 ? migratedUpdates : migratedUpdates.Sample(TimeSpan.FromMilliseconds(throttleTime));
+    observerSubscription = throttledUpdates.
+      Select(x => x.Value).Subscribe(observer);
 
     CompilationManager.Start();
   }
 
-  public void TriggerVerificationForFile(Uri triggeringFile) {
+  private void TriggerVerificationForFile(Uri triggeringFile) {
     if (AutomaticVerificationMode is VerifyOnMode.Change or VerifyOnMode.ChangeProject) {
       var _ = VerifyEverythingAsync(AutomaticVerificationMode == VerifyOnMode.Change ? triggeringFile : null);
     } else {
@@ -216,8 +226,8 @@ public async Task<IdeState> GetSnapshotAfterParsingAsync() {
       logger.LogDebug($"GetSnapshotAfterResolutionAsync caught OperationCanceledException for parsed compilation {Project.Uri}");
     }
 
-    logger.LogDebug($"GetSnapshotAfterParsingAsync returns state version {observer.LastPublishedState.Version}");
-    return observer.LastPublishedState;
+    logger.LogDebug($"GetSnapshotAfterParsingAsync returns state version {latestIdeState.Value.Version}");
+    return latestIdeState.Value;
   }
 
   public async Task<IdeState> GetStateAfterResolutionAsync() {
@@ -229,8 +239,8 @@ public async Task<IdeState> GetStateAfterResolutionAsync() {
       return await GetSnapshotAfterParsingAsync();
     }
 
-    logger.LogDebug($"GetStateAfterResolutionAsync returns state version {observer.LastPublishedState.Version}");
-    return observer.LastPublishedState;
+    logger.LogDebug($"GetStateAfterResolutionAsync returns state version {latestIdeState.Value.Version}");
+    return latestIdeState.Value;
   }
 
   public async Task<IdeState> GetIdeStateAfterVerificationAsync() {
@@ -239,7 +249,7 @@ public async Task<IdeState> GetIdeStateAfterVerificationAsync() {
     } catch (OperationCanceledException) {
     }
 
-    return observer.LastPublishedState;
+    return latestIdeState.Value;
   }
 
 
@@ -328,11 +338,9 @@ IntervalTree<Position, Position> GetTree(Uri uri) {
 
   public void OpenDocument(Uri uri, bool triggerCompilation) {
     Interlocked.Increment(ref openFileCount);
-    var lastPublishedState = observer.LastPublishedState;
-    var migratedVerificationTrees = lastPublishedState.VerificationTrees;
 
     if (triggerCompilation) {
-      StartNewCompilation(migratedVerificationTrees, lastPublishedState);
+      StartNewCompilation();
       TriggerVerificationForFile(uri);
     }
   }
diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
index f5695afd73a..450dca15f5b 100644
--- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
+++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
@@ -56,7 +56,7 @@ public IdeState CreateUnloaded(Compilation compilation) {
     }
 
     public async Task<CompilationAfterParsing> ParseAsync(DafnyOptions options, Compilation compilation,
-      IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees, CancellationToken cancellationToken) {
+      IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees, CancellationToken cancellationToken) {
 #pragma warning disable CS1998
       return await await DafnyMain.LargeStackFactory.StartNew(
         async () => ParseInternal(options, compilation, migratedVerificationTrees, cancellationToken), cancellationToken
@@ -65,7 +65,7 @@ public async Task<CompilationAfterParsing> ParseAsync(DafnyOptions options, Comp
     }
 
     private CompilationAfterParsing ParseInternal(DafnyOptions options, Compilation compilation,
-      IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees,
+      IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees,
       CancellationToken cancellationToken) {
       var project = compilation.Project;
       var errorReporter = new DiagnosticErrorReporter(options, project.Uri);
@@ -79,17 +79,16 @@ private CompilationAfterParsing ParseInternal(DafnyOptions options, Compilation
 
     public async Task<CompilationAfterResolution> ResolveAsync(DafnyOptions options,
       CompilationAfterParsing compilation,
-      IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees,
+      IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees,
       CancellationToken cancellationToken) {
 #pragma warning disable CS1998
       return await await DafnyMain.LargeStackFactory.StartNew(
-        async () => ResolveInternal(compilation, migratedVerificationTrees, cancellationToken), cancellationToken
+        async () => ResolveInternal(compilation, migratedVerificationTrees, cancellationToken), cancellationToken);
 #pragma warning restore CS1998
-        );
     }
 
     private CompilationAfterResolution ResolveInternal(CompilationAfterParsing compilation,
-      IReadOnlyDictionary<Uri, VerificationTree> migratedVerificationTrees, CancellationToken cancellationToken) {
+      IReadOnlyDictionary<Uri, DocumentVerificationTree> migratedVerificationTrees, CancellationToken cancellationToken) {
 
       var program = compilation.Program;
       var errorReporter = (DiagnosticErrorReporter)program.Reporter;
@@ -144,7 +143,7 @@ private IdeState CreateDocumentWithEmptySymbolTable(Compilation compilation,
         new(),
         Array.Empty<Counterexample>(),
         ImmutableDictionary<Uri, IReadOnlyList<Range>>.Empty,
-      ImmutableDictionary<Uri, VerificationTree>.Empty
+      ImmutableDictionary<Uri, DocumentVerificationTree>.Empty
       );
     }
   }
diff --git a/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs b/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs
index c9d0968d440..51da0d929e4 100644
--- a/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs
+++ b/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs
@@ -28,15 +28,21 @@ public VerificationProgressReporter(ILogger<VerificationProgressReporter> logger
   /// Fills up the document with empty verification diagnostics, one for each top-level declarations
   /// Possibly migrates previous diagnostics
   /// </summary>
-  public void RecomputeVerificationTrees(CompilationAfterResolution compilation) {
-    foreach (var tree in compilation.VerificationTrees.Values) {
-      UpdateTree(options, compilation, tree);
+  public void RecomputeVerificationTrees(CompilationAfterParsing compilation) {
+    foreach (var uri in compilation.VerificationTrees.Keys) {
+      compilation.VerificationTrees[uri] = UpdateTree(options, compilation, compilation.VerificationTrees[uri]);
     }
   }
 
-  public static void UpdateTree(DafnyOptions options, CompilationAfterParsing parsedCompilation, VerificationTree rootVerificationTree) {
+  private static DocumentVerificationTree UpdateTree(DafnyOptions options, CompilationAfterParsing parsedCompilation, DocumentVerificationTree rootVerificationTree) {
     var previousTrees = rootVerificationTree.Children;
 
+    if (parsedCompilation is not CompilationAfterResolution) {
+      return new DocumentVerificationTree(parsedCompilation.Program, rootVerificationTree.Uri) {
+        Children = rootVerificationTree.Children
+      };
+    }
+
     List<VerificationTree> result = new List<VerificationTree>();
 
     HashSet<Position> recordedPositions = new HashSet<Position>();
@@ -151,7 +157,9 @@ void AddAndPossiblyMigrateVerificationTree(VerificationTree verificationTree) {
       }
     }
 
-    rootVerificationTree.Children = result;
+    return new DocumentVerificationTree(parsedCompilation.Program, rootVerificationTree.Uri) {
+      Children = result
+    };
   }
 
   /// <summary>
diff --git a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj
index 7d2c524f988..d22194db572 100644
--- a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj
+++ b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj
@@ -13,7 +13,7 @@
 
   <ItemGroup>
     <PackageReference Include="DiffPlex" Version="1.7.0" />
-    <PackageReference Include="Microsoft.NET.Test.Sdk" Version="16.11.0" />
+    <PackageReference Include="Microsoft.NET.Test.Sdk" Version="17.1.0" />
     <PackageReference Include="xunit" Version="2.4.2" />
     <PackageReference Include="xunit.runner.visualstudio" Version="2.4.3">
       <IncludeAssets>runtime; build; native; contentfiles; analyzers; buildtransitive</IncludeAssets>
@@ -26,6 +26,7 @@
   </ItemGroup>
 
   <ItemGroup>
+    <ProjectReference Include="..\DafnyCore.Test\DafnyCore.Test.csproj" />
     <ProjectReference Include="..\DafnyDriver\DafnyDriver.csproj" />
   </ItemGroup>
 
diff --git a/Source/DafnyPipeline.Test/DocstringTest.cs b/Source/DafnyPipeline.Test/DocstringTest.cs
index 6067370e304..50e07bf3e60 100644
--- a/Source/DafnyPipeline.Test/DocstringTest.cs
+++ b/Source/DafnyPipeline.Test/DocstringTest.cs
@@ -1,8 +1,10 @@
 #nullable enable
 using System;
 using System.Collections.Generic;
+using System.IO;
 using System.Linq;
 using System.Text.RegularExpressions;
+using DafnyCore.Test;
 using DafnyTestGeneration;
 using Bpl = Microsoft.Boogie;
 using BplParser = Microsoft.Boogie.Parser;
@@ -426,7 +428,7 @@ protected void DocstringWorksFor(string source, string nodeTokenValue, string? e
     }
 
     protected void DocstringWorksFor(string source, List<(string nodeTokenValue, string? expectedDocstring)> tests) {
-      var options = DafnyOptions.Create(new WriterFromOutputHelper(output));
+      var options = DafnyOptions.Create((TextWriter)new WriterFromOutputHelper(output));
       var newlineTypes = Enum.GetValues(typeof(Newlines));
       foreach (Newlines newLinesType in newlineTypes) {
         currentNewlines = newLinesType;
diff --git a/Source/DafnyPipeline.Test/FormatterBaseTest.cs b/Source/DafnyPipeline.Test/FormatterBaseTest.cs
index f8bb5395f57..14718152321 100644
--- a/Source/DafnyPipeline.Test/FormatterBaseTest.cs
+++ b/Source/DafnyPipeline.Test/FormatterBaseTest.cs
@@ -4,6 +4,7 @@
 using System.Collections.Immutable;
 using System.IO;
 using System.Text.RegularExpressions;
+using DafnyCore.Test;
 using DafnyTestGeneration;
 using Bpl = Microsoft.Boogie;
 using BplParser = Microsoft.Boogie.Parser;
diff --git a/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs b/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs
index 3d5fd272f72..bd577a9b6ac 100644
--- a/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs
+++ b/Source/DafnyPipeline.Test/IntraMethodVerificationStability.cs
@@ -2,6 +2,7 @@
 using System.IO;
 using System.Linq;
 using System.Threading.Tasks;
+using DafnyCore.Test;
 using DafnyTestGeneration;
 using Microsoft.Boogie;
 using Microsoft.Dafny;
@@ -148,7 +149,7 @@ public IntraMethodVerificationStability(ITestOutputHelper testOutputHelper) {
 
     [Fact]
     public void NoUniqueLinesWhenConcatenatingUnrelatedPrograms() {
-      var options = DafnyOptions.Create(new WriterFromOutputHelper(testOutputHelper));
+      var options = DafnyOptions.Create((TextWriter)new WriterFromOutputHelper(testOutputHelper));
 
       var regularBoogie = GetBoogie(options, originalProgram).ToList();
       var renamedBoogie = GetBoogie(options, renamedProgram).ToList();
@@ -164,7 +165,7 @@ public void NoUniqueLinesWhenConcatenatingUnrelatedPrograms() {
 
     [Fact]
     public async Task EqualProverLogWhenReorderingProgram() {
-      var options = DafnyOptions.Create(new WriterFromOutputHelper(testOutputHelper));
+      var options = DafnyOptions.Create((TextWriter)new WriterFromOutputHelper(testOutputHelper));
       options.ProcsToCheck.Add("SomeMethod*");
 
       var reorderedProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, reorderedProgram));
@@ -174,7 +175,7 @@ public async Task EqualProverLogWhenReorderingProgram() {
 
     [Fact]
     public async Task EqualProverLogWhenRenamingProgram() {
-      var options = DafnyOptions.Create(new WriterFromOutputHelper(testOutputHelper));
+      var options = DafnyOptions.Create((TextWriter)new WriterFromOutputHelper(testOutputHelper));
       options.ProcsToCheck.Add("*SomeMethod*");
 
       var renamedProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, renamedProgram));
@@ -185,7 +186,7 @@ public async Task EqualProverLogWhenRenamingProgram() {
     [Fact]
     public async Task EqualProverLogWhenAddingUnrelatedProgram() {
 
-      var options = DafnyOptions.Create(new WriterFromOutputHelper(testOutputHelper));
+      var options = DafnyOptions.Create((TextWriter)new WriterFromOutputHelper(testOutputHelper));
       options.ProcsToCheck.Add("*SomeMethod *");
 
       var renamedProverLog = await GetProverLogForProgramAsync(options, GetBoogie(options, renamedProgram + originalProgram));
diff --git a/Source/DafnyPipeline.Test/Issue1355.cs b/Source/DafnyPipeline.Test/Issue1355.cs
index 8ac93cd5c8e..d4f260f09f3 100644
--- a/Source/DafnyPipeline.Test/Issue1355.cs
+++ b/Source/DafnyPipeline.Test/Issue1355.cs
@@ -1,4 +1,5 @@
 using System.IO;
+using DafnyCore.Test;
 using DafnyTestGeneration;
 using Bpl = Microsoft.Boogie;
 using BplParser = Microsoft.Boogie.Parser;
diff --git a/Source/DafnyPipeline.Test/PluginsTest.cs b/Source/DafnyPipeline.Test/PluginsTest.cs
index 7cfa42bbe93..f9a4fe97b0a 100644
--- a/Source/DafnyPipeline.Test/PluginsTest.cs
+++ b/Source/DafnyPipeline.Test/PluginsTest.cs
@@ -2,6 +2,7 @@
 using System.IO;
 using System.Linq;
 using System.Reflection;
+using DafnyCore.Test;
 using DafnyTestGeneration;
 using Microsoft.CodeAnalysis;
 using Microsoft.CodeAnalysis.CSharp;
diff --git a/Source/DafnyPipeline.Test/RelativePaths.cs b/Source/DafnyPipeline.Test/RelativePaths.cs
index 4d71cc07d1d..03ba9e4b93e 100644
--- a/Source/DafnyPipeline.Test/RelativePaths.cs
+++ b/Source/DafnyPipeline.Test/RelativePaths.cs
@@ -1,4 +1,5 @@
 using System.IO;
+using DafnyCore.Test;
 using Microsoft.Dafny;
 using Xunit;
 using Xunit.Abstractions;
diff --git a/Source/DafnyPipeline.Test/Trivia.cs b/Source/DafnyPipeline.Test/Trivia.cs
index be312c3e598..bd812e8b106 100644
--- a/Source/DafnyPipeline.Test/Trivia.cs
+++ b/Source/DafnyPipeline.Test/Trivia.cs
@@ -3,6 +3,7 @@
 using System.IO;
 using System.Linq;
 using System.Text.RegularExpressions;
+using DafnyCore.Test;
 using DafnyTestGeneration;
 using Bpl = Microsoft.Boogie;
 using BplParser = Microsoft.Boogie.Parser;
diff --git a/Source/DafnyPipeline.Test/WriterFromOutputHelper.cs b/Source/DafnyPipeline.Test/WriterFromOutputHelper.cs
deleted file mode 100644
index c8159df29ef..00000000000
--- a/Source/DafnyPipeline.Test/WriterFromOutputHelper.cs
+++ /dev/null
@@ -1,30 +0,0 @@
-#nullable enable
-using System.IO;
-using System.Text;
-using Xunit.Abstractions;
-
-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);
-  }
-}
\ No newline at end of file
diff --git a/Source/DafnyTestGeneration.Test/BasicTypes.cs b/Source/DafnyTestGeneration.Test/BasicTypes.cs
index a5358746ae0..2952b80bc95 100644
--- a/Source/DafnyTestGeneration.Test/BasicTypes.cs
+++ b/Source/DafnyTestGeneration.Test/BasicTypes.cs
@@ -8,6 +8,7 @@
 using System.Linq;
 using System.Text.RegularExpressions;
 using System.Threading.Tasks;
+using DafnyCore.Test;
 using Microsoft.Dafny;
 using Xunit;
 using Xunit.Abstractions;
diff --git a/Source/DafnyTestGeneration.Test/Collections.cs b/Source/DafnyTestGeneration.Test/Collections.cs
index 2a02446149e..5e3f85918fc 100644
--- a/Source/DafnyTestGeneration.Test/Collections.cs
+++ b/Source/DafnyTestGeneration.Test/Collections.cs
@@ -8,6 +8,7 @@
 using System.Linq;
 using System.Text.RegularExpressions;
 using System.Threading.Tasks;
+using DafnyCore.Test;
 using Microsoft.Dafny;
 using Xunit;
 using Xunit.Abstractions;
diff --git a/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj b/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj
index bf8594de184..b4920e58810 100644
--- a/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj
+++ b/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj
@@ -7,7 +7,7 @@
     </PropertyGroup>
 
     <ItemGroup>
-        <PackageReference Include="Microsoft.NET.Test.Sdk" Version="16.11.0" />
+        <PackageReference Include="Microsoft.NET.Test.Sdk" Version="17.1.0" />
         <PackageReference Include="xunit" Version="2.4.2" />
         <PackageReference Include="xunit.extensibility.core" Version="2.4.2" />
         <PackageReference Include="xunit.runner.visualstudio" Version="2.4.3">
@@ -18,6 +18,7 @@
     </ItemGroup>
 
     <ItemGroup>
+        <ProjectReference Include="..\DafnyCore.Test\DafnyCore.Test.csproj" />
         <ProjectReference Include="..\DafnyRuntime\DafnyRuntime.csproj" />
         <ProjectReference Include="..\DafnyTestGeneration\DafnyTestGeneration.csproj" />
     </ItemGroup>
diff --git a/Source/DafnyTestGeneration.Test/ShortCircuitRemoval.cs b/Source/DafnyTestGeneration.Test/ShortCircuitRemoval.cs
index 3d90ded7477..664b49d5e83 100644
--- a/Source/DafnyTestGeneration.Test/ShortCircuitRemoval.cs
+++ b/Source/DafnyTestGeneration.Test/ShortCircuitRemoval.cs
@@ -7,6 +7,7 @@
 using System.IO;
 using System.Linq;
 using System.Text.RegularExpressions;
+using DafnyCore.Test;
 using DafnyTestGeneration.Inlining;
 using Microsoft.Dafny;
 using Xunit;
diff --git a/Source/DafnyTestGeneration.Test/Various.cs b/Source/DafnyTestGeneration.Test/Various.cs
index 8d6237b43f9..2292fe2dd73 100644
--- a/Source/DafnyTestGeneration.Test/Various.cs
+++ b/Source/DafnyTestGeneration.Test/Various.cs
@@ -8,6 +8,7 @@
 using System.Linq;
 using System.Text.RegularExpressions;
 using System.Threading.Tasks;
+using DafnyCore.Test;
 using Microsoft.Dafny;
 using Xunit;
 using Xunit.Abstractions;