Allow the :test attribute when using run and build #3275
Conversation
| @@ -3390,7 +3390,7 @@ private class CSharpCompilationResult { | |||
| } | |||
|
|
|||
| private void AddTestCheckerIfNeeded(string name, Declaration decl, ConcreteSyntaxTree wr) { | |||
| if (DafnyOptions.O.RunAllTests || !Attributes.Contains(decl.Attributes, "test")) { | |||
| if (DafnyOptions.O.Compile || DafnyOptions.O.RunAllTests || !Attributes.Contains(decl.Attributes, "test")) { | |||
There was a problem hiding this comment.
Just checking that the intended behavior is that methods marked {:test} are only compiled when testing
There was a problem hiding this comment.
They're always compiled when compiling, but the C# XUnit.Fact attribute is only added when using dafny translate.
| @"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.
There are instances of the old spelling that ought to be changed concurrently (even if the old spelling still works):
grep -r -e '--useBaseNameForFileName' ../.. | grep -v Binary
../../Test/lit.site.cfg:'--useBaseNameForFileName',
../../Source/DafnyDriver/DafnyDriver.cs: "--useBaseNameForFileName",
../../Source/DafnyCore/Options/DeveloperOptionBag.cs: public static readonly Option UseBaseFileName = new("--useBaseNameForFileName",
../../Source/IntegrationTests/bin/Debug/net6.0/TestFiles/LitTests/LitTest/lit.site.cfg:'--useBaseNameForFileName',
../../Source/IntegrationTests/bin/Debug/net6.0/TestFiles/LitTests/LitTest/lit.site.cfg:config.substitutions.append( ('%resolveargs', "--useBaseNameForFileName" ) )
../../docs/check-examples:## "dafny verify --useBaseNameForFileName $F" and checks
../../docs/check-examples:## "dafny resolve --useBaseNameForFileName $F" and checks
../../docs/check-examples:## "dafny run --useBaseNameForFileName $F" and,
../../docs/check-examples: "$dafny" $com --useBaseNameForFileName $options $text > actual
There was a problem hiding this comment.
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.
My mistake, and I was also looking a a stale list of changes...
Thanks for making this option consistently spelled.
Fixes dafny-lang#3260 Also adds a hidden `--spill-translation` attribute for the `run`,`build` and `test` commands. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Fixes #3260
Also adds a hidden
--spill-translationattribute for therun,buildandtestcommands.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.