Stop reusing solvers with the IDE by default (#5325)

### Description
- By default, do not let the IDE reuse solvers between compilations.
This makes the IDE verification behavior more like that of the CLI

### How has this been tested?
Manually tested that latency of verification after a change still feels
snappy

<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/DafnyDriver/Commands/ServerCommand.cs

@@ -23,6 +23,7 @@ public class ServerCommand {
  LanguageServer.VerifySnapshots,
  DafnyLangSymbolResolver.UseCaching,
  ProjectManager.UpdateThrottling,
+ ProjectManager.ReuseSolvers,
  LegacySignatureAndCompletionTable.MigrateSignatureAndCompletionTable
  );
  }

Source/DafnyLanguageServer/Workspace/ProjectManager.cs

@@ -46,6 +46,11 @@ public class ProjectManager : IDisposable {
  ArgumentHelpName = "event"
  };
 
+ public static readonly Option<bool> ReuseSolvers = new("--reuse-solvers",
+ @"(experimental) Reuse solver for different verification of different document versions. Reduces verification latency but may reduce reliability of verification.".TrimStart()) {
+ ArgumentHelpName = "event"
+ };
+
  private readonly CreateMigrator createMigrator;
  public DafnyProject Project { get; }
 
@@ -55,6 +60,9 @@ public class ProjectManager : IDisposable {
  private readonly EventLoopScheduler ideStateUpdateScheduler = new();
  private readonly ILogger<ProjectManager> logger;
 
+ private readonly VerificationResultCache cache;
+ private readonly CustomStackSizePoolTaskScheduler scheduler;
+
  /// <summary>
  /// The version of this project.
  /// Is incremented when any file in the project is updated.
@@ -73,7 +81,7 @@ public class ProjectManager : IDisposable {
  private readonly DafnyOptions options;
  private readonly DafnyOptions serverOptions;
  private readonly CreateCompilation createCompilation;
- private readonly ExecutionEngine boogieEngine;
+ private ExecutionEngine? boogieEngine;
  private readonly IFileSystem fileSystem;
  private readonly TelemetryPublisherBase telemetryPublisher;
  private readonly IProjectDatabase projectDatabase;
@@ -104,13 +112,14 @@ public class ProjectManager : IDisposable {
 
  options = DetermineProjectOptions(project, serverOptions);
  options.Printer = new OutputLogger(logger);
- boogieEngine = new ExecutionEngine(options, cache, scheduler);
+ this.cache = cache;
+ this.scheduler = scheduler;
  var compilationInput = new CompilationInput(options, version, Project);
  var initialIdeState = IdeState.InitialIdeState(compilationInput);
  latestIdeState = initialIdeState;
 
  observer = createIdeStateObserver(initialIdeState);
- Compilation = createCompilation(boogieEngine, compilationInput);
+ Compilation = this.createCompilation(GetBoogie(), compilationInput);
 
  observerSubscription = Disposable.Empty;
  }
@@ -135,7 +144,7 @@ public class ProjectManager : IDisposable {
 
  Compilation.Dispose();
  var input = new CompilationInput(options, version, Project);
- Compilation = createCompilation(boogieEngine, input);
+ Compilation = createCompilation(GetBoogie(), input);
  var migratedUpdates = GetStates(Compilation);
  states = new ReplaySubject<IdeState>(1);
  var statesSubscription = observerSubscription =
@@ -155,6 +164,16 @@ public class ProjectManager : IDisposable {
  TriggerVerificationForFile(triggeringFile);
  }
 
+ private ExecutionEngine GetBoogie() {
+ if (options.Get(ReuseSolvers)) {
+ boogieEngine ??= new ExecutionEngine(options, cache, scheduler);
+ } else {
+ boogieEngine?.Dispose();
+ boogieEngine = new ExecutionEngine(options, cache, scheduler);
+ }
+ return boogieEngine;
+ }
+
  private void UpdateRecentChanges(DidChangeTextDocumentParams changes, Migrator? migrator) {
  lock (RecentChanges) {
  var newChanges = changes.ContentChanges.Where(c => c.Range != null).
@@ -354,7 +373,7 @@ public class ProjectManager : IDisposable {
  }
 
  public void Dispose() {
- boogieEngine.Dispose();
+ boogieEngine?.Dispose();
  Compilation.Dispose();
  observerSubscription.Dispose();
  // Dispose the update scheduler after the observer subscription, to prevent accessing a disposed object.