From 2d0a360c9acbedb961e6bac9e0468ebafcce3047 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 6 Apr 2023 13:19:12 +0200 Subject: [PATCH 01/34] Draft of project file support for CLI commands --- Source/DafnyCore/DafnyCore.csproj | 2 + Source/DafnyCore/DafnyOptions.cs | 2 +- Source/DafnyCore/Options/ProjectFile.cs | 62 +++++++++++++++++++ .../DafnyDriver/Commands/CommandRegistry.cs | 24 ++++++- Test/cli/projectFile/dafny.toml | 4 ++ Test/cli/projectFile/notInput.dfy | 8 +++ Test/cli/projectFile/projectFile.dfy | 4 ++ Test/cli/projectFile/projectFile.dfy.expect | 3 + Test/cli/projectFile/src/input.dfy | 8 +++ 9 files changed, 113 insertions(+), 4 deletions(-) create mode 100644 Source/DafnyCore/Options/ProjectFile.cs create mode 100644 Test/cli/projectFile/dafny.toml create mode 100644 Test/cli/projectFile/notInput.dfy create mode 100644 Test/cli/projectFile/projectFile.dfy create mode 100644 Test/cli/projectFile/projectFile.dfy.expect create mode 100644 Test/cli/projectFile/src/input.dfy diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 43713d9ab17..4a8b2f89b56 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -27,10 +27,12 @@ + + diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index daa755b4273..f86ba61dc8e 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -35,7 +35,7 @@ public enum QuantifierSyntaxOptions { public record Options(IDictionary OptionArguments); public class DafnyOptions : Bpl.CommandLineOptions { - + public ProjectFile ProjectFile { get; set; } public bool NonGhostsUseHeap => Allocated == 1 || Allocated == 2; public bool AlwaysUseHeap => Allocated == 2; public bool CommonHeapUse => Allocated >= 2; diff --git a/Source/DafnyCore/Options/ProjectFile.cs b/Source/DafnyCore/Options/ProjectFile.cs new file mode 100644 index 00000000000..5bf0d1a4fae --- /dev/null +++ b/Source/DafnyCore/Options/ProjectFile.cs @@ -0,0 +1,62 @@ +using System; +using System.Collections; +using System.Collections.Generic; +using System.CommandLine; +using System.IO; +using System.Linq; +using System.Runtime.Serialization; +using System.Text.Json; +using Microsoft.CodeAnalysis; +using Microsoft.Extensions.FileSystemGlobbing; +using Microsoft.Extensions.FileSystemGlobbing.Abstractions; +using Tomlyn; + +namespace Microsoft.Dafny; + +/// +/// { +/// options: { +/// warn-shadowing: true +/// } +/// } +/// +public class ProjectFile { + [IgnoreDataMember] + public Uri Uri { get; set; } + public string[] Includes { get; set; } + public Dictionary Options { get; set; } + + public static ProjectFile Open(Uri uri) { + var file = File.Open(uri.LocalPath, FileMode.Open); + var model = Toml.ToModel(new StreamReader(file).ReadToEnd()); + model.Uri = uri; + return model; + } + + public void ApplyToOptions(Command command, DafnyOptions options) { + ProcessIncludes(options); + } + + private void ProcessIncludes(DafnyOptions options) + { + var matcher = new Matcher(); + foreach (var includeGlob in Includes) + { + matcher.AddInclude(includeGlob); + } + + var root = Path.GetDirectoryName(Uri.LocalPath); + var result = matcher.Execute(new DirectoryInfoWrapper(new DirectoryInfo(root!))); + var files = result.Files.Select(f => Path.Combine(root, f.Path)); + foreach (var file in files) + { + options.AddFile(file); + } + } + + public bool TryGetValue(Option option, out object value) { + var name = option.Name.StartsWith("--") ? option.Name.Substring(2) : option.Name; + + return Options.TryGetValue(name, out value); + } +} \ No newline at end of file diff --git a/Source/DafnyDriver/Commands/CommandRegistry.cs b/Source/DafnyDriver/Commands/CommandRegistry.cs index 7975d84c438..116f7def78f 100644 --- a/Source/DafnyDriver/Commands/CommandRegistry.cs +++ b/Source/DafnyDriver/Commands/CommandRegistry.cs @@ -12,6 +12,7 @@ using Microsoft.Boogie; using Microsoft.Dafny.LanguageServer; using OmniSharp.Extensions.LanguageServer.Protocol.Models; +using Command = System.CommandLine.Command; namespace Microsoft.Dafny; @@ -112,17 +113,22 @@ void CommandHandler(InvocationContext context) { var singleFile = context.ParseResult.GetValueForArgument(FileArgument); if (singleFile != null) { - dafnyOptions.AddFile(singleFile.FullName); + ProcessFile(command, dafnyOptions, singleFile); } var files = context.ParseResult.GetValueForArgument(ICommandSpec.FilesArgument); if (files != null) { foreach (var file in files) { - dafnyOptions.AddFile(file.FullName); + ProcessFile(command, dafnyOptions, file); } } foreach (var option in command.Options) { - var value = context.ParseResult.GetValueForOption(option); + var result = context.ParseResult.FindResultFor(option); + object projectFileValue = null; + var hasProjectFileValue = dafnyOptions.ProjectFile?.TryGetValue(option, out projectFileValue) ?? false; + var value = result == null && hasProjectFileValue + ? projectFileValue + : context.ParseResult.GetValueForOption(option); options.OptionArguments[option] = value; dafnyOptions.ApplyBinding(option); } @@ -151,6 +157,18 @@ void CommandHandler(InvocationContext context) { return new ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult.PREPROCESSING_ERROR); } + private static void ProcessFile(Command command, DafnyOptions dafnyOptions, FileInfo singleFile) + { + if (Path.GetExtension(singleFile.FullName) == ".toml") { + var projectFile = ProjectFile.Open(new Uri(singleFile.FullName)); + // TODO check for existing + dafnyOptions.ProjectFile = projectFile; + projectFile.ApplyToOptions(command, dafnyOptions); + } else { + dafnyOptions.AddFile(singleFile.FullName); + } + } + private static CommandLineBuilder AddDeveloperHelp(RootCommand rootCommand, CommandLineBuilder builder) { var languageDeveloperHelp = new Option(ToolchainDebuggingHelpName, "Show help and usage information, including options designed for developing the Dafny language and toolchain."); diff --git a/Test/cli/projectFile/dafny.toml b/Test/cli/projectFile/dafny.toml new file mode 100644 index 00000000000..645c92da170 --- /dev/null +++ b/Test/cli/projectFile/dafny.toml @@ -0,0 +1,4 @@ +includes = ["src/**/*"] + +[options] +warn-shadowing = true \ No newline at end of file diff --git a/Test/cli/projectFile/notInput.dfy b/Test/cli/projectFile/notInput.dfy new file mode 100644 index 00000000000..0e5bca9d1d3 --- /dev/null +++ b/Test/cli/projectFile/notInput.dfy @@ -0,0 +1,8 @@ +// RUN: echo "" + +method Foo() { + var y := 3; + if (true) { + var y := 4; + } +} \ No newline at end of file diff --git a/Test/cli/projectFile/projectFile.dfy b/Test/cli/projectFile/projectFile.dfy new file mode 100644 index 00000000000..44c33896e3c --- /dev/null +++ b/Test/cli/projectFile/projectFile.dfy @@ -0,0 +1,4 @@ +// RUN: %baredafny resolve "%S/dafny.toml" > "%t" +// RUN: %diff "%s.expect" "%t" + +// How do I decide if I have a toml file or a .dfy file? \ No newline at end of file diff --git a/Test/cli/projectFile/projectFile.dfy.expect b/Test/cli/projectFile/projectFile.dfy.expect new file mode 100644 index 00000000000..24d53539907 --- /dev/null +++ b/Test/cli/projectFile/projectFile.dfy.expect @@ -0,0 +1,3 @@ +/Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/src/input.dfy(6,8): Warning: Shadowed local-variable name: x + +Dafny program verifier did not attempt verification diff --git a/Test/cli/projectFile/src/input.dfy b/Test/cli/projectFile/src/input.dfy new file mode 100644 index 00000000000..3aff32ba633 --- /dev/null +++ b/Test/cli/projectFile/src/input.dfy @@ -0,0 +1,8 @@ +// RUN: echo "" + +method Foo() { + var x := 3; + if (true) { + var x := 4; + } +} \ No newline at end of file From e84f9a4038e218f19f532363cbbac8d0b5e36fe3 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 6 Apr 2023 15:18:07 +0200 Subject: [PATCH 02/34] Add error handling and support for excludes --- Source/DafnyCore/Options/ProjectFile.cs | 42 ++++++++++++++++--- .../DafnyDriver/Commands/CommandRegistry.cs | 24 +++++++++-- Test/cli/projectFile/brokenDafny.toml | 4 ++ Test/cli/projectFile/dafny.toml | 1 + Test/cli/projectFile/projectFile.dfy | 2 + Test/cli/projectFile/projectFile.dfy.expect | 4 ++ Test/cli/projectFile/src/excluded.dfy | 8 ++++ 7 files changed, 75 insertions(+), 10 deletions(-) create mode 100644 Test/cli/projectFile/brokenDafny.toml create mode 100644 Test/cli/projectFile/src/excluded.dfy diff --git a/Source/DafnyCore/Options/ProjectFile.cs b/Source/DafnyCore/Options/ProjectFile.cs index 5bf0d1a4fae..cf91af2a6ab 100644 --- a/Source/DafnyCore/Options/ProjectFile.cs +++ b/Source/DafnyCore/Options/ProjectFile.cs @@ -4,8 +4,10 @@ using System.CommandLine; using System.IO; using System.Linq; +using System.Reflection.Metadata; using System.Runtime.Serialization; using System.Text.Json; +using System.Text.RegularExpressions; using Microsoft.CodeAnalysis; using Microsoft.Extensions.FileSystemGlobbing; using Microsoft.Extensions.FileSystemGlobbing.Abstractions; @@ -24,17 +26,45 @@ public class ProjectFile { [IgnoreDataMember] public Uri Uri { get; set; } public string[] Includes { get; set; } + public string[] Excludes { get; set; } public Dictionary Options { get; set; } - public static ProjectFile Open(Uri uri) { - var file = File.Open(uri.LocalPath, FileMode.Open); - var model = Toml.ToModel(new StreamReader(file).ReadToEnd()); - model.Uri = uri; - return model; + public static ProjectFile Open(Uri uri, TextWriter errorWriter) { + try { + var file = File.Open(uri.LocalPath, FileMode.Open); + var model = Toml.ToModel(new StreamReader(file).ReadToEnd(), null, new TomlModelOptions()); + model.Uri = uri; + return model; + + } catch (FileNotFoundException e) { + errorWriter.WriteLine(e.Message); + return null; + } catch (TomlException tomlException) { + errorWriter.WriteLine($"The Dafny project file {uri.LocalPath} contains the following errors:"); + errorWriter.WriteLine(tomlException.Message.Replace( + $"was not found on object type {typeof(ProjectFile).FullName}", + "does not exist")); + return null; + } } public void ApplyToOptions(Command command, DafnyOptions options) { - ProcessIncludes(options); + var matcher = new Matcher(); + foreach (var includeGlob in Includes) + { + matcher.AddInclude(includeGlob); + } + foreach (var includeGlob in Excludes) { + matcher.AddExclude(includeGlob); + } + + var root = Path.GetDirectoryName(Uri.LocalPath); + var result = matcher.Execute(new DirectoryInfoWrapper(new DirectoryInfo(root!))); + var files = result.Files.Select(f => Path.Combine(root, f.Path)); + foreach (var file in files) + { + options.AddFile(file); + } } private void ProcessIncludes(DafnyOptions options) diff --git a/Source/DafnyDriver/Commands/CommandRegistry.cs b/Source/DafnyDriver/Commands/CommandRegistry.cs index 116f7def78f..f417b6ca19d 100644 --- a/Source/DafnyDriver/Commands/CommandRegistry.cs +++ b/Source/DafnyDriver/Commands/CommandRegistry.cs @@ -106,6 +106,7 @@ public static ParseArgumentResult Create(string[] arguments) { rootCommand.AddCommand(command); } + var failedToProcessFile = false; void CommandHandler(InvocationContext context) { wasInvoked = true; var command = context.ParseResult.CommandResult.Command; @@ -113,12 +114,18 @@ void CommandHandler(InvocationContext context) { var singleFile = context.ParseResult.GetValueForArgument(FileArgument); if (singleFile != null) { - ProcessFile(command, dafnyOptions, singleFile); + if (!ProcessFile(command, dafnyOptions, singleFile)) { + failedToProcessFile = true; + return; + } } var files = context.ParseResult.GetValueForArgument(ICommandSpec.FilesArgument); if (files != null) { foreach (var file in files) { - ProcessFile(command, dafnyOptions, file); + if (!ProcessFile(command, dafnyOptions, file)) { + failedToProcessFile = true; + return; + } } } @@ -143,6 +150,11 @@ void CommandHandler(InvocationContext context) { #pragma warning disable VSTHRD002 var exitCode = builder.Build().InvokeAsync(arguments).Result; #pragma warning restore VSTHRD002 + + if (failedToProcessFile) { + return new ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult.PREPROCESSING_ERROR); + } + if (!wasInvoked) { if (exitCode == 0) { return new ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult.OK_EXIT_EARLY); @@ -157,16 +169,20 @@ void CommandHandler(InvocationContext context) { return new ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult.PREPROCESSING_ERROR); } - private static void ProcessFile(Command command, DafnyOptions dafnyOptions, FileInfo singleFile) + private static bool ProcessFile(Command command, DafnyOptions dafnyOptions, FileInfo singleFile) { if (Path.GetExtension(singleFile.FullName) == ".toml") { - var projectFile = ProjectFile.Open(new Uri(singleFile.FullName)); + var projectFile = ProjectFile.Open(new Uri(singleFile.FullName), Console.Error); + if (projectFile == null) { + return false; + } // TODO check for existing dafnyOptions.ProjectFile = projectFile; projectFile.ApplyToOptions(command, dafnyOptions); } else { dafnyOptions.AddFile(singleFile.FullName); } + return true; } private static CommandLineBuilder AddDeveloperHelp(RootCommand rootCommand, CommandLineBuilder builder) { diff --git a/Test/cli/projectFile/brokenDafny.toml b/Test/cli/projectFile/brokenDafny.toml new file mode 100644 index 00000000000..3fe6323945a --- /dev/null +++ b/Test/cli/projectFile/brokenDafny.toml @@ -0,0 +1,4 @@ +includdddes = ["src/**/*"] + +[options] +warn-shadowing = true \ No newline at end of file diff --git a/Test/cli/projectFile/dafny.toml b/Test/cli/projectFile/dafny.toml index 645c92da170..48c886a1b0f 100644 --- a/Test/cli/projectFile/dafny.toml +++ b/Test/cli/projectFile/dafny.toml @@ -1,4 +1,5 @@ includes = ["src/**/*"] +excludes = ["**/excluded.dfy"] [options] warn-shadowing = true \ No newline at end of file diff --git a/Test/cli/projectFile/projectFile.dfy b/Test/cli/projectFile/projectFile.dfy index 44c33896e3c..3b103a9115b 100644 --- a/Test/cli/projectFile/projectFile.dfy +++ b/Test/cli/projectFile/projectFile.dfy @@ -1,4 +1,6 @@ // RUN: %baredafny resolve "%S/dafny.toml" > "%t" +// RUN: ! %baredafny resolve "%S/brokenDafny.toml" 2>> "%t" +// RUN: ! %baredafny resolve "%S/doesNotExist.toml" 2>> "%t" // RUN: %diff "%s.expect" "%t" // How do I decide if I have a toml file or a .dfy file? \ No newline at end of file diff --git a/Test/cli/projectFile/projectFile.dfy.expect b/Test/cli/projectFile/projectFile.dfy.expect index 24d53539907..083a5703031 100644 --- a/Test/cli/projectFile/projectFile.dfy.expect +++ b/Test/cli/projectFile/projectFile.dfy.expect @@ -1,3 +1,7 @@ /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/src/input.dfy(6,8): Warning: Shadowed local-variable name: x Dafny program verifier did not attempt verification +The Dafny project file /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/brokenDafny.toml contains the following errors: +(1,1) : error : The property `includdddes` does not exist + +Could not find file '/Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/doesNotExist.toml'. diff --git a/Test/cli/projectFile/src/excluded.dfy b/Test/cli/projectFile/src/excluded.dfy new file mode 100644 index 00000000000..ec506c35223 --- /dev/null +++ b/Test/cli/projectFile/src/excluded.dfy @@ -0,0 +1,8 @@ +// RUN: echo "" + +method Foo() { + var z := 3; + if (true) { + var z := 4; + } +} \ No newline at end of file From 93a4dfb9738940a4ccbc225275ea3fb9f2e31f6b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 6 Apr 2023 15:24:02 +0200 Subject: [PATCH 03/34] Improvements --- Source/DafnyCore/Options/ProjectFile.cs | 33 ++++----------------- Test/cli/projectFile/projectFile.dfy | 4 +-- Test/cli/projectFile/projectFile.dfy.expect | 2 +- 3 files changed, 8 insertions(+), 31 deletions(-) diff --git a/Source/DafnyCore/Options/ProjectFile.cs b/Source/DafnyCore/Options/ProjectFile.cs index cf91af2a6ab..f3b75e51c11 100644 --- a/Source/DafnyCore/Options/ProjectFile.cs +++ b/Source/DafnyCore/Options/ProjectFile.cs @@ -15,13 +15,6 @@ namespace Microsoft.Dafny; -/// -/// { -/// options: { -/// warn-shadowing: true -/// } -/// } -/// public class ProjectFile { [IgnoreDataMember] public Uri Uri { get; set; } @@ -41,9 +34,12 @@ public static ProjectFile Open(Uri uri, TextWriter errorWriter) { return null; } catch (TomlException tomlException) { errorWriter.WriteLine($"The Dafny project file {uri.LocalPath} contains the following errors:"); - errorWriter.WriteLine(tomlException.Message.Replace( - $"was not found on object type {typeof(ProjectFile).FullName}", - "does not exist")); + var regex = new Regex( + @$"\((\d+),(\d+)\) : error : The property `(\w+)` was not found on object type {typeof(ProjectFile).FullName}"); + var newMessage = regex.Replace(tomlException.Message, + match => + $"({match.Groups[1].Value},{match.Groups[2].Value}): the property {match.Groups[3].Value} does not exist."); + errorWriter.WriteLine(newMessage); return null; } } @@ -67,23 +63,6 @@ public void ApplyToOptions(Command command, DafnyOptions options) { } } - private void ProcessIncludes(DafnyOptions options) - { - var matcher = new Matcher(); - foreach (var includeGlob in Includes) - { - matcher.AddInclude(includeGlob); - } - - var root = Path.GetDirectoryName(Uri.LocalPath); - var result = matcher.Execute(new DirectoryInfoWrapper(new DirectoryInfo(root!))); - var files = result.Files.Select(f => Path.Combine(root, f.Path)); - foreach (var file in files) - { - options.AddFile(file); - } - } - public bool TryGetValue(Option option, out object value) { var name = option.Name.StartsWith("--") ? option.Name.Substring(2) : option.Name; diff --git a/Test/cli/projectFile/projectFile.dfy b/Test/cli/projectFile/projectFile.dfy index 3b103a9115b..eeaf759b8d4 100644 --- a/Test/cli/projectFile/projectFile.dfy +++ b/Test/cli/projectFile/projectFile.dfy @@ -1,6 +1,4 @@ // RUN: %baredafny resolve "%S/dafny.toml" > "%t" // RUN: ! %baredafny resolve "%S/brokenDafny.toml" 2>> "%t" // RUN: ! %baredafny resolve "%S/doesNotExist.toml" 2>> "%t" -// RUN: %diff "%s.expect" "%t" - -// How do I decide if I have a toml file or a .dfy file? \ No newline at end of file +// RUN: %diff "%s.expect" "%t" \ No newline at end of file diff --git a/Test/cli/projectFile/projectFile.dfy.expect b/Test/cli/projectFile/projectFile.dfy.expect index 083a5703031..02a1179434a 100644 --- a/Test/cli/projectFile/projectFile.dfy.expect +++ b/Test/cli/projectFile/projectFile.dfy.expect @@ -2,6 +2,6 @@ Dafny program verifier did not attempt verification The Dafny project file /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/brokenDafny.toml contains the following errors: -(1,1) : error : The property `includdddes` does not exist +(1,1): the property includdddes does not exist. Could not find file '/Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/doesNotExist.toml'. From fbbdd165d511fe7f59363f520be380eeb8db3efe Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 6 Apr 2023 15:57:19 +0200 Subject: [PATCH 04/34] Update documentation --- Source/DafnyCore/Options/ICommandSpec.cs | 2 +- Source/DafnyDriver/Commands/CommandRegistry.cs | 2 +- docs/DafnyRef/UserGuide.md | 15 +++++++++++++++ 3 files changed, 17 insertions(+), 2 deletions(-) diff --git a/Source/DafnyCore/Options/ICommandSpec.cs b/Source/DafnyCore/Options/ICommandSpec.cs index 456f5cc50e8..1017f2270f8 100644 --- a/Source/DafnyCore/Options/ICommandSpec.cs +++ b/Source/DafnyCore/Options/ICommandSpec.cs @@ -15,7 +15,7 @@ public interface ICommandSpec { static ICommandSpec() { FilesArgument = new("file", r => { return r.Tokens.Where(t => !string.IsNullOrEmpty(t.Value)).Select(t => new FileInfo(t.Value)).ToList(); - }, true, "input files"); + }, true, "Dafny input files and/or a Dafny project file"); } public static Argument> FilesArgument { get; } diff --git a/Source/DafnyDriver/Commands/CommandRegistry.cs b/Source/DafnyDriver/Commands/CommandRegistry.cs index f417b6ca19d..c8f228b9221 100644 --- a/Source/DafnyDriver/Commands/CommandRegistry.cs +++ b/Source/DafnyDriver/Commands/CommandRegistry.cs @@ -44,7 +44,7 @@ static CommandRegistry() { AddCommand(new DeadCodeCommand()); AddCommand(new AuditCommand()); - FileArgument = new Argument("file", "input file"); + FileArgument = new Argument("file", "Dafny input file or Dafny project file"); } public static Argument FileArgument { get; } diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md index 0b3e446da00..71b7afe3080 100644 --- a/docs/DafnyRef/UserGuide.md +++ b/docs/DafnyRef/UserGuide.md @@ -571,6 +571,21 @@ Most output from `dafny` is directed to the standard output of the shell invokin - Dafny `expect` statements (when they fail) send a message to **standard-out**. - Dafny I/O libraries send output explicitly to either **standard-out or standard-error** +### 13.5.5. Project files + +Commands on the Dafny CLI that can be passed a Dafny file, can also be passed a Dafny project file. Such a project file may define which Dafny files the project contains, and which Dafny options it uses. The project file must be a [TOML](https://toml.io/en/) file, ending in the extension `.toml`. Here's an example of a Dafny project file: + +```toml +includes = ["src/**/*.dfy"] +excludes = ["**/ignore.dfy"] + +[options] + enforce-determinism = true + warn-shadowing = true +``` + +Options are applied to a command if they can be. Invalid options are ignored. + ## 13.6. Verification {#sec-verification} In this section, we suggest a methodology to figure out [why a single assertion might not hold](#sec-verification-debugging), we propose techniques to deal with [assertions that slow a proof down](#sec-verification-debugging-slow), we explain how to [verify assertions in parallel or in a focused way](#sec-assertion-batches), and we also give some more examples of [useful options and attributes to control verification](#sec-command-line-options-and-attributes-for-verification). From c0c070588ae16f7fa72df93ee3cb879beede2c07 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 6 Apr 2023 16:09:22 +0200 Subject: [PATCH 05/34] Add language server test for project files --- .../DafnyLanguageServer.Test.csproj | 6 ++++++ .../ProjectFiles/ProjectFiles.cs | 21 +++++++++++++++++++ .../ProjectFiles/TestFiles/dafny.toml | 4 ++++ .../ProjectFiles/TestFiles/src/foo.dfy | 6 ++++++ 4 files changed, 37 insertions(+) create mode 100644 Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFiles.cs create mode 100644 Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/dafny.toml create mode 100644 Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/src/foo.dfy diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj index 4cc3ec4ad04..28a027cd33c 100644 --- a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj +++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj @@ -68,6 +68,12 @@ PreserveNewest + + Always + + + Always + diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFiles.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFiles.cs new file mode 100644 index 00000000000..5630079dc40 --- /dev/null +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFiles.cs @@ -0,0 +1,21 @@ +using System.IO; +using System.Threading.Tasks; +using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; +using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; +using Xunit; + +namespace Microsoft.Dafny.LanguageServer.IntegrationTest; + +public class ProjectFiles : ClientBasedLanguageServerTest { + [Fact] + public async Task ProjectFileIsFound() { + var filePath = Path.Combine(Directory.GetCurrentDirectory(), "ProjectFiles/TestFiles/src/foo.dfy"); + var source = await File.ReadAllTextAsync(filePath); + var documentItem = CreateTestDocument(source, filePath); + await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken); + + Assert.Single(diagnostics); + Assert.Contains("shadows", diagnostics[0].Message); + } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/dafny.toml b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/dafny.toml new file mode 100644 index 00000000000..a450e981c8b --- /dev/null +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/dafny.toml @@ -0,0 +1,4 @@ +includes = ["src/**/*.dfy"] + +[options] +warn-shadowing = true diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/src/foo.dfy b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/src/foo.dfy new file mode 100644 index 00000000000..49a3a161baa --- /dev/null +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/src/foo.dfy @@ -0,0 +1,6 @@ +method Foo() { + var x := 3; + if (true) { + var x := 4; + } +} \ No newline at end of file From 2ddb0d4db1db0e1762c8757519bda350ad43dc45 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 6 Apr 2023 16:58:13 +0200 Subject: [PATCH 06/34] Server project file test passes --- Source/DafnyCore/DafnyOptions.cs | 1 + Source/DafnyCore/Options/ProjectFile.cs | 2 +- .../DafnyDriver/Commands/CommandRegistry.cs | 4 +- .../DafnyLanguageServerTestBase.cs | 4 +- .../ProjectFiles/ProjectFiles.cs | 2 +- .../Unit/TextDocumentLoaderTest.cs | 4 +- .../Various/ExceptionTests.cs | 5 ++- Source/DafnyLanguageServer/ServerCommand.cs | 8 +++- .../Workspace/Compilation.cs | 5 ++- .../Workspace/DocumentManager.cs | 42 ++++++++++++++++++- .../Workspace/DocumentManagerDatabase.cs | 1 - .../Workspace/ITextDocumentLoader.cs | 4 +- .../Workspace/TextDocumentLoader.cs | 13 +++--- docs/DafnyRef/UserGuide.md | 2 +- 14 files changed, 71 insertions(+), 26 deletions(-) diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index f86ba61dc8e..4bedd0b63e4 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -35,6 +35,7 @@ public enum QuantifierSyntaxOptions { public record Options(IDictionary OptionArguments); public class DafnyOptions : Bpl.CommandLineOptions { + public static DafnyOptions Default = new DafnyOptions(); public ProjectFile ProjectFile { get; set; } public bool NonGhostsUseHeap => Allocated == 1 || Allocated == 2; public bool AlwaysUseHeap => Allocated == 2; diff --git a/Source/DafnyCore/Options/ProjectFile.cs b/Source/DafnyCore/Options/ProjectFile.cs index f3b75e51c11..c448a202448 100644 --- a/Source/DafnyCore/Options/ProjectFile.cs +++ b/Source/DafnyCore/Options/ProjectFile.cs @@ -44,7 +44,7 @@ public static ProjectFile Open(Uri uri, TextWriter errorWriter) { } } - public void ApplyToOptions(Command command, DafnyOptions options) { + public void ApplyToOptions(DafnyOptions options) { var matcher = new Matcher(); foreach (var includeGlob in Includes) { diff --git a/Source/DafnyDriver/Commands/CommandRegistry.cs b/Source/DafnyDriver/Commands/CommandRegistry.cs index c8f228b9221..3f3a62076b4 100644 --- a/Source/DafnyDriver/Commands/CommandRegistry.cs +++ b/Source/DafnyDriver/Commands/CommandRegistry.cs @@ -38,7 +38,7 @@ static CommandRegistry() { AddCommand(new TranslateCommand()); AddCommand(new FormatCommand()); AddCommand(new MeasureComplexityCommand()); - AddCommand(new ServerCommand()); + AddCommand(ServerCommand.Instance); AddCommand(new TestCommand()); AddCommand(new GenerateTestsCommand()); AddCommand(new DeadCodeCommand()); @@ -178,7 +178,7 @@ private static bool ProcessFile(Command command, DafnyOptions dafnyOptions, File } // TODO check for existing dafnyOptions.ProjectFile = projectFile; - projectFile.ApplyToOptions(command, dafnyOptions); + projectFile.ApplyToOptions(dafnyOptions); } else { dafnyOptions.AddFile(singleFile.FullName); } diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs index 64e77f043bc..1e7fb744a56 100644 --- a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs +++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs @@ -84,12 +84,12 @@ void NewServerOptionsAction(LanguageServerOptions options) { private static void ApplyDefaultOptionValues(DafnyOptions dafnyOptions) { var testCommand = new System.CommandLine.Command("test"); - foreach (var serverOption in new ServerCommand().Options) { + foreach (var serverOption in ServerCommand.Instance.Options) { testCommand.AddOption(serverOption); } var result = testCommand.Parse("test"); - foreach (var option in new ServerCommand().Options) { + foreach (var option in ServerCommand.Instance.Options) { if (!dafnyOptions.Options.OptionArguments.ContainsKey(option)) { var value = result.GetValueForOption(option); diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFiles.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFiles.cs index 5630079dc40..614f1473f58 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFiles.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFiles.cs @@ -16,6 +16,6 @@ public async Task ProjectFileIsFound() { var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken); Assert.Single(diagnostics); - Assert.Contains("shadows", diagnostics[0].Message); + Assert.Equal("Shadowed local-variable name: x", diagnostics[0].Message); } } \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs index 39ca329e553..41c6bfc0b31 100644 --- a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs @@ -53,7 +53,7 @@ public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() { var source = new CancellationTokenSource(); parser.Setup(p => p.Parse(It.IsAny(), It.IsAny(), It.IsAny())).Callback(() => source.Cancel()) .Throws(); - var task = textDocumentLoader.LoadAsync(CreateTestDocument(), source.Token); + var task = textDocumentLoader.LoadAsync(DafnyOptions.Default, CreateTestDocument(), source.Token); try { await task; Assert.Fail("document load was not cancelled"); @@ -68,7 +68,7 @@ public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() { public async Task LoadReturnsFaultedTaskIfAnyExceptionOccured() { parser.Setup(p => p.Parse(It.IsAny(), It.IsAny(), It.IsAny())) .Throws(); - var task = textDocumentLoader.LoadAsync(CreateTestDocument(), default); + var task = textDocumentLoader.LoadAsync(DafnyOptions.Default, CreateTestDocument(), default); try { await task; Assert.Fail("document load did not fail"); diff --git a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs index 56f7e7a004d..f18d1caf969 100644 --- a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs +++ b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs @@ -123,11 +123,12 @@ public IdeState CreateUnloaded(DocumentTextBuffer textDocument, CancellationToke return loader.CreateUnloaded(textDocument, cancellationToken); } - public Task LoadAsync(DocumentTextBuffer textDocument, CancellationToken cancellationToken) { + public Task LoadAsync(DafnyOptions options, DocumentTextBuffer textDocument, + CancellationToken cancellationToken) { if (tests.CrashOnLoad) { throw new IOException("crash"); } - return loader.LoadAsync(textDocument, cancellationToken); + return loader.LoadAsync(options, textDocument, cancellationToken); } } } diff --git a/Source/DafnyLanguageServer/ServerCommand.cs b/Source/DafnyLanguageServer/ServerCommand.cs index 35aea9985c7..52ac741f45d 100644 --- a/Source/DafnyLanguageServer/ServerCommand.cs +++ b/Source/DafnyLanguageServer/ServerCommand.cs @@ -8,6 +8,11 @@ namespace Microsoft.Dafny.LanguageServer; public class ServerCommand : ICommandSpec { + public static readonly ServerCommand Instance = new(); + + private ServerCommand() + { + } static ServerCommand() { DafnyOptions.RegisterLegacyBinding(VerifySnapshots, (options, u) => options.VerifySnapshots = (int)u); @@ -53,8 +58,7 @@ related locations Concat(ICommandSpec.ResolverOptions); public Command Create() { - var command = new Command("server", "Start the Dafny language server"); - return command; + return new Command("server", "Start the Dafny language server"); } public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationContext context) { diff --git a/Source/DafnyLanguageServer/Workspace/Compilation.cs b/Source/DafnyLanguageServer/Workspace/Compilation.cs index 09ecf63f3e8..8780723af50 100644 --- a/Source/DafnyLanguageServer/Workspace/Compilation.cs +++ b/Source/DafnyLanguageServer/Workspace/Compilation.cs @@ -52,9 +52,10 @@ public class Compilation { public Task TranslatedDocument { get; } public Compilation(IServiceProvider services, + DafnyOptions options, DocumentTextBuffer textBuffer, VerificationTree? migratedVerificationTree) { - options = services.GetRequiredService(); + this.options = options; logger = services.GetRequiredService>(); documentLoader = services.GetRequiredService(); notificationPublisher = services.GetRequiredService(); @@ -79,7 +80,7 @@ public void Start() { private async Task ResolveAsync() { try { await started.Task; - var documentAfterParsing = await documentLoader.LoadAsync(TextBuffer, cancellationSource.Token); + var documentAfterParsing = await documentLoader.LoadAsync(options, TextBuffer, cancellationSource.Token); // TODO, let gutter icon publications also used the published CompilationView. var state = documentAfterParsing.InitialIdeState(options); diff --git a/Source/DafnyLanguageServer/Workspace/DocumentManager.cs b/Source/DafnyLanguageServer/Workspace/DocumentManager.cs index 80de9a8b72b..9ca82335d17 100644 --- a/Source/DafnyLanguageServer/Workspace/DocumentManager.cs +++ b/Source/DafnyLanguageServer/Workspace/DocumentManager.cs @@ -1,5 +1,6 @@ using System; using System.Collections.Generic; +using System.IO; using System.Linq; using System.Reactive.Linq; using System.Threading; @@ -10,6 +11,7 @@ using Microsoft.Dafny.LanguageServer.Workspace.Notifications; using Microsoft.Extensions.DependencyInjection; using Microsoft.Extensions.Logging; +using OmniSharp.Extensions.LanguageServer.Protocol; using OmniSharp.Extensions.LanguageServer.Protocol.Models; using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; @@ -53,7 +55,8 @@ public DocumentManager( services.GetRequiredService(), document); Compilation = new Compilation( - services, + services, + DetermineDocumentOptions(options, document.Uri), document, null); @@ -104,8 +107,11 @@ public void UpdateDocument(DidChangeTextDocumentParams documentChange) { relocator.RelocateRange(range, documentChange, CancellationToken.None))). Where(r => r != null).Take(MaxRememberedChanges).ToList()!; } + + var dafnyOptions = DetermineDocumentOptions(options, documentChange.TextDocument.Uri); Compilation = new Compilation( services, + dafnyOptions, updatedText, // TODO do not pass this to CompilationManager but instead use it in FillMissingStateUsingLastPublishedDocument migratedVerificationTree @@ -127,6 +133,40 @@ public void UpdateDocument(DidChangeTextDocumentParams documentChange) { Compilation.Start(); } + private static DafnyOptions DetermineDocumentOptions(DafnyOptions serverOptions, DocumentUri uri) { + ProjectFile? projectFile = null; + + var folder = Path.GetDirectoryName(uri.Path); + while (folder != null) { + var children = Directory.GetFiles(folder, "dafny.toml"); + if (children.Length > 0) { + var errorWriter = TextWriter.Null; + projectFile = ProjectFile.Open(new Uri(children[0]), errorWriter); + if (projectFile != null) { + break; + } + } + folder = Path.GetDirectoryName(folder); + } + + if (projectFile != null) { + var result = new DafnyOptions(serverOptions); + + foreach (var option in ServerCommand.Instance.Options) { + object? projectFileValue = null; + var hasProjectFileValue = projectFile?.TryGetValue(option, out projectFileValue) ?? false; + if (hasProjectFileValue) { + result.Options.OptionArguments[option] = projectFileValue; + result.ApplyBinding(option); + } + } + + return result; + } + + return serverOptions; + } + private Dictionary MigrateImplementationViews(DidChangeTextDocumentParams documentChange, IReadOnlyDictionary oldVerificationDiagnostics) { var result = new Dictionary(); diff --git a/Source/DafnyLanguageServer/Workspace/DocumentManagerDatabase.cs b/Source/DafnyLanguageServer/Workspace/DocumentManagerDatabase.cs index 4977992cac9..65026b8702a 100644 --- a/Source/DafnyLanguageServer/Workspace/DocumentManagerDatabase.cs +++ b/Source/DafnyLanguageServer/Workspace/DocumentManagerDatabase.cs @@ -18,7 +18,6 @@ public class DocumentManagerDatabase : IDocumentDatabase { private readonly Dictionary documents = new(); public DocumentManagerDatabase(IServiceProvider services) { - this.services = services; } diff --git a/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs index b66fb55baf1..268069c040d 100644 --- a/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs @@ -26,11 +26,13 @@ public interface ITextDocumentLoader { /// Loads the specified document item of the language server and applies the necessary steps /// to generate a dafny document instance. /// + /// /// The text document to load. /// A token to cancel the update operation before its completion. /// The loaded dafny document. /// Thrown when the cancellation was requested before completion. /// Thrown if the cancellation token was disposed before the completion. - Task LoadAsync(DocumentTextBuffer textDocument, CancellationToken cancellationToken); + Task LoadAsync(DafnyOptions options, DocumentTextBuffer textDocument, + CancellationToken cancellationToken); } } diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs index cf2f449398c..73edeb83bb3 100644 --- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs @@ -23,7 +23,6 @@ public class TextDocumentLoader : ITextDocumentLoader { private const int ResolverMaxStackSize = 0x10000000; // 256MB private static readonly ThreadTaskScheduler ResolverScheduler = new(ResolverMaxStackSize); - private readonly DafnyOptions options; private readonly IDafnyParser parser; private readonly ISymbolResolver symbolResolver; private readonly ISymbolTableFactory symbolTableFactory; @@ -33,7 +32,6 @@ public class TextDocumentLoader : ITextDocumentLoader { protected readonly INotificationPublisher NotificationPublisher; protected TextDocumentLoader( - DafnyOptions options, ILoggerFactory loggerFactory, IDafnyParser parser, ISymbolResolver symbolResolver, @@ -41,7 +39,6 @@ protected TextDocumentLoader( IGhostStateDiagnosticCollector ghostStateDiagnosticCollector, ICompilationStatusNotificationPublisher statusPublisher, INotificationPublisher notificationPublisher) { - this.options = options; this.parser = parser; this.symbolResolver = symbolResolver; this.symbolTableFactory = symbolTableFactory; @@ -61,7 +58,7 @@ public static TextDocumentLoader Create( ILoggerFactory loggerFactory, INotificationPublisher notificationPublisher ) { - return new TextDocumentLoader(options, loggerFactory, parser, symbolResolver, symbolTableFactory, ghostStateDiagnosticCollector, statusPublisher, notificationPublisher); + return new TextDocumentLoader(loggerFactory, parser, symbolResolver, symbolTableFactory, ghostStateDiagnosticCollector, statusPublisher, notificationPublisher); } public IdeState CreateUnloaded(DocumentTextBuffer textDocument, CancellationToken cancellationToken) { @@ -75,16 +72,16 @@ public IdeState CreateUnloaded(DocumentTextBuffer textDocument, CancellationToke ); } - public async Task LoadAsync(DocumentTextBuffer textDocument, + public async Task LoadAsync(DafnyOptions options, DocumentTextBuffer textDocument, CancellationToken cancellationToken) { #pragma warning disable CS1998 return await await Task.Factory.StartNew( - async () => LoadInternal(textDocument, cancellationToken), cancellationToken, + async () => LoadInternal(options, textDocument, cancellationToken), cancellationToken, #pragma warning restore CS1998 TaskCreationOptions.None, ResolverScheduler); } - private DocumentAfterParsing LoadInternal(DocumentTextBuffer textDocument, + private DocumentAfterParsing LoadInternal(DafnyOptions options, DocumentTextBuffer textDocument, CancellationToken cancellationToken) { var errorReporter = new DiagnosticErrorReporter(options, textDocument.Text, textDocument.Uri); statusPublisher.SendStatusNotification(textDocument, CompilationStatus.ResolutionStarted); @@ -124,7 +121,7 @@ IReadOnlyList diagnostics textDocument, diagnostics, SymbolTable.Empty(), - SignatureAndCompletionTable.Empty(options, textDocument), + SignatureAndCompletionTable.Empty(DafnyOptions.Default, textDocument), new Dictionary(), Array.Empty(), false, diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md index 71b7afe3080..0c0ce9809f8 100644 --- a/docs/DafnyRef/UserGuide.md +++ b/docs/DafnyRef/UserGuide.md @@ -573,7 +573,7 @@ Most output from `dafny` is directed to the standard output of the shell invokin ### 13.5.5. Project files -Commands on the Dafny CLI that can be passed a Dafny file, can also be passed a Dafny project file. Such a project file may define which Dafny files the project contains, and which Dafny options it uses. The project file must be a [TOML](https://toml.io/en/) file, ending in the extension `.toml`. Here's an example of a Dafny project file: +Commands on the Dafny CLI that can be passed a Dafny file, can also be passed a Dafny project file. Such a project file may define which Dafny files the project contains, and which Dafny options it uses. The project file must be a [TOML](https://toml.io/en/) file named `dafny.toml`. Here's an example of a Dafny project file: ```toml includes = ["src/**/*.dfy"] From 71acc75170db8a884d35e095cb4f3020abc29474 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 6 Apr 2023 17:00:38 +0200 Subject: [PATCH 07/34] Fix test --- Source/DafnyCore/Options/ProjectFile.cs | 2 +- Test/cli/projectFile/{brokenDafny.toml => broken/dafny.toml} | 0 Test/cli/projectFile/projectFile.dfy | 4 ++-- Test/cli/projectFile/projectFile.dfy.expect | 4 ++-- 4 files changed, 5 insertions(+), 5 deletions(-) rename Test/cli/projectFile/{brokenDafny.toml => broken/dafny.toml} (100%) diff --git a/Source/DafnyCore/Options/ProjectFile.cs b/Source/DafnyCore/Options/ProjectFile.cs index c448a202448..f29aaf86ae1 100644 --- a/Source/DafnyCore/Options/ProjectFile.cs +++ b/Source/DafnyCore/Options/ProjectFile.cs @@ -29,7 +29,7 @@ public static ProjectFile Open(Uri uri, TextWriter errorWriter) { model.Uri = uri; return model; - } catch (FileNotFoundException e) { + } catch (IOException e) { errorWriter.WriteLine(e.Message); return null; } catch (TomlException tomlException) { diff --git a/Test/cli/projectFile/brokenDafny.toml b/Test/cli/projectFile/broken/dafny.toml similarity index 100% rename from Test/cli/projectFile/brokenDafny.toml rename to Test/cli/projectFile/broken/dafny.toml diff --git a/Test/cli/projectFile/projectFile.dfy b/Test/cli/projectFile/projectFile.dfy index eeaf759b8d4..3e50d30e79d 100644 --- a/Test/cli/projectFile/projectFile.dfy +++ b/Test/cli/projectFile/projectFile.dfy @@ -1,4 +1,4 @@ // RUN: %baredafny resolve "%S/dafny.toml" > "%t" -// RUN: ! %baredafny resolve "%S/brokenDafny.toml" 2>> "%t" -// RUN: ! %baredafny resolve "%S/doesNotExist.toml" 2>> "%t" +// RUN: ! %baredafny resolve "%S/broken/dafny.toml" 2>> "%t" +// RUN: ! %baredafny resolve "%S/doesNotExist/dafny.toml" 2>> "%t" // RUN: %diff "%s.expect" "%t" \ No newline at end of file diff --git a/Test/cli/projectFile/projectFile.dfy.expect b/Test/cli/projectFile/projectFile.dfy.expect index 02a1179434a..e9ca9d5d524 100644 --- a/Test/cli/projectFile/projectFile.dfy.expect +++ b/Test/cli/projectFile/projectFile.dfy.expect @@ -1,7 +1,7 @@ /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/src/input.dfy(6,8): Warning: Shadowed local-variable name: x Dafny program verifier did not attempt verification -The Dafny project file /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/brokenDafny.toml contains the following errors: +The Dafny project file /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/broken/dafny.toml contains the following errors: (1,1): the property includdddes does not exist. -Could not find file '/Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/doesNotExist.toml'. +Could not find a part of the path '/Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/doesNotExist/dafny.toml'. From 5e4b69485b868141bea305f29f7d23e7df540f77 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 6 Apr 2023 17:02:47 +0200 Subject: [PATCH 08/34] Run formatter --- Source/DafnyCore/Options/ProjectFile.cs | 14 ++++++-------- Source/DafnyDriver/Commands/CommandRegistry.cs | 5 ++--- .../ProjectFiles/ProjectFiles.cs | 2 +- Source/DafnyLanguageServer/ServerCommand.cs | 3 +-- .../Workspace/DocumentManager.cs | 6 +++--- 5 files changed, 13 insertions(+), 17 deletions(-) diff --git a/Source/DafnyCore/Options/ProjectFile.cs b/Source/DafnyCore/Options/ProjectFile.cs index f29aaf86ae1..ab679d4cfd1 100644 --- a/Source/DafnyCore/Options/ProjectFile.cs +++ b/Source/DafnyCore/Options/ProjectFile.cs @@ -18,10 +18,10 @@ namespace Microsoft.Dafny; public class ProjectFile { [IgnoreDataMember] public Uri Uri { get; set; } - public string[] Includes { get; set; } - public string[] Excludes { get; set; } - public Dictionary Options { get; set; } - + public string[] Includes { get; set; } + public string[] Excludes { get; set; } + public Dictionary Options { get; set; } + public static ProjectFile Open(Uri uri, TextWriter errorWriter) { try { var file = File.Open(uri.LocalPath, FileMode.Open); @@ -46,8 +46,7 @@ public static ProjectFile Open(Uri uri, TextWriter errorWriter) { public void ApplyToOptions(DafnyOptions options) { var matcher = new Matcher(); - foreach (var includeGlob in Includes) - { + foreach (var includeGlob in Includes) { matcher.AddInclude(includeGlob); } foreach (var includeGlob in Excludes) { @@ -57,8 +56,7 @@ public void ApplyToOptions(DafnyOptions options) { var root = Path.GetDirectoryName(Uri.LocalPath); var result = matcher.Execute(new DirectoryInfoWrapper(new DirectoryInfo(root!))); var files = result.Files.Select(f => Path.Combine(root, f.Path)); - foreach (var file in files) - { + foreach (var file in files) { options.AddFile(file); } } diff --git a/Source/DafnyDriver/Commands/CommandRegistry.cs b/Source/DafnyDriver/Commands/CommandRegistry.cs index 3f3a62076b4..3b419060c05 100644 --- a/Source/DafnyDriver/Commands/CommandRegistry.cs +++ b/Source/DafnyDriver/Commands/CommandRegistry.cs @@ -154,7 +154,7 @@ void CommandHandler(InvocationContext context) { if (failedToProcessFile) { return new ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult.PREPROCESSING_ERROR); } - + if (!wasInvoked) { if (exitCode == 0) { return new ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult.OK_EXIT_EARLY); @@ -169,8 +169,7 @@ void CommandHandler(InvocationContext context) { return new ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult.PREPROCESSING_ERROR); } - private static bool ProcessFile(Command command, DafnyOptions dafnyOptions, FileInfo singleFile) - { + private static bool ProcessFile(Command command, DafnyOptions dafnyOptions, FileInfo singleFile) { if (Path.GetExtension(singleFile.FullName) == ".toml") { var projectFile = ProjectFile.Open(new Uri(singleFile.FullName), Console.Error); if (projectFile == null) { diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFiles.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFiles.cs index 614f1473f58..1c177a8f9e3 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFiles.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFiles.cs @@ -14,7 +14,7 @@ public async Task ProjectFileIsFound() { var documentItem = CreateTestDocument(source, filePath); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken); - + Assert.Single(diagnostics); Assert.Equal("Shadowed local-variable name: x", diagnostics[0].Message); } diff --git a/Source/DafnyLanguageServer/ServerCommand.cs b/Source/DafnyLanguageServer/ServerCommand.cs index 52ac741f45d..9a347965d63 100644 --- a/Source/DafnyLanguageServer/ServerCommand.cs +++ b/Source/DafnyLanguageServer/ServerCommand.cs @@ -10,8 +10,7 @@ namespace Microsoft.Dafny.LanguageServer; public class ServerCommand : ICommandSpec { public static readonly ServerCommand Instance = new(); - private ServerCommand() - { + private ServerCommand() { } static ServerCommand() { diff --git a/Source/DafnyLanguageServer/Workspace/DocumentManager.cs b/Source/DafnyLanguageServer/Workspace/DocumentManager.cs index 9ca82335d17..d3c1e73fce6 100644 --- a/Source/DafnyLanguageServer/Workspace/DocumentManager.cs +++ b/Source/DafnyLanguageServer/Workspace/DocumentManager.cs @@ -55,7 +55,7 @@ public DocumentManager( services.GetRequiredService(), document); Compilation = new Compilation( - services, + services, DetermineDocumentOptions(options, document.Uri), document, null); @@ -135,7 +135,7 @@ public void UpdateDocument(DidChangeTextDocumentParams documentChange) { private static DafnyOptions DetermineDocumentOptions(DafnyOptions serverOptions, DocumentUri uri) { ProjectFile? projectFile = null; - + var folder = Path.GetDirectoryName(uri.Path); while (folder != null) { var children = Directory.GetFiles(folder, "dafny.toml"); @@ -151,7 +151,7 @@ private static DafnyOptions DetermineDocumentOptions(DafnyOptions serverOptions, if (projectFile != null) { var result = new DafnyOptions(serverOptions); - + foreach (var option in ServerCommand.Instance.Options) { object? projectFileValue = null; var hasProjectFileValue = projectFile?.TryGetValue(option, out projectFileValue) ?? false; From d89e4c2043c56e801eec843f6d6ea36261259269 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 6 Apr 2023 17:02:52 +0200 Subject: [PATCH 09/34] Update documentation --- docs/DafnyRef/UserGuide.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md index 0c0ce9809f8..337d97bee12 100644 --- a/docs/DafnyRef/UserGuide.md +++ b/docs/DafnyRef/UserGuide.md @@ -586,6 +586,8 @@ excludes = ["**/ignore.dfy"] Options are applied to a command if they can be. Invalid options are ignored. +When using a Dafny IDE based on the `dafny server` command, the IDE will search for project files by traversing up the file tree, and options from the first found project file will override options passed to `dafny server`. + ## 13.6. Verification {#sec-verification} In this section, we suggest a methodology to figure out [why a single assertion might not hold](#sec-verification-debugging), we propose techniques to deal with [assertions that slow a proof down](#sec-verification-debugging-slow), we explain how to [verify assertions in parallel or in a focused way](#sec-assertion-batches), and we also give some more examples of [useful options and attributes to control verification](#sec-command-line-options-and-attributes-for-verification). From 642849a89c4df8cb7f0bf15b4dddc4e1e5fd4145 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 6 Apr 2023 17:05:24 +0200 Subject: [PATCH 10/34] Add multiple project files check --- Source/DafnyDriver/Commands/CommandRegistry.cs | 11 +++++++---- Test/cli/projectFile/projectFile.dfy | 1 + Test/cli/projectFile/projectFile.dfy.expect | 1 + 3 files changed, 9 insertions(+), 4 deletions(-) diff --git a/Source/DafnyDriver/Commands/CommandRegistry.cs b/Source/DafnyDriver/Commands/CommandRegistry.cs index 3b419060c05..4bd849f081e 100644 --- a/Source/DafnyDriver/Commands/CommandRegistry.cs +++ b/Source/DafnyDriver/Commands/CommandRegistry.cs @@ -12,7 +12,6 @@ using Microsoft.Boogie; using Microsoft.Dafny.LanguageServer; using OmniSharp.Extensions.LanguageServer.Protocol.Models; -using Command = System.CommandLine.Command; namespace Microsoft.Dafny; @@ -114,7 +113,7 @@ void CommandHandler(InvocationContext context) { var singleFile = context.ParseResult.GetValueForArgument(FileArgument); if (singleFile != null) { - if (!ProcessFile(command, dafnyOptions, singleFile)) { + if (!ProcessFile(dafnyOptions, singleFile)) { failedToProcessFile = true; return; } @@ -122,7 +121,7 @@ void CommandHandler(InvocationContext context) { var files = context.ParseResult.GetValueForArgument(ICommandSpec.FilesArgument); if (files != null) { foreach (var file in files) { - if (!ProcessFile(command, dafnyOptions, file)) { + if (!ProcessFile(dafnyOptions, file)) { failedToProcessFile = true; return; } @@ -169,8 +168,12 @@ void CommandHandler(InvocationContext context) { return new ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult.PREPROCESSING_ERROR); } - private static bool ProcessFile(Command command, DafnyOptions dafnyOptions, FileInfo singleFile) { + private static bool ProcessFile(DafnyOptions dafnyOptions, FileInfo singleFile) { if (Path.GetExtension(singleFile.FullName) == ".toml") { + if (dafnyOptions.ProjectFile != null) { + Console.Error.WriteLine($"Only one project file can be used at a time. Both {dafnyOptions.ProjectFile.Uri.LocalPath} and {singleFile.FullName} were specified"); + return false; + } var projectFile = ProjectFile.Open(new Uri(singleFile.FullName), Console.Error); if (projectFile == null) { return false; diff --git a/Test/cli/projectFile/projectFile.dfy b/Test/cli/projectFile/projectFile.dfy index 3e50d30e79d..a33b843e454 100644 --- a/Test/cli/projectFile/projectFile.dfy +++ b/Test/cli/projectFile/projectFile.dfy @@ -1,4 +1,5 @@ // RUN: %baredafny resolve "%S/dafny.toml" > "%t" +// RUN: ! %baredafny resolve "%S/dafny.toml" "%S/broken/dafny.toml" 2>> "%t" // RUN: ! %baredafny resolve "%S/broken/dafny.toml" 2>> "%t" // RUN: ! %baredafny resolve "%S/doesNotExist/dafny.toml" 2>> "%t" // RUN: %diff "%s.expect" "%t" \ No newline at end of file diff --git a/Test/cli/projectFile/projectFile.dfy.expect b/Test/cli/projectFile/projectFile.dfy.expect index e9ca9d5d524..0f878b78cb9 100644 --- a/Test/cli/projectFile/projectFile.dfy.expect +++ b/Test/cli/projectFile/projectFile.dfy.expect @@ -1,6 +1,7 @@ /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/src/input.dfy(6,8): Warning: Shadowed local-variable name: x Dafny program verifier did not attempt verification +Only one project file can be used at a time. Both /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/dafny.toml and /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/broken/dafny.toml were specified The Dafny project file /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/broken/dafny.toml contains the following errors: (1,1): the property includdddes does not exist. From 38a0ad35830c0427b63e39d77ded0e0ee00cce80 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 6 Apr 2023 17:06:49 +0200 Subject: [PATCH 11/34] Test for option override behavior --- .../ProjectFiles/{ProjectFiles.cs => ProjectFilesTest.cs} | 2 +- Test/cli/projectFile/projectFile.dfy | 1 + Test/cli/projectFile/projectFile.dfy.expect | 3 +++ 3 files changed, 5 insertions(+), 1 deletion(-) rename Source/DafnyLanguageServer.Test/ProjectFiles/{ProjectFiles.cs => ProjectFilesTest.cs} (92%) diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFiles.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs similarity index 92% rename from Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFiles.cs rename to Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs index 1c177a8f9e3..6a040e610ac 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFiles.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs @@ -6,7 +6,7 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest; -public class ProjectFiles : ClientBasedLanguageServerTest { +public class ProjectFilesTest : ClientBasedLanguageServerTest { [Fact] public async Task ProjectFileIsFound() { var filePath = Path.Combine(Directory.GetCurrentDirectory(), "ProjectFiles/TestFiles/src/foo.dfy"); diff --git a/Test/cli/projectFile/projectFile.dfy b/Test/cli/projectFile/projectFile.dfy index a33b843e454..53c8934f2e9 100644 --- a/Test/cli/projectFile/projectFile.dfy +++ b/Test/cli/projectFile/projectFile.dfy @@ -1,4 +1,5 @@ // RUN: %baredafny resolve "%S/dafny.toml" > "%t" +// RUN: %baredafny resolve "%S/dafny.toml" --warn-shadowing=false >> "%t" // RUN: ! %baredafny resolve "%S/dafny.toml" "%S/broken/dafny.toml" 2>> "%t" // RUN: ! %baredafny resolve "%S/broken/dafny.toml" 2>> "%t" // RUN: ! %baredafny resolve "%S/doesNotExist/dafny.toml" 2>> "%t" diff --git a/Test/cli/projectFile/projectFile.dfy.expect b/Test/cli/projectFile/projectFile.dfy.expect index 0f878b78cb9..281ef9810ba 100644 --- a/Test/cli/projectFile/projectFile.dfy.expect +++ b/Test/cli/projectFile/projectFile.dfy.expect @@ -1,6 +1,9 @@ /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/src/input.dfy(6,8): Warning: Shadowed local-variable name: x Dafny program verifier did not attempt verification + +Dafny program verifier did not attempt verification + Only one project file can be used at a time. Both /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/dafny.toml and /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/broken/dafny.toml were specified The Dafny project file /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/broken/dafny.toml contains the following errors: (1,1): the property includdddes does not exist. From ad354ef9e758f59eb78518eb18edabbaa9dcf3ab Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 6 Apr 2023 17:08:13 +0200 Subject: [PATCH 12/34] Add test documentation --- Test/cli/projectFile/projectFile.dfy | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Test/cli/projectFile/projectFile.dfy b/Test/cli/projectFile/projectFile.dfy index 53c8934f2e9..bf1ae91c31e 100644 --- a/Test/cli/projectFile/projectFile.dfy +++ b/Test/cli/projectFile/projectFile.dfy @@ -1,6 +1,15 @@ +// A project file can specify input files and configure options // RUN: %baredafny resolve "%S/dafny.toml" > "%t" + +// Test option override behavior // RUN: %baredafny resolve "%S/dafny.toml" --warn-shadowing=false >> "%t" + +// Multiple project files are not allowed // RUN: ! %baredafny resolve "%S/dafny.toml" "%S/broken/dafny.toml" 2>> "%t" + +// Project files may not contain unknown properties // RUN: ! %baredafny resolve "%S/broken/dafny.toml" 2>> "%t" + +// Project files must be files on disk. // RUN: ! %baredafny resolve "%S/doesNotExist/dafny.toml" 2>> "%t" // RUN: %diff "%s.expect" "%t" \ No newline at end of file From cdf036909545da499646af6a3dc1889353182a14 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 6 Apr 2023 17:41:58 +0200 Subject: [PATCH 13/34] Added dafny server test, release notes, and removed TODO --- Source/DafnyDriver/Commands/CommandRegistry.cs | 1 - .../DafnyLanguageServer.Test.csproj | 9 +++++++++ .../ProjectFiles/ProjectFilesTest.cs | 16 ++++++++++++++-- .../ProjectFiles/TestFiles/Nesting/dafny.toml | 4 ++++ .../TestFiles/{ => Nesting}/src/foo.dfy | 0 .../ProjectFiles/TestFiles/dafny.toml | 4 ++-- .../ProjectFiles/TestFiles/noWarnShadowing.dfy | 6 ++++++ docs/dev/news/2907.feat | 3 +++ 8 files changed, 38 insertions(+), 5 deletions(-) create mode 100644 Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/Nesting/dafny.toml rename Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/{ => Nesting}/src/foo.dfy (100%) create mode 100644 Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/noWarnShadowing.dfy create mode 100644 docs/dev/news/2907.feat diff --git a/Source/DafnyDriver/Commands/CommandRegistry.cs b/Source/DafnyDriver/Commands/CommandRegistry.cs index 4bd849f081e..0176cb00eac 100644 --- a/Source/DafnyDriver/Commands/CommandRegistry.cs +++ b/Source/DafnyDriver/Commands/CommandRegistry.cs @@ -178,7 +178,6 @@ private static bool ProcessFile(DafnyOptions dafnyOptions, FileInfo singleFile) if (projectFile == null) { return false; } - // TODO check for existing dafnyOptions.ProjectFile = projectFile; projectFile.ApplyToOptions(dafnyOptions); } else { diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj index 28a027cd33c..a34b7aa8765 100644 --- a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj +++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj @@ -71,9 +71,18 @@ Always + + Always + Always + + Always + + + Always + diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs index 6a040e610ac..d56b8ed55ba 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs @@ -8,8 +8,8 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest; public class ProjectFilesTest : ClientBasedLanguageServerTest { [Fact] - public async Task ProjectFileIsFound() { - var filePath = Path.Combine(Directory.GetCurrentDirectory(), "ProjectFiles/TestFiles/src/foo.dfy"); + public async Task ClosestProjectFileIsFound() { + var filePath = Path.Combine(Directory.GetCurrentDirectory(), "ProjectFiles/TestFiles/Nesting/src/foo.dfy"); var source = await File.ReadAllTextAsync(filePath); var documentItem = CreateTestDocument(source, filePath); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); @@ -18,4 +18,16 @@ public async Task ProjectFileIsFound() { Assert.Single(diagnostics); Assert.Equal("Shadowed local-variable name: x", diagnostics[0].Message); } + + [Fact] + public async Task ProjectFileOverridesOptions() { + await SetUp(options => options.WarnShadowing = true); + var filePath = Path.Combine(Directory.GetCurrentDirectory(), "ProjectFiles/TestFiles/noWarnShadowing.dfy"); + var source = await File.ReadAllTextAsync(filePath); + var documentItem = CreateTestDocument(source, filePath); + await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken); + + Assert.Empty(diagnostics); + } } \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/Nesting/dafny.toml b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/Nesting/dafny.toml new file mode 100644 index 00000000000..a450e981c8b --- /dev/null +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/Nesting/dafny.toml @@ -0,0 +1,4 @@ +includes = ["src/**/*.dfy"] + +[options] +warn-shadowing = true diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/src/foo.dfy b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/Nesting/src/foo.dfy similarity index 100% rename from Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/src/foo.dfy rename to Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/Nesting/src/foo.dfy diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/dafny.toml b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/dafny.toml index a450e981c8b..59f848c998a 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/dafny.toml +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/dafny.toml @@ -1,4 +1,4 @@ -includes = ["src/**/*.dfy"] +includes = ["**/*.dfy"] [options] -warn-shadowing = true +warn-shadowing = false diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/noWarnShadowing.dfy b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/noWarnShadowing.dfy new file mode 100644 index 00000000000..49a3a161baa --- /dev/null +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/noWarnShadowing.dfy @@ -0,0 +1,6 @@ +method Foo() { + var x := 3; + if (true) { + var x := 4; + } +} \ No newline at end of file diff --git a/docs/dev/news/2907.feat b/docs/dev/news/2907.feat new file mode 100644 index 00000000000..a04c647d689 --- /dev/null +++ b/docs/dev/news/2907.feat @@ -0,0 +1,3 @@ +Added support for Dafny project files. For now the project file only allows specifying which Dafny files to include and exclude, and what options to use. +The CLI commands that take Dafny files as input, such as build, run, translate, will also accept Dafny project files. +When using an IDE based on `dafny server`, such as the Dafny VSCode extension, the IDE will look for Dafny project files by traversing up the file tree from the currently opened file. The first found project file will override options specified in the IDE. \ No newline at end of file From ad7b23fa5f755c61284e2312afbb837d53b74d5c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 6 Apr 2023 17:48:40 +0200 Subject: [PATCH 14/34] Fix tests --- Test/cli/projectFile/projectFile.dfy | 10 +++++----- Test/cli/projectFile/projectFile.dfy.expect | 4 +--- 2 files changed, 6 insertions(+), 8 deletions(-) diff --git a/Test/cli/projectFile/projectFile.dfy b/Test/cli/projectFile/projectFile.dfy index bf1ae91c31e..08d26512420 100644 --- a/Test/cli/projectFile/projectFile.dfy +++ b/Test/cli/projectFile/projectFile.dfy @@ -1,15 +1,15 @@ // A project file can specify input files and configure options -// RUN: %baredafny resolve "%S/dafny.toml" > "%t" +// RUN: %baredafny resolve --use-basename-for-filename "%S/dafny.toml" > "%t" // Test option override behavior -// RUN: %baredafny resolve "%S/dafny.toml" --warn-shadowing=false >> "%t" +// RUN: %baredafny resolve --use-basename-for-filename "%S/dafny.toml" --warn-shadowing=false >> "%t" // Multiple project files are not allowed -// RUN: ! %baredafny resolve "%S/dafny.toml" "%S/broken/dafny.toml" 2>> "%t" +// RUN: ! %baredafny resolve --use-basename-for-filename "%S/dafny.toml" "%S/broken/dafny.toml" // Project files may not contain unknown properties -// RUN: ! %baredafny resolve "%S/broken/dafny.toml" 2>> "%t" +// RUN: ! %baredafny resolve --use-basename-for-filename "%S/broken/dafny.toml" 2>> "%t" // Project files must be files on disk. -// RUN: ! %baredafny resolve "%S/doesNotExist/dafny.toml" 2>> "%t" +// RUN: ! %baredafny resolve --use-basename-for-filename "%S/doesNotExist/dafny.toml" 2>> "%t" // RUN: %diff "%s.expect" "%t" \ No newline at end of file diff --git a/Test/cli/projectFile/projectFile.dfy.expect b/Test/cli/projectFile/projectFile.dfy.expect index 281ef9810ba..dc2b1bf542c 100644 --- a/Test/cli/projectFile/projectFile.dfy.expect +++ b/Test/cli/projectFile/projectFile.dfy.expect @@ -1,10 +1,8 @@ -/Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/src/input.dfy(6,8): Warning: Shadowed local-variable name: x +input.dfy(6,8): Warning: Shadowed local-variable name: x Dafny program verifier did not attempt verification Dafny program verifier did not attempt verification - -Only one project file can be used at a time. Both /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/dafny.toml and /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/broken/dafny.toml were specified The Dafny project file /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/broken/dafny.toml contains the following errors: (1,1): the property includdddes does not exist. From 260fbbf7e6ddaca6ef423ba932208de4ac6dce6e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 6 Apr 2023 17:50:59 +0200 Subject: [PATCH 15/34] Fix crash --- Source/DafnyLanguageServer/Workspace/DocumentManager.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyLanguageServer/Workspace/DocumentManager.cs b/Source/DafnyLanguageServer/Workspace/DocumentManager.cs index d3c1e73fce6..19b3d562d72 100644 --- a/Source/DafnyLanguageServer/Workspace/DocumentManager.cs +++ b/Source/DafnyLanguageServer/Workspace/DocumentManager.cs @@ -137,7 +137,7 @@ private static DafnyOptions DetermineDocumentOptions(DafnyOptions serverOptions, ProjectFile? projectFile = null; var folder = Path.GetDirectoryName(uri.Path); - while (folder != null) { + while (!string.IsNullOrEmpty(folder)) { var children = Directory.GetFiles(folder, "dafny.toml"); if (children.Length > 0) { var errorWriter = TextWriter.Null; From eb52f49fbd8d7e82810b16d5534a65215ea50266 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 6 Apr 2023 17:51:14 +0200 Subject: [PATCH 16/34] Run formatter --- .../DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs index d56b8ed55ba..984a601c35b 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs @@ -18,7 +18,7 @@ public async Task ClosestProjectFileIsFound() { Assert.Single(diagnostics); Assert.Equal("Shadowed local-variable name: x", diagnostics[0].Message); } - + [Fact] public async Task ProjectFileOverridesOptions() { await SetUp(options => options.WarnShadowing = true); From d8a96dd01771c42ed14de871fb71ff48b601c811 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 6 Apr 2023 18:05:50 +0200 Subject: [PATCH 17/34] Add check against bad types --- Source/DafnyCore/Options/ProjectFile.cs | 16 ++++++++++++---- Source/DafnyDriver/Commands/CommandRegistry.cs | 2 +- .../Workspace/DocumentManager.cs | 2 +- Test/cli/projectFile/badTypes/dafny.toml | 4 ++++ Test/cli/projectFile/projectFile.dfy | 4 ++++ Test/cli/projectFile/projectFile.dfy.expect | 1 + 6 files changed, 23 insertions(+), 6 deletions(-) create mode 100644 Test/cli/projectFile/badTypes/dafny.toml diff --git a/Source/DafnyCore/Options/ProjectFile.cs b/Source/DafnyCore/Options/ProjectFile.cs index ab679d4cfd1..2cb55b37a78 100644 --- a/Source/DafnyCore/Options/ProjectFile.cs +++ b/Source/DafnyCore/Options/ProjectFile.cs @@ -46,10 +46,10 @@ public static ProjectFile Open(Uri uri, TextWriter errorWriter) { public void ApplyToOptions(DafnyOptions options) { var matcher = new Matcher(); - foreach (var includeGlob in Includes) { + foreach (var includeGlob in Includes ?? Enumerable.Empty()) { matcher.AddInclude(includeGlob); } - foreach (var includeGlob in Excludes) { + foreach (var includeGlob in Excludes ?? Enumerable.Empty()) { matcher.AddExclude(includeGlob); } @@ -61,9 +61,17 @@ public void ApplyToOptions(DafnyOptions options) { } } - public bool TryGetValue(Option option, out object value) { + public bool TryGetValue(Option option, TextWriter errorWriter, out object value) { var name = option.Name.StartsWith("--") ? option.Name.Substring(2) : option.Name; - return Options.TryGetValue(name, out value); + if (Options.TryGetValue(name, out value)) { + if (value.GetType() != option.ValueType) { + errorWriter.WriteLine($"Error: property '{name}' is of type '{value.GetType().Name}' but should be of type '{option.ValueType.Name}'"); + return false; + } + return true; + } + + return false; } } \ No newline at end of file diff --git a/Source/DafnyDriver/Commands/CommandRegistry.cs b/Source/DafnyDriver/Commands/CommandRegistry.cs index 0176cb00eac..90da0edc937 100644 --- a/Source/DafnyDriver/Commands/CommandRegistry.cs +++ b/Source/DafnyDriver/Commands/CommandRegistry.cs @@ -131,7 +131,7 @@ void CommandHandler(InvocationContext context) { foreach (var option in command.Options) { var result = context.ParseResult.FindResultFor(option); object projectFileValue = null; - var hasProjectFileValue = dafnyOptions.ProjectFile?.TryGetValue(option, out projectFileValue) ?? false; + var hasProjectFileValue = dafnyOptions.ProjectFile?.TryGetValue(option, Console.Error, out projectFileValue) ?? false; var value = result == null && hasProjectFileValue ? projectFileValue : context.ParseResult.GetValueForOption(option); diff --git a/Source/DafnyLanguageServer/Workspace/DocumentManager.cs b/Source/DafnyLanguageServer/Workspace/DocumentManager.cs index 19b3d562d72..882b4454813 100644 --- a/Source/DafnyLanguageServer/Workspace/DocumentManager.cs +++ b/Source/DafnyLanguageServer/Workspace/DocumentManager.cs @@ -154,7 +154,7 @@ private static DafnyOptions DetermineDocumentOptions(DafnyOptions serverOptions, foreach (var option in ServerCommand.Instance.Options) { object? projectFileValue = null; - var hasProjectFileValue = projectFile?.TryGetValue(option, out projectFileValue) ?? false; + var hasProjectFileValue = projectFile?.TryGetValue(option, TextWriter.Null, out projectFileValue) ?? false; if (hasProjectFileValue) { result.Options.OptionArguments[option] = projectFileValue; result.ApplyBinding(option); diff --git a/Test/cli/projectFile/badTypes/dafny.toml b/Test/cli/projectFile/badTypes/dafny.toml new file mode 100644 index 00000000000..fd3420857b7 --- /dev/null +++ b/Test/cli/projectFile/badTypes/dafny.toml @@ -0,0 +1,4 @@ +includes = ["../src/**/*"] + +[options] +warn-shadowing = 3 \ No newline at end of file diff --git a/Test/cli/projectFile/projectFile.dfy b/Test/cli/projectFile/projectFile.dfy index 08d26512420..44c0d76ce40 100644 --- a/Test/cli/projectFile/projectFile.dfy +++ b/Test/cli/projectFile/projectFile.dfy @@ -12,4 +12,8 @@ // Project files must be files on disk. // RUN: ! %baredafny resolve --use-basename-for-filename "%S/doesNotExist/dafny.toml" 2>> "%t" + +// Project file options must have the right type +// RUN: ! %baredafny resolve --use-basename-for-filename "%S/badTypes/dafny.toml" 2>> "%t" + // RUN: %diff "%s.expect" "%t" \ No newline at end of file diff --git a/Test/cli/projectFile/projectFile.dfy.expect b/Test/cli/projectFile/projectFile.dfy.expect index dc2b1bf542c..9edd55be7e0 100644 --- a/Test/cli/projectFile/projectFile.dfy.expect +++ b/Test/cli/projectFile/projectFile.dfy.expect @@ -7,3 +7,4 @@ The Dafny project file /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/br (1,1): the property includdddes does not exist. Could not find a part of the path '/Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/doesNotExist/dafny.toml'. +Error: property 'warn-shadowing' is of type 'Int64' but should be of type 'Boolean' From 71a72b9fe0b8d57a2303c361c436384ce8f62dc9 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 7 Apr 2023 10:46:48 +0200 Subject: [PATCH 18/34] Code review --- Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs | 3 --- docs/DafnyRef/UserGuide.md | 4 ++-- 2 files changed, 2 insertions(+), 5 deletions(-) diff --git a/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs index 268069c040d..e7cb0536492 100644 --- a/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs +++ b/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs @@ -26,9 +26,6 @@ public interface ITextDocumentLoader { /// Loads the specified document item of the language server and applies the necessary steps /// to generate a dafny document instance. /// - /// - /// The text document to load. - /// A token to cancel the update operation before its completion. /// The loaded dafny document. /// Thrown when the cancellation was requested before completion. /// Thrown if the cancellation token was disposed before the completion. diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md index 337d97bee12..c9319e72b3d 100644 --- a/docs/DafnyRef/UserGuide.md +++ b/docs/DafnyRef/UserGuide.md @@ -580,8 +580,8 @@ includes = ["src/**/*.dfy"] excludes = ["**/ignore.dfy"] [options] - enforce-determinism = true - warn-shadowing = true +enforce-determinism = true +warn-shadowing = true ``` Options are applied to a command if they can be. Invalid options are ignored. From b06d4b561904f462e091674c08fb84dd48626ae0 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 7 Apr 2023 10:54:16 +0200 Subject: [PATCH 19/34] Add a default includes pattern --- Source/DafnyCore/Options/ProjectFile.cs | 2 +- Test/cli/projectFile/badTypes/badTypes.dfy | 8 ++++++++ Test/cli/projectFile/badTypes/dafny.toml | 2 +- Test/cli/projectFile/noIncludes/dafny.toml | 2 ++ Test/cli/projectFile/noIncludes/src/input.dfy | 8 ++++++++ .../projectFile/noIncludes/src/moreNested/moreInput.dfy | 8 ++++++++ Test/cli/projectFile/projectFile.dfy | 3 +++ Test/cli/projectFile/projectFile.dfy.expect | 4 ++++ 8 files changed, 35 insertions(+), 2 deletions(-) create mode 100644 Test/cli/projectFile/badTypes/badTypes.dfy create mode 100644 Test/cli/projectFile/noIncludes/dafny.toml create mode 100644 Test/cli/projectFile/noIncludes/src/input.dfy create mode 100644 Test/cli/projectFile/noIncludes/src/moreNested/moreInput.dfy diff --git a/Source/DafnyCore/Options/ProjectFile.cs b/Source/DafnyCore/Options/ProjectFile.cs index 2cb55b37a78..e3b53c8c983 100644 --- a/Source/DafnyCore/Options/ProjectFile.cs +++ b/Source/DafnyCore/Options/ProjectFile.cs @@ -46,7 +46,7 @@ public static ProjectFile Open(Uri uri, TextWriter errorWriter) { public void ApplyToOptions(DafnyOptions options) { var matcher = new Matcher(); - foreach (var includeGlob in Includes ?? Enumerable.Empty()) { + foreach (var includeGlob in Includes ?? new[] { "**/*.dfy" }) { matcher.AddInclude(includeGlob); } foreach (var includeGlob in Excludes ?? Enumerable.Empty()) { diff --git a/Test/cli/projectFile/badTypes/badTypes.dfy b/Test/cli/projectFile/badTypes/badTypes.dfy new file mode 100644 index 00000000000..3aff32ba633 --- /dev/null +++ b/Test/cli/projectFile/badTypes/badTypes.dfy @@ -0,0 +1,8 @@ +// RUN: echo "" + +method Foo() { + var x := 3; + if (true) { + var x := 4; + } +} \ No newline at end of file diff --git a/Test/cli/projectFile/badTypes/dafny.toml b/Test/cli/projectFile/badTypes/dafny.toml index fd3420857b7..e5c8d4481ce 100644 --- a/Test/cli/projectFile/badTypes/dafny.toml +++ b/Test/cli/projectFile/badTypes/dafny.toml @@ -1,4 +1,4 @@ -includes = ["../src/**/*"] +includes = ["**/*"] [options] warn-shadowing = 3 \ No newline at end of file diff --git a/Test/cli/projectFile/noIncludes/dafny.toml b/Test/cli/projectFile/noIncludes/dafny.toml new file mode 100644 index 00000000000..39b81f42b08 --- /dev/null +++ b/Test/cli/projectFile/noIncludes/dafny.toml @@ -0,0 +1,2 @@ +[options] +warn-shadowing = true \ No newline at end of file diff --git a/Test/cli/projectFile/noIncludes/src/input.dfy b/Test/cli/projectFile/noIncludes/src/input.dfy new file mode 100644 index 00000000000..3aff32ba633 --- /dev/null +++ b/Test/cli/projectFile/noIncludes/src/input.dfy @@ -0,0 +1,8 @@ +// RUN: echo "" + +method Foo() { + var x := 3; + if (true) { + var x := 4; + } +} \ No newline at end of file diff --git a/Test/cli/projectFile/noIncludes/src/moreNested/moreInput.dfy b/Test/cli/projectFile/noIncludes/src/moreNested/moreInput.dfy new file mode 100644 index 00000000000..d05a03de449 --- /dev/null +++ b/Test/cli/projectFile/noIncludes/src/moreNested/moreInput.dfy @@ -0,0 +1,8 @@ +// RUN: echo "" + +method Bar() { + var x := 3; + if (true) { + var x := 4; + } +} \ No newline at end of file diff --git a/Test/cli/projectFile/projectFile.dfy b/Test/cli/projectFile/projectFile.dfy index 44c0d76ce40..c0f0e29d56e 100644 --- a/Test/cli/projectFile/projectFile.dfy +++ b/Test/cli/projectFile/projectFile.dfy @@ -16,4 +16,7 @@ // Project file options must have the right type // RUN: ! %baredafny resolve --use-basename-for-filename "%S/badTypes/dafny.toml" 2>> "%t" +// A project file without includes will take all .dfy files as input +// RUN: %baredafny resolve --use-basename-for-filename "%S/noIncludes/dafny.toml" >> "%t" + // RUN: %diff "%s.expect" "%t" \ No newline at end of file diff --git a/Test/cli/projectFile/projectFile.dfy.expect b/Test/cli/projectFile/projectFile.dfy.expect index 9edd55be7e0..e67e06acb04 100644 --- a/Test/cli/projectFile/projectFile.dfy.expect +++ b/Test/cli/projectFile/projectFile.dfy.expect @@ -8,3 +8,7 @@ The Dafny project file /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/br Could not find a part of the path '/Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/doesNotExist/dafny.toml'. Error: property 'warn-shadowing' is of type 'Int64' but should be of type 'Boolean' +input.dfy(6,8): Warning: Shadowed local-variable name: x +moreInput.dfy(6,8): Warning: Shadowed local-variable name: x + +Dafny program verifier did not attempt verification From cbbe7e6af4ea041b45a15d5d130a2bdcd4e50f6a Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 7 Apr 2023 17:57:48 +0200 Subject: [PATCH 20/34] Fix tests --- Test/cli/projectFile/projectFile.dfy | 4 ++-- Test/cli/projectFile/projectFile.dfy.expect | 4 ---- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/Test/cli/projectFile/projectFile.dfy b/Test/cli/projectFile/projectFile.dfy index c0f0e29d56e..ee68578e959 100644 --- a/Test/cli/projectFile/projectFile.dfy +++ b/Test/cli/projectFile/projectFile.dfy @@ -8,10 +8,10 @@ // RUN: ! %baredafny resolve --use-basename-for-filename "%S/dafny.toml" "%S/broken/dafny.toml" // Project files may not contain unknown properties -// RUN: ! %baredafny resolve --use-basename-for-filename "%S/broken/dafny.toml" 2>> "%t" +// RUN: ! %baredafny resolve --use-basename-for-filename "%S/broken/dafny.toml" // Project files must be files on disk. -// RUN: ! %baredafny resolve --use-basename-for-filename "%S/doesNotExist/dafny.toml" 2>> "%t" +// RUN: ! %baredafny resolve --use-basename-for-filename "%S/doesNotExist/dafny.toml" // Project file options must have the right type // RUN: ! %baredafny resolve --use-basename-for-filename "%S/badTypes/dafny.toml" 2>> "%t" diff --git a/Test/cli/projectFile/projectFile.dfy.expect b/Test/cli/projectFile/projectFile.dfy.expect index e67e06acb04..1ec4f2752ab 100644 --- a/Test/cli/projectFile/projectFile.dfy.expect +++ b/Test/cli/projectFile/projectFile.dfy.expect @@ -3,10 +3,6 @@ input.dfy(6,8): Warning: Shadowed local-variable name: x Dafny program verifier did not attempt verification Dafny program verifier did not attempt verification -The Dafny project file /Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/broken/dafny.toml contains the following errors: -(1,1): the property includdddes does not exist. - -Could not find a part of the path '/Users/rwillems/SourceCode/dafny2/Test/cli/projectFile/doesNotExist/dafny.toml'. Error: property 'warn-shadowing' is of type 'Int64' but should be of type 'Boolean' input.dfy(6,8): Warning: Shadowed local-variable name: x moreInput.dfy(6,8): Warning: Shadowed local-variable name: x From 3d759e3237d95e62d25206424ddb7a64461f6ad2 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 7 Apr 2023 18:03:01 +0200 Subject: [PATCH 21/34] Update customBoogie.patch --- customBoogie.patch | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/customBoogie.patch b/customBoogie.patch index a71499bcc71..5bfb4c1f360 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -54,15 +54,15 @@ index 426b132e2..18db4aebb 100644 EndGlobalSection EndGlobal diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj -index 0f17aa923..6b937ebcb 100644 +index 4a8b2f89b..a308be9bf 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj -@@ -30,7 +30,7 @@ +@@ -31,7 +31,7 @@ - + + - From bbfb98f39a9c50ec3ad576f66da2351f1607f8e1 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 10 Apr 2023 12:08:22 +0200 Subject: [PATCH 22/34] Fix test exception and remove some annoying debug log lines --- Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs | 2 +- .../Language/Symbols/DafnyLangSymbolResolver.cs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs index e9641526d04..faa82646d0c 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs @@ -15,7 +15,7 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup { public class HoverTest : ClientBasedLanguageServerTest { protected override async Task SetUp(Action modifyOptions = null) { void ModifyOptions(DafnyOptions options) { - options.ProverOptions.Add("-proverOpt:SOLVER=noop"); + options.ProverOptions.Add("SOLVER=noop"); modifyOptions?.Invoke(options); } diff --git a/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs b/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs index c9ca0677875..a884a5a1f95 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs @@ -99,7 +99,7 @@ private ModuleSymbol ProcessModule(Symbol scope, ModuleDefinition moduleDefiniti case DatatypeDecl dataTypeDeclaration: return ProcessDataType(moduleSymbol, dataTypeDeclaration); default: - logger.LogDebug("encountered unknown top level declaration {Name} of type {Type}", topLevelDeclaration.Name, topLevelDeclaration.GetType()); + logger.LogTrace("encountered unknown top level declaration {Name} of type {Type}", topLevelDeclaration.Name, topLevelDeclaration.GetType()); return null; } } From f0bf21287e217678201938a04b247d0c8d7c5b98 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 10 Apr 2023 12:48:32 +0200 Subject: [PATCH 23/34] Turn off some logging and hopefulyl fix a Windows bug --- .../Language/Symbols/DafnyLangSymbolResolver.cs | 2 +- Source/DafnyLanguageServer/Workspace/Compilation.cs | 4 ++-- Source/DafnyLanguageServer/Workspace/DocumentManager.cs | 2 +- Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs b/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs index a884a5a1f95..8acd9bc90dc 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs @@ -276,7 +276,7 @@ public void Resolve(Expression bodyExpression) { } public override void VisitUnknown(object node, IToken token) { - logger.LogDebug("encountered unknown syntax node of type {NodeType} in {Filename}@({Line},{Column})", + logger.LogTrace("encountered unknown syntax node of type {NodeType} in {Filename}@({Line},{Column})", node.GetType(), token.GetDocumentFileName(), token.line, token.col); } diff --git a/Source/DafnyLanguageServer/Workspace/Compilation.cs b/Source/DafnyLanguageServer/Workspace/Compilation.cs index 8780723af50..356e71b8e4f 100644 --- a/Source/DafnyLanguageServer/Workspace/Compilation.cs +++ b/Source/DafnyLanguageServer/Workspace/Compilation.cs @@ -338,14 +338,14 @@ public void CancelPendingUpdates() { private readonly DafnyOptions options; public void MarkVerificationStarted() { - logger.LogDebug("MarkVerificationStarted called"); + logger.LogTrace("MarkVerificationStarted called"); if (verificationCompleted.Task.IsCompleted) { verificationCompleted = new TaskCompletionSource(); } } public void MarkVerificationFinished() { - logger.LogDebug("MarkVerificationFinished called"); + logger.LogTrace("MarkVerificationFinished called"); verificationCompleted.TrySetResult(); } diff --git a/Source/DafnyLanguageServer/Workspace/DocumentManager.cs b/Source/DafnyLanguageServer/Workspace/DocumentManager.cs index 882b4454813..a556a7f83d0 100644 --- a/Source/DafnyLanguageServer/Workspace/DocumentManager.cs +++ b/Source/DafnyLanguageServer/Workspace/DocumentManager.cs @@ -136,7 +136,7 @@ public void UpdateDocument(DidChangeTextDocumentParams documentChange) { private static DafnyOptions DetermineDocumentOptions(DafnyOptions serverOptions, DocumentUri uri) { ProjectFile? projectFile = null; - var folder = Path.GetDirectoryName(uri.Path); + var folder = Path.GetDirectoryName(uri.GetFileSystemPath()); while (!string.IsNullOrEmpty(folder)) { var children = Directory.GetFiles(folder, "dafny.toml"); if (children.Length > 0) { diff --git a/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs b/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs index 42898c31cbb..3e04f890321 100644 --- a/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs +++ b/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs @@ -56,7 +56,7 @@ public void OnError(Exception exception) { } public void OnNext(IdeState snapshot) { - logger.LogDebug($"IdeStateObserver.OnNext entered, threadId: {Thread.CurrentThread.ManagedThreadId}"); + logger.LogTrace($"IdeStateObserver.OnNext entered, threadId: {Thread.CurrentThread.ManagedThreadId}"); lock (lastPublishedStateLock) { if (snapshot.Version < LastPublishedState.Version) { return; From a78368157792aefd64716edb928195b055955b64 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 11 Apr 2023 12:16:24 +0200 Subject: [PATCH 24/34] Improve documentation --- docs/DafnyRef/UserGuide.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md index c9319e72b3d..f72f6ee3ed6 100644 --- a/docs/DafnyRef/UserGuide.md +++ b/docs/DafnyRef/UserGuide.md @@ -584,10 +584,12 @@ enforce-determinism = true warn-shadowing = true ``` -Options are applied to a command if they can be. Invalid options are ignored. +Under the section `[options]`, any options from the Dafny CLI can be specified using the option's name without the `--` prefix. When executing a `dafny` command using a project file, any options specified in the file that can be applied to the command, will be. Options that can't be applied or are misspelled, are ignored. When using a Dafny IDE based on the `dafny server` command, the IDE will search for project files by traversing up the file tree, and options from the first found project file will override options passed to `dafny server`. +It's not possible to use Dafny project files in combination with the legacy CLI UI. + ## 13.6. Verification {#sec-verification} In this section, we suggest a methodology to figure out [why a single assertion might not hold](#sec-verification-debugging), we propose techniques to deal with [assertions that slow a proof down](#sec-verification-debugging-slow), we explain how to [verify assertions in parallel or in a focused way](#sec-assertion-batches), and we also give some more examples of [useful options and attributes to control verification](#sec-command-line-options-and-attributes-for-verification). From 8fbff1883ed2a464c1282b5f746e3482dae133cc Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 12 Apr 2023 10:43:32 +0200 Subject: [PATCH 25/34] Refactoring --- Source/DafnyCore/Options/ProjectFile.cs | 25 ++++++++++++------- .../DafnyDriver/Commands/CommandRegistry.cs | 2 +- 2 files changed, 17 insertions(+), 10 deletions(-) diff --git a/Source/DafnyCore/Options/ProjectFile.cs b/Source/DafnyCore/Options/ProjectFile.cs index e3b53c8c983..0e3402ba427 100644 --- a/Source/DafnyCore/Options/ProjectFile.cs +++ b/Source/DafnyCore/Options/ProjectFile.cs @@ -44,7 +44,7 @@ public static ProjectFile Open(Uri uri, TextWriter errorWriter) { } } - public void ApplyToOptions(DafnyOptions options) { + public void AddFilesToOptions(DafnyOptions options) { var matcher = new Matcher(); foreach (var includeGlob in Includes ?? new[] { "**/*.dfy" }) { matcher.AddInclude(includeGlob); @@ -62,16 +62,23 @@ public void ApplyToOptions(DafnyOptions options) { } public bool TryGetValue(Option option, TextWriter errorWriter, out object value) { - var name = option.Name.StartsWith("--") ? option.Name.Substring(2) : option.Name; + if (!option.Name.StartsWith("--")) { + value = null; + return false; + } + + var name = option.Name.Substring(2); + if (!Options.TryGetValue(name, out value)) { + return false; + } - if (Options.TryGetValue(name, out value)) { - if (value.GetType() != option.ValueType) { - errorWriter.WriteLine($"Error: property '{name}' is of type '{value.GetType().Name}' but should be of type '{option.ValueType.Name}'"); - return false; - } - return true; + if (value.GetType() != option.ValueType) { + errorWriter.WriteLine( + $"Error: property '{name}' is of type '{value.GetType().Name}' but should be of type '{option.ValueType.Name}'"); + return false; } - return false; + return true; + } } \ No newline at end of file diff --git a/Source/DafnyDriver/Commands/CommandRegistry.cs b/Source/DafnyDriver/Commands/CommandRegistry.cs index 90da0edc937..a1a6f99742d 100644 --- a/Source/DafnyDriver/Commands/CommandRegistry.cs +++ b/Source/DafnyDriver/Commands/CommandRegistry.cs @@ -179,7 +179,7 @@ private static bool ProcessFile(DafnyOptions dafnyOptions, FileInfo singleFile) return false; } dafnyOptions.ProjectFile = projectFile; - projectFile.ApplyToOptions(dafnyOptions); + projectFile.AddFilesToOptions(dafnyOptions); } else { dafnyOptions.AddFile(singleFile.FullName); } From e5acbfc0a86903746a95fba108a965824365b225 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 12 Apr 2023 10:54:56 +0200 Subject: [PATCH 26/34] Fix and test extensions --- Source/DafnyCore/Options/ProjectFile.cs | 10 ++-------- Source/IntegrationTests/LitTests.cs | 2 +- Test/cli/projectFile/projectFile.dfy | 6 ++++++ Test/cli/projectFile/projectFile.dfy.expect | 7 +++++++ 4 files changed, 16 insertions(+), 9 deletions(-) diff --git a/Source/DafnyCore/Options/ProjectFile.cs b/Source/DafnyCore/Options/ProjectFile.cs index 0e3402ba427..66673fe742d 100644 --- a/Source/DafnyCore/Options/ProjectFile.cs +++ b/Source/DafnyCore/Options/ProjectFile.cs @@ -62,19 +62,13 @@ public void AddFilesToOptions(DafnyOptions options) { } public bool TryGetValue(Option option, TextWriter errorWriter, out object value) { - if (!option.Name.StartsWith("--")) { - value = null; - return false; - } - - var name = option.Name.Substring(2); - if (!Options.TryGetValue(name, out value)) { + if (!Options.TryGetValue(option.Name, out value)) { return false; } if (value.GetType() != option.ValueType) { errorWriter.WriteLine( - $"Error: property '{name}' is of type '{value.GetType().Name}' but should be of type '{option.ValueType.Name}'"); + $"Error: property '{option.Name}' is of type '{value.GetType().Name}' but should be of type '{option.ValueType.Name}'"); return false; } diff --git a/Source/IntegrationTests/LitTests.cs b/Source/IntegrationTests/LitTests.cs index 78d13a65a95..6fac9ade8c1 100644 --- a/Source/IntegrationTests/LitTests.cs +++ b/Source/IntegrationTests/LitTests.cs @@ -18,7 +18,7 @@ public class LitTests { // Change this to true in order to debug the execution of commands like %dafny. // This is false by default because the main dafny CLI implementation currently has shared static state, which // causes errors when invoking the CLI in the same process on multiple inputs in sequence, much less in parallel. - private const bool InvokeMainMethodsDirectly = false; + private const bool InvokeMainMethodsDirectly = true; private static readonly Assembly DafnyDriverAssembly = typeof(Dafny.Dafny).Assembly; private static readonly Assembly TestDafnyAssembly = typeof(TestDafny.TestDafny).Assembly; diff --git a/Test/cli/projectFile/projectFile.dfy b/Test/cli/projectFile/projectFile.dfy index ee68578e959..004c75545b1 100644 --- a/Test/cli/projectFile/projectFile.dfy +++ b/Test/cli/projectFile/projectFile.dfy @@ -19,4 +19,10 @@ // A project file without includes will take all .dfy files as input // RUN: %baredafny resolve --use-basename-for-filename "%S/noIncludes/dafny.toml" >> "%t" +// Files included by the project file and on the CLI, duplicate is ignored. +// RUN: %baredafny resolve --use-basename-for-filename "%S/dafny.toml" "%S/src/input.dfy" >> "%t" + +// Files excluded by the project file and included on the CLI, are included +// RUN: ! %baredafny resolve --use-basename-for-filename "%S/dafny.toml" "%S/src/excluded.dfy" >> "%t" + // RUN: %diff "%s.expect" "%t" \ No newline at end of file diff --git a/Test/cli/projectFile/projectFile.dfy.expect b/Test/cli/projectFile/projectFile.dfy.expect index 1ec4f2752ab..efcef6202ad 100644 --- a/Test/cli/projectFile/projectFile.dfy.expect +++ b/Test/cli/projectFile/projectFile.dfy.expect @@ -8,3 +8,10 @@ input.dfy(6,8): Warning: Shadowed local-variable name: x moreInput.dfy(6,8): Warning: Shadowed local-variable name: x Dafny program verifier did not attempt verification +input.dfy(6,8): Warning: Shadowed local-variable name: x + +Dafny program verifier did not attempt verification +excluded.dfy(3,7): Error: Duplicate member name: Foo +input.dfy(6,8): Warning: Shadowed local-variable name: x +excluded.dfy(6,8): Warning: Shadowed local-variable name: z +1 resolution/type errors detected in the_program From 5f588abfc9f193ccddf2e16ef2d270382da4ed73 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 12 Apr 2023 11:47:10 +0200 Subject: [PATCH 27/34] Add validation to check for options in a project file that don't exist --- Source/DafnyCore/Options/ProjectFile.cs | 7 +++++++ Source/DafnyDriver/Commands/CommandRegistry.cs | 8 +++++++- Test/cli/projectFile/broken/invalidOption.toml | 3 +++ Test/cli/projectFile/projectFile.dfy | 3 +++ Test/cli/projectFile/projectFile.dfy.expect | 3 +++ 5 files changed, 23 insertions(+), 1 deletion(-) create mode 100644 Test/cli/projectFile/broken/invalidOption.toml diff --git a/Source/DafnyCore/Options/ProjectFile.cs b/Source/DafnyCore/Options/ProjectFile.cs index 66673fe742d..e4af2bdbbbf 100644 --- a/Source/DafnyCore/Options/ProjectFile.cs +++ b/Source/DafnyCore/Options/ProjectFile.cs @@ -61,6 +61,13 @@ public void AddFilesToOptions(DafnyOptions options) { } } + public void Validate(IEnumerable