Add two options, /quiet and /silent

[atomb]

The /quiet option suppresses output other than warnings and errors. The /silent option suppresses all output except the exit code.

[davidcok]

LGTM, aside from my comments, but I'm not familiar with boogie code, so another review would be appropriate.

[davidcok]

Elsewhere you test with == against Silent. Choose one consistent method of comparison.

[atomb]

Done.

[davidcok]

Does boogie have an exit code to test?

[atomb]

I thought it did, but apparently not! So -silent is not super useful for Boogie alone. The internal option it controls is useful for clients of Boogie as a library, like Dafny, however.

[davidcok]

How does dafny know whether boogie is successful or not? I presume it makes some API call rather than spawning a command-line invocation.

I suggest you add an issue for boogie to return a proper exit code (though it is not an issue for me) like all good citizens should

[shazqadeer]

Is the exit code typically spit out on the console along with other output?

It would be great if we could add the standard story for exit code to Boogie also.

[davidcok]

In dafny testing, we write things like %exits-with 1 %parallel-boogie ...
to check the output exit code

[atomb]

Dafny uses Boogie as a library, so it inspects the verification results directly. I added #695 to make Boogie emit a non-zero exit code when verification fails, like Dafny does.

[keyboardDrummer]

Could you say something about the use-case for this change? I'm guessing it was made in support of Dafny. However, I'm surprised this would affect Dafny, because it works through the ConsolePrinter, a class that Dafny will override anyways.

From Boogie's perspective, it seems like a reasonable change, but as you commented the silent option can't affectively be used right now. Should we fix that?

---

More generally, I wonder whether Dafny should allow Boogie to write anything to the Console, or whether Dafny should take full ownership of its stdio, just like it new takes full ownership of its options.

I'm guessing that by default Dafny should not allow Boogie to write anything to stdio, and rely purely on an C# API provided by Boogie to get data that it then uses to write output. If Dafny is configured to show debug output, then it could show debug output from Boogie as well.

[atomb]

Could you say something about the use-case for this change? I'm guessing it was made in support of Dafny. However, I'm surprised this would affect Dafny, because it works through the ConsolePrinter, a class that Dafny will override anyways.

The key use case for this is in testing, particularly when testing manually. Running with /silent and seeing no output is an indication of no internal failures (regardless of the status of verification).

Dafny extends ConsolePrinter, but doesn't override these methods (though it could). My inclination is that it's nice to have Dafny and Boogie behave the same way when it comes to printing errors, warnings, and verification summaries, and therefore to have this in Boogie.

From Boogie's perspective, it seems like a reasonable change, but as you commented the silent option can't affectively be used right now. Should we fix that?

As I mentioned above, I think there still is a useful role for /silent even with the current exit code behavior. Addressing #695 would make it more useful, but I'm happy to leave that as a separate task.

More generally, I wonder whether Dafny should allow Boogie to write anything to the Console, or whether Dafny should take full ownership of its stdio, just like it new takes full ownership of its options.

I'm guessing that by default Dafny should not allow Boogie to write anything to stdio, and rely purely on an C# API provided by Boogie to get data that it then uses to write output. If Dafny is configured to show debug output, then it could show debug output from Boogie as well.

This seems like a reasonable approach, on the Dafny side. :) I don't think the answer will affect what we do with Boogie right now, though.

[davidcok]

I like tools that have a quiet option for scripting. This just makes dafny fit in well -- plus I've heard requests for an option to shut off info message.

Completely silent is a rarer need, but I've used it in CI on other projects.

[keyboardDrummer]

Could you say something about the use-case for this change? I'm guessing it was made in support of Dafny. However, I'm surprised this would affect Dafny, because it works through the ConsolePrinter, a class that Dafny will override anyways.

The key use case for this is in testing, particularly when testing manually. Running with /silent and seeing no output is an indication of no internal failures (regardless of the status of verification).

Dafny extends ConsolePrinter, but doesn't override these methods (though it could). My inclination is that it's nice to have Dafny and Boogie behave the same way when it comes to printing errors, warnings, and verification summaries, and therefore to have this in Boogie.

From Boogie's perspective, it seems like a reasonable change, but as you commented the silent option can't affectively be used right now. Should we fix that?

As I mentioned above, I think there still is a useful role for /silent even with the current exit code behavior. Addressing #695 would make it more useful, but I'm happy to leave that as a separate task.

More generally, I wonder whether Dafny should allow Boogie to write anything to the Console, or whether Dafny should take full ownership of its stdio, just like it new takes full ownership of its options.
I'm guessing that by default Dafny should not allow Boogie to write anything to stdio, and rely purely on an C# API provided by Boogie to get data that it then uses to write output. If Dafny is configured to show debug output, then it could show debug output from Boogie as well.

This seems like a reasonable approach, on the Dafny side. :) I don't think the answer will affect what we do with Boogie right now, though.

Makes sense, thanks.