From 0beaffbff22e165e2d117ad51d26987c2f177279 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 1 Sep 2023 17:55:23 +0200 Subject: [PATCH 1/9] Support all option types in the project file --- Source/DafnyCore.Test/DafnyProjectTest.cs | 12 ++-- Source/DafnyCore/DooFile.cs | 9 +-- Source/DafnyCore/Generic/TomlUtil.cs | 70 +++++++++++++++++++ Source/DafnyCore/Options/DafnyProject.cs | 56 ++------------- .../ProjectFiles/ProjectFilesTest.cs | 11 ++- 5 files changed, 95 insertions(+), 63 deletions(-) create mode 100644 Source/DafnyCore/Generic/TomlUtil.cs diff --git a/Source/DafnyCore.Test/DafnyProjectTest.cs b/Source/DafnyCore.Test/DafnyProjectTest.cs index 836b21309bc..e5e27233bfe 100644 --- a/Source/DafnyCore.Test/DafnyProjectTest.cs +++ b/Source/DafnyCore.Test/DafnyProjectTest.cs @@ -10,7 +10,7 @@ public class DafnyProjectTest { Uri = new Uri(randomFileName, UriKind.Absolute), Includes = new[] { "a", "a2" }, Excludes = new[] { "b", "b2" }, - Options = new Dictionary() { + Options = new Dictionary() { { "c", "d" }, { "e", "f" } } @@ -20,7 +20,7 @@ public class DafnyProjectTest { Uri = new Uri(randomFileName, UriKind.Absolute), Includes = new[] { "a2", "a" }, Excludes = new[] { "b2", "b" }, - Options = new Dictionary() { + Options = new Dictionary() { { "e", "f" }, { "c", "d" }, } @@ -28,13 +28,13 @@ public class DafnyProjectTest { Assert.Equal(first, second); - first.Options.Add("k", new[] { 1, 2, 3 }); - second.Options.Add("k", new[] { 1, 2, 3 }); + first.Options.Add("k", "1, 2, 3"); + second.Options.Add("k", "1, 2, 3"); Assert.Equal(first, second); - first.Options.Add("m", new[] { 1, 2, 3 }); - second.Options.Add("m", new[] { 3, 2, 1 }); + first.Options.Add("m", "1, 2, 3"); + second.Options.Add("m", "3, 2, 1"); Assert.NotEqual(first, second); } } \ No newline at end of file diff --git a/Source/DafnyCore/DooFile.cs b/Source/DafnyCore/DooFile.cs index 07d5dde5049..2ff6ab92c69 100644 --- a/Source/DafnyCore/DooFile.cs +++ b/Source/DafnyCore/DooFile.cs @@ -1,18 +1,13 @@ using System; using System.Collections.Generic; using System.CommandLine; -using System.CommandLine.Binding; -using System.Configuration; using System.IO; using System.IO.Compression; using System.Linq; using System.Text; -using System.Threading; +using DafnyCore.Generic; using Microsoft.Dafny; -using Microsoft.Dafny.Auditor; using Tomlyn; -using Tomlyn.Model; -using Type = System.Type; namespace DafnyCore; @@ -137,7 +132,7 @@ public class ManifestData { object libraryValue = null; if (Manifest.Options.TryGetValue(option.Name, out var manifestValue)) { - if (!DafnyProject.TryGetValueFromToml(Console.Out, null, + if (!TomlUtil.TryGetValueFromToml(Console.Out, null, option.Name, option.ValueType, manifestValue, out libraryValue)) { return false; } diff --git a/Source/DafnyCore/Generic/TomlUtil.cs b/Source/DafnyCore/Generic/TomlUtil.cs new file mode 100644 index 00000000000..b98d92da3f0 --- /dev/null +++ b/Source/DafnyCore/Generic/TomlUtil.cs @@ -0,0 +1,70 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using Tomlyn.Model; + +namespace DafnyCore.Generic; + +public static class TomlUtil { + + public static bool TryGetValueFromToml(TextWriter errorWriter, string sourceDir, string tomlPath, Type type, object tomlValue, out object value) { + if (tomlValue == null) { + value = null; + return false; + } + + if (type.IsAssignableFrom(typeof(List))) { + return TryGetListValueFromToml(errorWriter, sourceDir, tomlPath, (TomlArray)tomlValue, out value); + } + if (type.IsAssignableFrom(typeof(List))) { + return TryGetListValueFromToml(errorWriter, sourceDir, tomlPath, (TomlArray)tomlValue, out value); + } + + if (tomlValue is string tomlString) { + if (type == typeof(FileInfo)) { + // Need to make sure relative paths are interpreted relative to the source of the value, + // not the current directory. + var fullPath = sourceDir != null ? Path.GetFullPath(tomlString, sourceDir) : tomlString; + value = new FileInfo(fullPath); + return true; + } + + if (typeof(Enum).IsAssignableFrom(type)) { + try { + value = Enum.Parse(type, tomlString); + return true; + } catch (ArgumentException) { + value = null; + return false; + } + } + } + + if (!type.IsInstanceOfType(tomlValue)) { + if (type == typeof(string)) { + value = tomlValue.ToString(); + return true; + } + errorWriter.WriteLine( + $"Error: property '{tomlPath}' is of type '{tomlValue.GetType()}' but should be of type '{type}'"); + value = null; + return false; + } + + value = tomlValue; + return true; + } + + private static bool TryGetListValueFromToml(TextWriter errorWriter, string sourceDir, string tomlPath, TomlArray tomlValue, out object value) { + var success = true; + value = tomlValue.Select((e, i) => { + if (TryGetValueFromToml(errorWriter, sourceDir, $"{tomlPath}[{i}]", typeof(T), e, out var elementValue)) { + return (T)elementValue; + } + success = false; + return default(T); + }).ToList(); + return success; + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Options/DafnyProject.cs b/Source/DafnyCore/Options/DafnyProject.cs index 8576c45e229..90226c83b1c 100644 --- a/Source/DafnyCore/Options/DafnyProject.cs +++ b/Source/DafnyCore/Options/DafnyProject.cs @@ -10,7 +10,6 @@ using DafnyCore.Options; using Microsoft.Extensions.FileSystemGlobbing; using Tomlyn; -using Tomlyn.Model; namespace Microsoft.Dafny; @@ -23,7 +22,7 @@ public class DafnyProject : IEquatable { public Uri Uri { get; set; } public string[] Includes { get; set; } public string[] Excludes { get; set; } - public Dictionary Options { get; set; } + public Dictionary Options { get; set; } public bool UsesProjectFile => Path.GetFileName(Uri.LocalPath) == FileName; public static async Task Open(IFileSystem fileSystem, Uri uri, TextWriter outputWriter, TextWriter errorWriter) { @@ -140,57 +139,16 @@ public class DafnyProject : IEquatable { return false; } - return TryGetValueFromToml(errorWriter, Path.GetDirectoryName(Uri.LocalPath), option.Name, option.ValueType, tomlValue, out value); - } - - public static bool TryGetValueFromToml(TextWriter errorWriter, string sourceDir, string tomlPath, System.Type type, object tomlValue, out object value) { - if (tomlValue == null) { - value = null; - return false; - } - - if (type.IsAssignableFrom(typeof(List))) { - return TryGetListValueFromToml(errorWriter, sourceDir, tomlPath, (TomlArray)tomlValue, out value); - } - if (type.IsAssignableFrom(typeof(List))) { - return TryGetListValueFromToml(errorWriter, sourceDir, tomlPath, (TomlArray)tomlValue, out value); - } - - if (type == typeof(FileInfo) && tomlValue is string tomlString) { - // Need to make sure relative paths are interpreted relative to the source of the value, - // not the current directory. - var fullPath = sourceDir != null ? Path.GetFullPath(tomlString, sourceDir) : tomlString; - value = new FileInfo(fullPath); - return true; - } - - if (!type.IsInstanceOfType(tomlValue)) { - if (type == typeof(string)) { - value = tomlValue.ToString(); - return true; - } - errorWriter.WriteLine( - $"Error: property '{tomlPath}' is of type '{tomlValue.GetType()}' but should be of type '{type}'"); + var parseResult = option.Parse(new[] { option.Aliases.First(), tomlValue }); + if (parseResult.Errors.Any()) { value = null; return false; } - value = tomlValue; + value = parseResult.GetValueForOption(option); return true; } - private static bool TryGetListValueFromToml(TextWriter errorWriter, string sourceDir, string tomlPath, TomlArray tomlValue, out object value) { - var success = true; - value = tomlValue.Select((e, i) => { - if (TryGetValueFromToml(errorWriter, sourceDir, $"{tomlPath}[{i}]", typeof(T), e, out var elementValue)) { - return (T)elementValue; - } - success = false; - return default(T); - }).ToList(); - return success; - } - public bool Equals(DafnyProject other) { if (ReferenceEquals(null, other)) { return false; @@ -200,13 +158,13 @@ public class DafnyProject : IEquatable { return true; } - var orderedOptions = Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty>(); - var otherOrderedOptions = other.Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty>(); + var orderedOptions = Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty>(); + var otherOrderedOptions = other.Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty>(); return Equals(Uri, other.Uri) && NullableSetEqual(Includes?.ToHashSet(), other.Includes) && NullableSetEqual(Excludes?.ToHashSet(), other.Excludes) && - orderedOptions.SequenceEqual(otherOrderedOptions, new LambdaEqualityComparer>( + orderedOptions.SequenceEqual(otherOrderedOptions, new LambdaEqualityComparer>( (kv1, kv2) => kv1.Key == kv2.Key && GenericEquals(kv1.Value, kv2.Value), kv => kv.GetHashCode())); } diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs index 0da11b10df7..27c5de71dd1 100644 --- a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs +++ b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs @@ -1,4 +1,5 @@ using System.IO; +using System.Linq; using System.Threading.Tasks; using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; @@ -67,6 +68,7 @@ public class ProjectFilesTest : ClientBasedLanguageServerTest { public async Task ProjectFileOverridesOptions() { await SetUp(options => { options.Set(Function.FunctionSyntaxOption, "3"); + options.Set(CommonOptionBag.QuantifierSyntax, QuantifierSyntaxOptions.Version3); options.Set(CommonOptionBag.WarnShadowing, true); }); var source = @" @@ -77,6 +79,10 @@ public class ProjectFilesTest : ClientBasedLanguageServerTest { } } +function Zoo(): set<(int,int)> { + set x: int | 0 <= x < 5, y | 0 <= y < 6 :: (x,y) +} + ghost function Bar(): int { 3 }".TrimStart(); var projectFileSource = @" @@ -84,6 +90,7 @@ public class ProjectFilesTest : ClientBasedLanguageServerTest { [options] warn-shadowing = false +quantifier-syntax = 4 function-syntax = 4"; var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName()); @@ -94,7 +101,9 @@ public class ProjectFilesTest : ClientBasedLanguageServerTest { Assert.Single(diagnostics1); // Stops after parsing await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName), projectFileSource); - await CreateAndOpenTestDocument(source, Path.Combine(directory, "source.dfy")); + var sourceFile = await CreateAndOpenTestDocument(source, Path.Combine(directory, "source.dfy")); + var diagnostics2 = await GetLastDiagnostics(sourceFile, CancellationToken); + Assert.Empty(diagnostics2.Where(d => d.Severity == DiagnosticSeverity.Error)); await AssertNoDiagnosticsAreComing(CancellationToken); } From 7a6914d09d0ccc4eba014eb73a22e58f04a1f09d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 7 Sep 2023 16:12:59 +0200 Subject: [PATCH 2/9] Add release note and fix path resolution in Dafny project file --- Source/DafnyCore/Options/DafnyProject.cs | 3 +++ docs/dev/news/4506.fix | 1 + 2 files changed, 4 insertions(+) create mode 100644 docs/dev/news/4506.fix diff --git a/Source/DafnyCore/Options/DafnyProject.cs b/Source/DafnyCore/Options/DafnyProject.cs index 90226c83b1c..04a769c78a7 100644 --- a/Source/DafnyCore/Options/DafnyProject.cs +++ b/Source/DafnyCore/Options/DafnyProject.cs @@ -139,7 +139,10 @@ public class DafnyProject : IEquatable { return false; } + var previousWorkingDirectory = Directory.GetCurrentDirectory(); + Directory.SetCurrentDirectory(Path.GetDirectoryName(Uri.LocalPath)); var parseResult = option.Parse(new[] { option.Aliases.First(), tomlValue }); + Directory.SetCurrentDirectory(previousWorkingDirectory); if (parseResult.Errors.Any()) { value = null; return false; diff --git a/docs/dev/news/4506.fix b/docs/dev/news/4506.fix new file mode 100644 index 00000000000..abf29f7417e --- /dev/null +++ b/docs/dev/news/4506.fix @@ -0,0 +1 @@ +Support all types of options in the Dafny project file (dfyconfig.toml) \ No newline at end of file From e913591e89fe2116ce917eb8ecd37500eb9136df Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 8 Sep 2023 11:15:33 +0200 Subject: [PATCH 3/9] Fixes for using library in options --- Source/DafnyCore.Test/DafnyProjectTest.cs | 4 +-- Source/DafnyCore/Options/DafnyProject.cs | 41 +++++++++++++++++------ 2 files changed, 33 insertions(+), 12 deletions(-) diff --git a/Source/DafnyCore.Test/DafnyProjectTest.cs b/Source/DafnyCore.Test/DafnyProjectTest.cs index e5e27233bfe..ce1c35265be 100644 --- a/Source/DafnyCore.Test/DafnyProjectTest.cs +++ b/Source/DafnyCore.Test/DafnyProjectTest.cs @@ -10,7 +10,7 @@ public class DafnyProjectTest { Uri = new Uri(randomFileName, UriKind.Absolute), Includes = new[] { "a", "a2" }, Excludes = new[] { "b", "b2" }, - Options = new Dictionary() { + Options = new Dictionary() { { "c", "d" }, { "e", "f" } } @@ -20,7 +20,7 @@ public class DafnyProjectTest { Uri = new Uri(randomFileName, UriKind.Absolute), Includes = new[] { "a2", "a" }, Excludes = new[] { "b2", "b" }, - Options = new Dictionary() { + Options = new Dictionary() { { "e", "f" }, { "c", "d" }, } diff --git a/Source/DafnyCore/Options/DafnyProject.cs b/Source/DafnyCore/Options/DafnyProject.cs index 04a769c78a7..a1272ec688c 100644 --- a/Source/DafnyCore/Options/DafnyProject.cs +++ b/Source/DafnyCore/Options/DafnyProject.cs @@ -2,14 +2,18 @@ using System.Collections; using System.Collections.Generic; using System.CommandLine; +using System.CommandLine.Parsing; using System.IO; using System.Linq; +using System.Reflection; using System.Runtime.Serialization; +using System.Text; using System.Text.RegularExpressions; using System.Threading.Tasks; using DafnyCore.Options; using Microsoft.Extensions.FileSystemGlobbing; using Tomlyn; +using Tomlyn.Model; namespace Microsoft.Dafny; @@ -22,7 +26,7 @@ public class DafnyProject : IEquatable { public Uri Uri { get; set; } public string[] Includes { get; set; } public string[] Excludes { get; set; } - public Dictionary Options { get; set; } + public Dictionary Options { get; set; } public bool UsesProjectFile => Path.GetFileName(Uri.LocalPath) == FileName; public static async Task Open(IFileSystem fileSystem, Uri uri, TextWriter outputWriter, TextWriter errorWriter) { @@ -139,19 +143,36 @@ public class DafnyProject : IEquatable { return false; } - var previousWorkingDirectory = Directory.GetCurrentDirectory(); - Directory.SetCurrentDirectory(Path.GetDirectoryName(Uri.LocalPath)); - var parseResult = option.Parse(new[] { option.Aliases.First(), tomlValue }); - Directory.SetCurrentDirectory(previousWorkingDirectory); + var printTomlValue = PrintTomlOptionToCliValue(tomlValue); + var parseResult = option.Parse(new[] { option.Aliases.First(), printTomlValue }); if (parseResult.Errors.Any()) { value = null; return false; } - - value = parseResult.GetValueForOption(option); + var previousWorkingDirectory = Directory.GetCurrentDirectory(); + // Change the current directory, for when converting string to file-paths. + Directory.SetCurrentDirectory(Path.GetDirectoryName(Uri.LocalPath)!); + // By using the dynamic keyword, we can use the generic version of GetValueForOption which does type conversion, + // which is sadly not accessible without generics. + value = parseResult.GetValueForOption((dynamic)option); + Directory.SetCurrentDirectory(previousWorkingDirectory); return true; } + record Verbatim(string value) { + public override string ToString() { + return value; + } + } + + string PrintTomlOptionToCliValue(object value) { + if (value is TomlArray array) { + return string.Join(" ", array); + } + + return value.ToString(); + } + public bool Equals(DafnyProject other) { if (ReferenceEquals(null, other)) { return false; @@ -161,13 +182,13 @@ public class DafnyProject : IEquatable { return true; } - var orderedOptions = Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty>(); - var otherOrderedOptions = other.Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty>(); + var orderedOptions = Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty>(); + var otherOrderedOptions = other.Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty>(); return Equals(Uri, other.Uri) && NullableSetEqual(Includes?.ToHashSet(), other.Includes) && NullableSetEqual(Excludes?.ToHashSet(), other.Excludes) && - orderedOptions.SequenceEqual(otherOrderedOptions, new LambdaEqualityComparer>( + orderedOptions.SequenceEqual(otherOrderedOptions, new LambdaEqualityComparer>( (kv1, kv2) => kv1.Key == kv2.Key && GenericEquals(kv1.Value, kv2.Value), kv => kv.GetHashCode())); } From c89fd3261fb7fae06925e0d2e0e1cfe9cb88f5a5 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 8 Sep 2023 11:21:34 +0200 Subject: [PATCH 4/9] Update release notes --- docs/dev/news/4435.feat | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/dev/news/4435.feat b/docs/dev/news/4435.feat index c77007ac7ed..1abaa28654e 100644 --- a/docs/dev/news/4435.feat +++ b/docs/dev/news/4435.feat @@ -1,10 +1,10 @@ The Dafny IDE now has improved behavior when working with a Dafny file that's part of a Dafny project. A Dafny file is part of a project if a `dfyconfig.toml` can be found somewhere in the file's path hierarchy, such as in the same folder or in the parent folder. A `dfyconfig.toml` can specify which Dafny options to use for that project, and can specify which Dafny files are part of the project. By default, the project will include all .dfy files reachable from the folder in which the `dfyconfig.toml` resides. Project related features of the IDE are: - Whenever one file in the project is opened, diagnostics for all files in the Dafny project are shown. When including a file with errors that's part of the same project, the message "the included file contains errors" is no longer shown. Instead, the included file's errors are shown directly. -- If any file in the project in changed, diagnostics for all files in the project are updated. Without a project, changing an included file will not update diagnostics for the including file until the including file is also changed. -- If any file in the project is resolved, all files in the project are resolved. Opening a file in a project that's already resolved means the opened file is resolved instantly. -- The IDE's memory consumption stays the same regardless of how many files in a project are opened. Without a project, the IDE increases it's memory usage for each open file. +- If any file in the project is changed, diagnostics for all files in the project are updated. Without a project, changing an included file will not update diagnostics for the including file until the including file is also changed. - The find references feature (also added in this release), works better in files that are part of a project, since only then can it find references that are inside files that include the current file. - The assisted rename feature (also added in this release), only works for files that are part of a project. -- For files that are part of a project, the Dafny IDE does not require the use of include directives to work, and neither does the CLI if you run it using the project file. This means that Dafny projects can be used without use include directives for files inside the project. When using library files that are outside the project, it's still necessary to use includes. +- When using a project file, it is no longer necessary to use include directives. In the previous version of Dafny, it was already the case that the Dafny CLI, when passed a Dafny project file, does not require include directives to process the Dafny program. The same now holds for the Dafny IDE when working with Dafny files for which a project file can be found. +- If any file in the project is resolved, all files in the project are resolved. Opening a file in a project that's already resolved means the opened file is resolved instantly. +- The IDE's memory consumption stays the same regardless of how many files in a project are opened. Without a project, the IDE increases it's memory usage for each open file. Try out the IDE's project support now by creating an empty `dfyconfig.toml` file in the root of your project repository. \ No newline at end of file From 8df76c846b190e10a2026d99cda8df9fe24dd097 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 8 Sep 2023 11:28:34 +0200 Subject: [PATCH 5/9] Run formatter --- Source/DafnyCore/Options/DafnyProject.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyCore/Options/DafnyProject.cs b/Source/DafnyCore/Options/DafnyProject.cs index a1272ec688c..75b2f8405ab 100644 --- a/Source/DafnyCore/Options/DafnyProject.cs +++ b/Source/DafnyCore/Options/DafnyProject.cs @@ -164,7 +164,7 @@ record Verbatim(string value) { return value; } } - + string PrintTomlOptionToCliValue(object value) { if (value is TomlArray array) { return string.Join(" ", array); @@ -172,7 +172,7 @@ record Verbatim(string value) { return value.ToString(); } - + public bool Equals(DafnyProject other) { if (ReferenceEquals(null, other)) { return false; From 7dde794773640b0576c55e9601f63de6503cbd2a Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 8 Sep 2023 19:23:00 +0200 Subject: [PATCH 6/9] More fixes --- Source/DafnyCore/Options/DafnyProject.cs | 29 +++++++++++++-------- Test/cli/projectFile/projectFile.dfy.expect | 2 +- 2 files changed, 19 insertions(+), 12 deletions(-) diff --git a/Source/DafnyCore/Options/DafnyProject.cs b/Source/DafnyCore/Options/DafnyProject.cs index 75b2f8405ab..ea747e662ac 100644 --- a/Source/DafnyCore/Options/DafnyProject.cs +++ b/Source/DafnyCore/Options/DafnyProject.cs @@ -143,33 +143,40 @@ public class DafnyProject : IEquatable { return false; } - var printTomlValue = PrintTomlOptionToCliValue(tomlValue); + var printTomlValue = PrintTomlOptionToCliValue(tomlValue, option); var parseResult = option.Parse(new[] { option.Aliases.First(), printTomlValue }); if (parseResult.Errors.Any()) { + errorWriter.WriteLine($"Error: Could not parse value '{tomlValue}' for option '{option.Name}' that has type '{option.ValueType.Name}'"); value = null; return false; } - var previousWorkingDirectory = Directory.GetCurrentDirectory(); - // Change the current directory, for when converting string to file-paths. - Directory.SetCurrentDirectory(Path.GetDirectoryName(Uri.LocalPath)!); // By using the dynamic keyword, we can use the generic version of GetValueForOption which does type conversion, // which is sadly not accessible without generics. value = parseResult.GetValueForOption((dynamic)option); - Directory.SetCurrentDirectory(previousWorkingDirectory); return true; } - record Verbatim(string value) { - public override string ToString() { - return value; - } - } + string PrintTomlOptionToCliValue(object value, Option valueType) { + var projectDirectory = Path.GetDirectoryName(Uri.LocalPath); - string PrintTomlOptionToCliValue(object value) { if (value is TomlArray array) { + if (valueType.ValueType == typeof(IEnumerable)) { + return string.Join(" ", array.Select(element => { + if (element is string elementString) { + return Path.GetFullPath(elementString, projectDirectory!); + } + + return element.ToString(); + })); + } + return string.Join(" ", array); } + if (value is string stringValue && valueType.ValueType == typeof(FileInfo)) { + value = Path.GetFullPath(stringValue, projectDirectory); + } + return value.ToString(); } diff --git a/Test/cli/projectFile/projectFile.dfy.expect b/Test/cli/projectFile/projectFile.dfy.expect index 82778703cd4..32b6fb8073a 100644 --- a/Test/cli/projectFile/projectFile.dfy.expect +++ b/Test/cli/projectFile/projectFile.dfy.expect @@ -9,7 +9,7 @@ Warning: only Dafny project files named dfyconfig.toml are recognised by the Daf Warning: option 'does-not-exist' that was specified in the project file, is not a valid Dafny option. Dafny program verifier did not attempt verification -Error: property 'warn-shadowing' is of type 'System.Int64' but should be of type 'System.Boolean' +Error: Could not parse value '3' for option 'warn-shadowing' that has type 'Boolean' input.dfy(6,8): Warning: Shadowed local-variable name: x moreInput.dfy(6,8): Warning: Shadowed local-variable name: x From 177f6cbd4b10223bea7b2876436d7d313104c4b2 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Sun, 10 Sep 2023 10:00:56 +0200 Subject: [PATCH 7/9] Trigger CI From e6a4a504133ff5c465f170c8690691cd5c67d19e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 11 Sep 2023 10:55:10 +0200 Subject: [PATCH 8/9] usesLibrary test now passes --- Source/DafnyCore/Options/DafnyProject.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Options/DafnyProject.cs b/Source/DafnyCore/Options/DafnyProject.cs index ea747e662ac..55c44aa1dfd 100644 --- a/Source/DafnyCore/Options/DafnyProject.cs +++ b/Source/DafnyCore/Options/DafnyProject.cs @@ -160,7 +160,7 @@ public class DafnyProject : IEquatable { var projectDirectory = Path.GetDirectoryName(Uri.LocalPath); if (value is TomlArray array) { - if (valueType.ValueType == typeof(IEnumerable)) { + if (valueType.ValueType.IsAssignableTo(typeof(IEnumerable))) { return string.Join(" ", array.Select(element => { if (element is string elementString) { return Path.GetFullPath(elementString, projectDirectory!); From 5e499c2b986d66c88623794ae90af7e1a6eb39f1 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 12 Sep 2023 13:44:30 +0200 Subject: [PATCH 9/9] Make test more stable --- Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs | 2 ++ .../DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs index e4950514827..e059c76bb5f 100644 --- a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs +++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs @@ -41,6 +41,8 @@ public class DafnyLanguageServerTestBase : LanguageProtocolTestBase { } }".TrimStart(); + protected string SlowToVerifyNoLimit => SlowToVerify.Replace(" {:rlimit 100}", ""); + protected readonly string NeverVerifies = @" lemma {:neverVerify} HasNeverVerifyAttribute(p: nat, q: nat) ensures true diff --git a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs index 80f92dfdbe4..a89e4ddd239 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs @@ -1082,7 +1082,7 @@ method test() method test() { assert false; } -".TrimStart() + SlowToVerify; +".TrimStart() + SlowToVerifyNoLimit; await SetUp(options => options.Set(BoogieOptionBag.Cores, 1U)); var documentItem = CreateTestDocument(source, "ApplyChangeBeforeVerificationFinishes.dfy"); client.OpenDocument(documentItem);