Chore: Not generate boogie translation if not verifying #6067
Conversation
And not activated by default if `--no-verify` is set. This option emulates the `/dafnyVerify` command in the previous CLI Added tests
| @@ -46,6 +46,8 @@ public static class BoogieOptionBag { | |||
|
|
|||
| public static readonly Option<bool> NoVerify = new("--no-verify", "Skip verification"); | |||
|
|
|||
| public static readonly Option<bool> DoBoogieTranslation = new("--do-boogie-translation", "Requires --no-verify. Does translation to Boogie but Boogie won't verify it."); | |||
There was a problem hiding this comment.
It seems strange to have an option that can only be used if another option is also used. Why not have the first option imply the second then? Instead of --do-boogie-translation why not have --no-verify-boogie that tells Dafny to translate to Boogie but not verify it.
That way, whenever the user would type --no-verify --do-boogie-translation they only have to type --no-verify-boogie.
Secondly, I would make this option hidden since it only seems useful for the purpose of debugging the Dafny verification pipeline.
Thirdly, why are you adding this option? Is someone missing this? An alternative would be to let --no-verify --bprint ... cause Dafny to translate to Boogie but not verify that Boogie, and --no-verify to not translate to Boogie at all.
There was a problem hiding this comment.
Let's do the simple way. Since we already have --bprint, we can use it as the flag to do boogie translation, period. I like that idea.
There was a problem hiding this comment.
And --pprint as well. Added
MikaelMayer
changed the title
--do-boogie-translation| DafnyOptions.RegisterLegacyBinding(NoVerify, (options, dotNotVerify) => { | ||
| var shouldVerify = !dotNotVerify && !options.Get(HiddenNoVerify); | ||
| options.Verify = shouldVerify; // Boogie won't verify | ||
| options.DafnyVerify = shouldVerify || options.Get(DeveloperOptionBag.BoogiePrint) != null; |
There was a problem hiding this comment.
Could you add || options.Get(DeveloperOptionBag.SplitPrint) != null ?
| @@ -49,7 +49,7 @@ static RunCommand() { | |||
| Concat(DafnyCommands.ConsoleOutputOptions). | |||
| Concat(DafnyCommands.ResolverOptions); | |||
|
|
|||
| public static Command Create() { | |||
| public static Command Create(Func<DafnyOptions, int> continuation = null) { | |||
There was a problem hiding this comment.
It's to be able to create a Run command but with a continuation different than the one that launches the regular pipeline, to be able to test the parsing of options only. If you have any other way I could achieve the same result, I'd happily consider it.
docs/DafnyRef/UserGuide.md
Outdated
| @@ -2294,6 +2294,8 @@ and what information it produces about the verification process. | |||
|
|
|||
| * `--no-verify` - turns off verification (for translate, build, run commands) | |||
|
|
|||
| * `--do-boogie-translation` - turns on translation to Boogie after resolving or if `--no-verify` is set. Automatically set if `--bprint` is set. | |||
There was a problem hiding this comment.
Outdated, please remove
| [Fact] | ||
| public async Task RunFlagsOverride() { | ||
| await TestCliRunArgs([], options => { | ||
| Assert.True(options.DafnyVerify); |
There was a problem hiding this comment.
I'm not a fan of tests for values in options., since these are implementation details. In the future we could do a refactoring that removes options.DafnyVerify, and then what would we do with this test?
There was a problem hiding this comment.
Implementation details can still be tested by unit tests, and this is the meaning of that.
If we remove options.DafnyVerify, we would simply remove that test (and add new tests to test the new behavior).
There was a problem hiding this comment.
But why test like this? You could also test without looking at internals. For example, by using the --progress Symbol flag, you will see different results when using --no-verify and when not using it, and of course you can check that --no-verify --bprint still creates a file.
What was changed?
I ensure the
Options.DafnyVerifyis set to false if--no-verifyis provided, except if--bprintis setHow has this been tested?
A new driver test verifies the new behavior. Without the test, I got it wrong, so I'm confident that the test ensures the behavior is correct.
I don't think there is another way to test that the Boogie translation does not happen when it won't actually verify;
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.