Allow not migrating legacy symbols

Source/DafnyDriver/Commands/ServerCommand.cs

@@ -22,7 +22,8 @@ static ServerCommand() {
  GutterIconAndHoverVerificationDetailsManager.LineVerificationStatus,
  LanguageServer.VerifySnapshots,
  DafnyLangSymbolResolver.UseCaching,
- ProjectManager.UpdateThrottling
+ ProjectManager.UpdateThrottling,
+ LegacySignatureAndCompletionTable.MigrateSignatureAndCompletionTable
  );
  }
 

Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs

@@ -4,6 +4,7 @@
 using System.Threading.Tasks;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Microsoft.Dafny.LanguageServer.Language.Symbols;
 using Microsoft.Dafny.LanguageServer.Workspace;
 using Xunit;
 using Xunit.Abstractions;
@@ -18,6 +19,7 @@ protected override Task SetUp(Action<DafnyOptions> modifyOptions) {
  modifyOptions?.Invoke(options);
  // We're setting LineVerificationStatus to false already, with the expectation that this will become the default.
  options.Set(GutterIconAndHoverVerificationDetailsManager.LineVerificationStatus, false);
+ options.Set(LegacySignatureAndCompletionTable.MigrateSignatureAndCompletionTable, false);
  options.Set(ProjectManager.UpdateThrottling, ProjectManager.DefaultThrottleTime);
  });
  }

Source/DafnyLanguageServer.Test/Unit/CompilationManagerTest.cs

@@ -18,7 +18,7 @@ public async Task CancelUnstartedCompilationLeadsToCancelledTasks() {
  new Mock<IProgramVerifier>().Object,
  new Mock<IGutterIconAndHoverVerificationDetailsManager>().Object,
  dafnyOptions,
- null, new Compilation(0, new DafnyProject() { Uri = new Uri(Directory.GetCurrentDirectory()) }, new Uri[] { }), null);
+ null, new Compilation(dafnyOptions, 0, new DafnyProject() { Uri = new Uri(Directory.GetCurrentDirectory()) }, new Uri[] { }), null);
  compilationManager.CancelPendingUpdates();
  await Assert.ThrowsAsync<TaskCanceledException>(() => compilationManager.ParsedCompilation);
  }

Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs

@@ -81,7 +81,7 @@ public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() {
 
  private static Compilation GetCompilation() {
  var versionedTextDocumentIdentifier = CreateTestDocumentId();
- var compilation = new Compilation(0, ProjectManagerDatabase.ImplicitProject(versionedTextDocumentIdentifier.Uri.ToUri()), new[] { versionedTextDocumentIdentifier.Uri.ToUri() });
+ var compilation = new Compilation(DafnyOptions.Default, 0, ProjectManagerDatabase.ImplicitProject(versionedTextDocumentIdentifier.Uri.ToUri()), new[] { versionedTextDocumentIdentifier.Uri.ToUri() });
  return compilation;
  }
 

Source/DafnyLanguageServer/Language/Symbols/LegacySignatureAndCompletionTable.cs

@@ -3,8 +3,10 @@
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using System.Collections.Generic;
 using System.Collections.Immutable;
+using System.CommandLine;
 using System.Diagnostics.CodeAnalysis;
 using System.Linq;
+using System.Runtime.CompilerServices;
 using System.Threading;
 using Microsoft.Extensions.Logging;
 using Microsoft.Extensions.Logging.Abstractions;
@@ -16,6 +18,11 @@ namespace Microsoft.Dafny.LanguageServer.Language.Symbols {
  /// Represents the symbol table
  /// </summary>
  public class LegacySignatureAndCompletionTable {
+
+ public static readonly Option<bool> MigrateSignatureAndCompletionTable = new("--migrate-signature-and-completion-table", () => true) {
+ IsHidden = true
+ };
+
  private readonly ILogger<LegacySignatureAndCompletionTable> logger;
 
  // TODO Guard the properties from changes
@@ -54,16 +61,27 @@ public static LegacySignatureAndCompletionTable Empty(DafnyOptions options, Dafn
  symbolsResolved: false);
  }
 
+ private static readonly ConditionalWeakTable<DafnyOptions, SystemModuleManager> systemModuleManagers = new();
+
  public static Program GetEmptyProgram(DafnyOptions options, Uri uri) {
  var outerModule = new DefaultModuleDefinition(new List<Uri>() { uri });
  var errorReporter = new DiagnosticErrorReporter(options, uri);
  var compilation = new CompilationData(errorReporter, new List<Include>(), new List<Uri>(), Sets.Empty<Uri>(),
  Sets.Empty<Uri>());
+
+ SystemModuleManager manager;
+ lock (options) {
+ if (!systemModuleManagers.TryGetValue(options, out manager!)) {
+ manager = new SystemModuleManager(options);
+ systemModuleManagers.Add(options, manager);
+ }
+ }
+
  var emptyProgram = new Program(
  uri.ToString(),
  new LiteralModuleDecl(outerModule, null, Guid.NewGuid()),
  // BuiltIns cannot be initialized without Type.ResetScopes() before.
- new SystemModuleManager(options), // TODO creating a BuiltIns is a heavy operation
+ manager,
  errorReporter, compilation
  );
  return emptyProgram;

Source/DafnyLanguageServer/LanguageServer.cs

@@ -28,7 +28,8 @@ public class LanguageServer {
  ProjectManager.UpdateThrottling,
  DeveloperOptionBag.BoogiePrint,
  CommonOptionBag.EnforceDeterminism,
- CommonOptionBag.UseJavadocLikeDocstringRewriterOption
+ CommonOptionBag.UseJavadocLikeDocstringRewriterOption,
+ LegacySignatureAndCompletionTable.MigrateSignatureAndCompletionTable
  }.Concat(DafnyCommands.VerificationOptions).
  Concat(DafnyCommands.ResolverOptions);
 

Source/DafnyLanguageServer/Workspace/Documents/Compilation.cs

@@ -28,11 +28,13 @@ public class Compilation {
  /// </summary>
  public IReadOnlyList<Uri> RootUris { get; }
  public int Version { get; }
+ public DafnyOptions Options { get; }
  public DafnyProject Project { get; }
  public DocumentUri Uri => Project.Uri;
 
- public Compilation(int version, DafnyProject project, IReadOnlyList<Uri> rootUris) {
+ public Compilation(DafnyOptions options, int version, DafnyProject project, IReadOnlyList<Uri> rootUris) {
  this.RootUris = rootUris;
+ Options = options;
  Version = version;
  Project = project;
  }

Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterParsing.cs

@@ -17,7 +17,7 @@ public CompilationAfterParsing(Compilation compilation,
  Program program,
  IReadOnlyDictionary<Uri, List<DafnyDiagnostic>> diagnostics,
  Dictionary<Uri, DocumentVerificationTree> verificationTrees)
- : base(compilation.Version, compilation.Project, compilation.RootUris) {
+ : base(compilation.Options, compilation.Version, compilation.Project, compilation.RootUris) {
  ResolutionDiagnostics = diagnostics;
  VerificationTrees = verificationTrees;
  Program = program;

Source/DafnyLanguageServer/Workspace/IdeState.cs

@@ -44,7 +44,8 @@ public IdeState Migrate(Migrator migrator, int version) {
  return this with {
  Version = version,
  VerificationResults = MigrateImplementationViews(migrator, VerificationResults),
- SignatureAndCompletionTable = migrator.MigrateSymbolTable(SignatureAndCompletionTable),
+ SignatureAndCompletionTable = Compilation.Options.Get(LegacySignatureAndCompletionTable.MigrateSignatureAndCompletionTable)
+ ? migrator.MigrateSymbolTable(SignatureAndCompletionTable) : LegacySignatureAndCompletionTable.Empty(Compilation.Options, Compilation.Project),
  VerificationTrees = migratedVerificationTrees
  };
  }

Source/DafnyLanguageServer/Workspace/ProjectManager.cs

@@ -115,7 +115,7 @@ public ProjectManager(
 
  private Compilation CreateInitialCompilation() {
  var rootUris = Project.GetRootSourceUris(fileSystem).Concat(options.CliRootSourceUris).ToList();
- return new Compilation(version, Project, rootUris);
+ return new Compilation(options, version, Project, rootUris);
  }
 
  private const int MaxRememberedChanges = 100;