-
Notifications
You must be signed in to change notification settings - Fork 261
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
Allow the :test attribute when using run and build #3275
Changes from all commits
529bd38
675998d
401e432
2f1e680
4513439
72a5b70
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -5,13 +5,18 @@ namespace Microsoft.Dafny; | |
|
||
public class DeveloperOptionBag { | ||
|
||
public static readonly Option<bool> SpillTranslation = new("--spill-translation", | ||
@"In case the Dafny source code is translated to another language, emit that translation.") { | ||
IsHidden = true | ||
}; | ||
|
||
public static readonly Option<bool> UseBaseFileName = new("--use-basename-for-filename", | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. There are instances of the old spelling that ought to be changed concurrently (even if the old spelling still works): There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Seems like this grep was not done on this PR. I only see three occurrences in comments (that have been resolved now) There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. My mistake, and I was also looking a a stale list of changes... |
||
"When parsing use basename of file for tokens instead of the path supplied on the command line") { | ||
IsHidden = true | ||
}; | ||
|
||
public static readonly Option<string> BoogiePrint = new("--bprint", | ||
@" | ||
@" | ||
Print Boogie program translated from Dafny | ||
(use - as <file> to print to console)".TrimStart()) { | ||
IsHidden = true, | ||
|
@@ -33,6 +38,8 @@ Print Dafny program after resolving it. | |
}; | ||
|
||
static DeveloperOptionBag() { | ||
DafnyOptions.RegisterLegacyBinding(SpillTranslation, (o, f) => o.SpillTargetCode = f ? 1U : 0U); | ||
|
||
DafnyOptions.RegisterLegacyBinding(ResolvedPrint, (options, value) => { | ||
options.DafnyPrintResolvedFile = value; | ||
options.ExpandFilename(options.DafnyPrintResolvedFile, x => options.DafnyPrintResolvedFile = x, options.LogPrefix, | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just checking that the intended behavior is that methods marked {:test} are only compiled when testing
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
They're always compiled when compiling, but the C#
XUnit.Fact
attribute is only added when usingdafny translate
.