Support all option types in the project file

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<string, string>() {
+ Options = new Dictionary<string, object>() {
  { "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<string, string>() {
+ Options = new Dictionary<string, object>() {
  { "e", "f" },
  { "c", "d" },
  }

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<DafnyProject> {
  public Uri Uri { get; set; }
  public string[] Includes { get; set; }
  public string[] Excludes { get; set; }
- public Dictionary<string, string> Options { get; set; }
+ public Dictionary<string, object> Options { get; set; }
  public bool UsesProjectFile => Path.GetFileName(Uri.LocalPath) == FileName;
 
  public static async Task<DafnyProject> Open(IFileSystem fileSystem, Uri uri, TextWriter outputWriter, TextWriter errorWriter) {
@@ -139,19 +143,43 @@ public class DafnyProject : IEquatable<DafnyProject> {
  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, 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;
  }
-
- value = parseResult.GetValueForOption(option);
+ // 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);
  return true;
  }
 
+ string PrintTomlOptionToCliValue(object value, Option valueType) {
+ var projectDirectory = Path.GetDirectoryName(Uri.LocalPath);
+
+ if (value is TomlArray array) {
+ if (valueType.ValueType == typeof(IEnumerable<FileInfo>)) {
+ 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();
+ }
+
  public bool Equals(DafnyProject other) {
  if (ReferenceEquals(null, other)) {
  return false;
@@ -161,13 +189,13 @@ public class DafnyProject : IEquatable<DafnyProject> {
  return true;
  }
 
- var orderedOptions = Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty<KeyValuePair<string, string>>();
- var otherOrderedOptions = other.Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty<KeyValuePair<string, string>>();
+ var orderedOptions = Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty<KeyValuePair<string, object>>();
+ var otherOrderedOptions = other.Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty<KeyValuePair<string, object>>();
 
  return Equals(Uri, other.Uri) &&
  NullableSetEqual(Includes?.ToHashSet(), other.Includes) &&
  NullableSetEqual(Excludes?.ToHashSet(), other.Excludes) &&
- orderedOptions.SequenceEqual(otherOrderedOptions, new LambdaEqualityComparer<KeyValuePair<string, string>>(
+ orderedOptions.SequenceEqual(otherOrderedOptions, new LambdaEqualityComparer<KeyValuePair<string, object>>(
  (kv1, kv2) => kv1.Key == kv2.Key && GenericEquals(kv1.Value, kv2.Value),
  kv => kv.GetHashCode()));
  }

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
 

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.