Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support all option types in the project file #4506

Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
0beaffb
Support all option types in the project file
keyboardDrummer Sep 1, 2023
4946ac6
Merge branch 'master' into supportAllOptionTypesInProjectFile
keyboardDrummer Sep 7, 2023
7a6914d
Add release note and fix path resolution in Dafny project file
keyboardDrummer Sep 7, 2023
81c7863
Merge branch 'supportAllOptionTypesInProjectFile' of github.com:keybo…
keyboardDrummer Sep 7, 2023
8b3b1ee
Merge branch 'master' into supportAllOptionTypesInProjectFile
keyboardDrummer Sep 7, 2023
32c61ba
Merge branch 'master' into supportAllOptionTypesInProjectFile
keyboardDrummer Sep 7, 2023
e913591
Fixes for using library in options
keyboardDrummer Sep 8, 2023
c89fd32
Update release notes
keyboardDrummer Sep 8, 2023
327817f
Merge branch 'master' into supportAllOptionTypesInProjectFile
keyboardDrummer Sep 8, 2023
8df76c8
Run formatter
keyboardDrummer Sep 8, 2023
9e29a2a
Merge branch 'supportAllOptionTypesInProjectFile' of github.com:keybo…
keyboardDrummer Sep 8, 2023
7dde794
More fixes
keyboardDrummer Sep 8, 2023
19ca042
Merge branch 'master' into supportAllOptionTypesInProjectFile
keyboardDrummer Sep 8, 2023
177f6cb
Trigger CI
keyboardDrummer Sep 10, 2023
3146dc2
Merge branch 'supportAllOptionTypesInProjectFile' of github.com:keybo…
keyboardDrummer Sep 10, 2023
e6a4a50
usesLibrary test now passes
keyboardDrummer Sep 11, 2023
d52dd2c
Merge branch 'master' into supportAllOptionTypesInProjectFile
keyboardDrummer Sep 11, 2023
e7c0a23
Merge branch 'master' into supportAllOptionTypesInProjectFile
keyboardDrummer Sep 11, 2023
282a0ec
Merge branch 'master' into supportAllOptionTypesInProjectFile
keyboardDrummer Sep 11, 2023
5e499c2
Make test more stable
keyboardDrummer Sep 12, 2023
bbab8ae
Merge branch 'master' into supportAllOptionTypesInProjectFile
keyboardDrummer Sep 12, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
More fixes
  • Loading branch information
keyboardDrummer committed Sep 8, 2023
commit 7dde794773640b0576c55e9601f63de6503cbd2a
29 changes: 18 additions & 11 deletions Source/DafnyCore/Options/DafnyProject.cs
Original file line number Diff line number Diff line change
Expand Up @@ -143,33 +143,40 @@ public class DafnyProject : IEquatable<DafnyProject> {
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<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();
}

Expand Down
2 changes: 1 addition & 1 deletion Test/cli/projectFile/projectFile.dfy.expect
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Much better error message.

input.dfy(6,8): Warning: Shadowed local-variable name: x
moreInput.dfy(6,8): Warning: Shadowed local-variable name: x

Expand Down
Loading