diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs index 0bbf1e16ed8..8e188130f53 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs +++ b/Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs @@ -25,7 +25,6 @@ protected override async Task SetUp(Action modifyOptions) { void ModifyOptions(DafnyOptions options) { options.Set(ServerCommand.LineVerificationStatus, true); - options.Set(ServerCommand.ProjectMode, true); modifyOptions?.Invoke(options); } await base.SetUp(ModifyOptions); diff --git a/Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs b/Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs index 2d82c173fe1..4fc172d35e3 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs @@ -13,7 +13,6 @@ public class GoToDefinitionTest : ClientBasedLanguageServerTest { [Fact] public async Task ExplicitProjectToGoDefinitionWorks() { - await SetUp(o => o.Set(ServerCommand.ProjectMode, true)); var sourceA = @" const a := 3; ".TrimStart(); diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs index f3f3914a007..d977e4ae0dc 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs @@ -17,7 +17,6 @@ public class HoverTest : ClientBasedLanguageServerTest { protected override async Task SetUp(Action modifyOptions = null) { void ModifyOptions(DafnyOptions options) { options.ProverOptions.Add("SOLVER=noop"); - options.Set(ServerCommand.ProjectMode, true); modifyOptions?.Invoke(options); } diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs index ed862d5ec81..36ab1f6d369 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs @@ -21,13 +21,6 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup { [Collection("Sequential Collection")] // Let slow tests run sequentially public class HoverVerificationTest : ClientBasedLanguageServerTest { - protected override Task SetUp(Action modifyOptions) { - return base.SetUp(o => { - o.Set(ServerCommand.ProjectMode, true); - modifyOptions?.Invoke(o); - }); - } - private const int MaxTestExecutionTimeMs = 30000; [Fact(Timeout = MaxTestExecutionTimeMs)] diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/CompetingProjectFilesTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/CompetingProjectFilesTest.cs index 2036af3fa26..233740089b8 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/CompetingProjectFilesTest.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/CompetingProjectFilesTest.cs @@ -12,13 +12,6 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.ProjectFiles; public class CompetingProjectFilesTest : ClientBasedLanguageServerTest { - protected override Task SetUp(Action modifyOptions) { - return base.SetUp(o => { - o.Set(ServerCommand.ProjectMode, true); - modifyOptions?.Invoke(o); - }); - } - /// /// A project should only publish diagnostics for uris which it owns, diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesProjectTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesProjectTest.cs index aa5afd0651c..7da97f1a69b 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesProjectTest.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesProjectTest.cs @@ -13,43 +13,6 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.ProjectFiles; public class MultipleFilesProjectTest : ClientBasedLanguageServerTest { - protected override Task SetUp(Action modifyOptions) { - return base.SetUp(o => { - o.Set(ServerCommand.ProjectMode, true); - modifyOptions?.Invoke(o); - }); - } - - [Fact] - public async Task NoProjectModeWithProjectFileAndMultipleFiles() { - await SetUp(o => { - o.Set(ServerCommand.ProjectMode, false); - }); - var producerSource = @" -method Foo(x: int) { - var y: char := 3.0; -} -".TrimStart(); - - var consumerSource = @" -include ""A.dfy"" -method Bar() { - Foo(true); -} -"; - - var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName()); - Directory.CreateDirectory(directory); - await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName), ""); - // The names A and B are important, because A must be alphabetically before B to trigger a particular cache without cloning bug - await File.WriteAllTextAsync(Path.Combine(directory, "A.dfy"), producerSource); - await CreateAndOpenTestDocument(consumerSource, Path.Combine(directory, "B.dfy")); - - var consumerDiagnostics = await diagnosticsReceiver.AwaitNextNotificationAsync(CancellationToken); - Assert.Equal(2, consumerDiagnostics.Diagnostics.Count()); - Assert.Contains(consumerDiagnostics.Diagnostics, diagnostic => diagnostic.Message.Contains("bool")); - await AssertNoDiagnosticsAreComing(CancellationToken); - } [Fact] public async Task OnDiskProducerResolutionErrors() { diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs index a87ed26915e..5a57a327cec 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs @@ -69,14 +69,32 @@ await SetUp(options => { options.Set(Function.FunctionSyntaxOption, "3"); options.Set(CommonOptionBag.WarnShadowing, true); }); - var filePath = Path.Combine(Directory.GetCurrentDirectory(), "ProjectFiles/TestFiles/noWarnShadowing.dfy"); - var source = await File.ReadAllTextAsync(filePath); - source += "\nghost function Bar(): int { 3 }"; + var source = @" +method Foo() { + var x := 3; + if (true) { + var x := 4; + } +} - var doc1 = await CreateAndOpenTestDocument(source, "orphaned"); - var diagnostics1 = await GetLastDiagnostics(doc1, CancellationToken); +ghost function Bar(): int { 3 }".TrimStart(); + + var projectFileSource = @" +includes = [""**/*.dfy""] + +[options] +warn-shadowing = false +function-syntax = 4"; + + var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName()); + Directory.CreateDirectory(directory); + + var noProjectFile = await CreateAndOpenTestDocument(source, "orphaned.dfy"); + var diagnostics1 = await GetLastDiagnostics(noProjectFile, CancellationToken); Assert.Single(diagnostics1); // Stops after parsing - await CreateAndOpenTestDocument(source, filePath); + + await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName), projectFileSource); + await CreateAndOpenTestDocument(source, Path.Combine(directory, "source.dfy")); await AssertNoDiagnosticsAreComing(CancellationToken); } diff --git a/Source/DafnyLanguageServer.Test/Refactoring/RenameTest.cs b/Source/DafnyLanguageServer.Test/Refactoring/RenameTest.cs index 2d6d978298c..5b8f58a1e5e 100644 --- a/Source/DafnyLanguageServer.Test/Refactoring/RenameTest.cs +++ b/Source/DafnyLanguageServer.Test/Refactoring/RenameTest.cs @@ -118,13 +118,6 @@ protected async Task SetUpProjectFile() { return tempDir; } - protected override Task SetUp(Action modifyOptions) { - return base.SetUp(o => { - o.Set(ServerCommand.ProjectMode, true); - modifyOptions?.Invoke(o); - }); - } - /// /// Assert that after requesting a rename to /// at the markup position in diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationOrderTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationOrderTest.cs index 64b257efccd..82e2c9b119e 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/VerificationOrderTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/VerificationOrderTest.cs @@ -16,7 +16,6 @@ public class VerificationOrderTest : ClientBasedLanguageServerTest { public async Task VerificationPriorityBasedOnChangesWorksWithMultipleFiles() { await SetUp(options => { options.Set(BoogieOptionBag.Cores, 1U); - options.Set(ServerCommand.ProjectMode, true); options.Set(ServerCommand.Verification, VerifyOnMode.ChangeProject); }); diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs index 9103a0e735e..07329f9ed7c 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs @@ -23,7 +23,6 @@ public async Task RunWithMultipleSimilarDocuments() { }".TrimStart(); await SetUp(options => { options.Set(ServerCommand.Verification, VerifyOnMode.Never); - options.Set(ServerCommand.ProjectMode, true); }); var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName()); await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName)); diff --git a/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs b/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs index c8c755f7234..c4f42797f85 100644 --- a/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs @@ -24,9 +24,6 @@ public async Task MultipleDocuments() { method Foo() returns (x: int) ensures x / 2 == 1; { return 2; }".TrimStart(); - await SetUp(options => { - options.Set(ServerCommand.ProjectMode, true); - }); var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName()); Directory.CreateDirectory(directory); await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName)); diff --git a/Source/DafnyLanguageServer/ServerCommand.cs b/Source/DafnyLanguageServer/ServerCommand.cs index 22e78ff0708..cb32f591ac0 100644 --- a/Source/DafnyLanguageServer/ServerCommand.cs +++ b/Source/DafnyLanguageServer/ServerCommand.cs @@ -16,7 +16,6 @@ static ServerCommand() { DafnyOptions.RegisterLegacyBinding(VerifySnapshots, (options, u) => options.VerifySnapshots = (int)u); DooFile.RegisterNoChecksNeeded( - ProjectMode, Verification, GhostIndicators, LineVerificationStatus, @@ -46,11 +45,6 @@ static ServerCommand() { Send notifications about the verification status of each line in the program. ".TrimStart()); - public static readonly Option ProjectMode = new("--project-mode", () => false, - "New mode with working with project files. Will become the default") { - IsHidden = true - }; - public static readonly Option VerifySnapshots = new("--cache-verification", @" (experimental) 0 - do not use any verification result caching (default) @@ -64,7 +58,6 @@ related locations }; public IEnumerable