--show-snippets with default true and off in tests #4087
Conversation
davidcok
changed the title
|
I'm OK with this change, but requested some others to review as well. |
docs/check-examples
Outdated
| @@ -379,11 +380,11 @@ do | |||
| else | |||
| if [ "$command" == "%check-legacy" ]; then | |||
| isverbose=-compileVerbose:$checkIds | |||
| (cd "$dir"; "$dafny" $verb $dOptions $isverbose ${options[@]} $text ) > "$actualOut" 2> "$actualError" | |||
| (cd "$dir"; "$dafny" $verb /showSnippets:0 $dOptions $isverbose ${options[@]} $text ) > "$actualOut" 2> "$actualError" | |||
There was a problem hiding this comment.
@keyboardDrummer This looks suspicious, it should probably be --show-snippets:false
There was a problem hiding this comment.
$verb is always empty at this point -- this is the branch for legacy CLI tests. SO it is correct, but perhaps $verb could be removed.
There was a problem hiding this comment.
Removed $verb on this line to avoid confusion.
There was a problem hiding this comment.
And tests now pass after nightlies have been fixed. Mikael - can you approve now?
…/dafny into cok-3304-show-snippet-2
There was a problem hiding this comment.
I'm fine with changing the default here since most users aren't going to be parsing console output, and even if they are broken by this it's just a matter of adding --show-snippets:false.
But on that note, do add a release note to explicitly call this change out, so it's easier for users to spot it.
(not explicitly requesting changes so another reviewer is free to approve once this is done)
|
Mikael (or Robin) - I have added a release note per Robin’s request. Please approve the PR or let me know what else needs improvement.
Thanks - David
… On Jun 19, 2023, at 5:10 PM, Robin Salkeld ***@***.***> wrote:
@robin-aws commented on this pull request.
I'm fine with changing the default here since most users aren't going to be parsing console output, and even if they are broken by this it's just a matter of adding --show-snippets:false.
But on that note, do add a release note to explicitly call this change out, so it's easier for users to spot it.
(not explicitly requesting changes so another reviewer is free to approve once this is done)
—
Reply to this email directly, view it on GitHub <#4087 (review)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABITDQEB3RVNIFLQDPK4FFLXMC54BANCNFSM6AAAAAAYQURHDM>.
You are receiving this because you authored the thread.
|
| @@ -0,0 +1 @@ | |||
| errors issued in command-line mode now show source code context by default; this behavior can be disabled using the option --show-snippets:false. | |||
There was a problem hiding this comment.
I would phrase this as "Errors emitted by the command-line interface". "Mode" seems like a strange concept here, since the IDE and CLI are so different as an experience, I wouldn't describe them as two different modes.
A recent change (#4087) explicitly turned on snippets in `lit`-based testing. The change causes many tests to fail, when run using `lit`. This PR turns them back off. <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>
Adjusts the tests so that if --show-snippets is on by default, the tests do not fail.
Also sets --show-snippets on by default.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.