Add --verbosity and --solver-opt flags
#3625
Conversation
Accepts Silent, Quiet, Normal, and Trace options. Defaults to Normal, which is the prior behavior. The previous --verbose flag is now gone, and CompileVerbose is set when the verbosity level is Trace.
Also add a test for this and --verbosity
| public static readonly Option<string> SolverPlugin = new("--solver-plugin", @"Specify a plugin to use to solve verification conditions (instead of an external Z3 process)."); | ||
| public static readonly Option<string> SolverLog = new("--solver-log", @"Specify a file to use to log the SMT-Lib text sent to the solver."); | ||
| public static readonly Option<IList<string>> SolverOpt = new("--solver-opt", @"Specify an option to control how the solver works."); |
There was a problem hiding this comment.
I don't think there is a need to be cryptic: call it --solver-options
| new("--error-limit", () => 5, "Set the maximum number of verification errors to report (0 for unlimited)."); | ||
|
|
||
| public static readonly Option<Boogie.CoreOptions.VerbosityLevel> Verbosity = | ||
| new("--verbosity", () => CoreOptions.VerbosityLevel.Normal, "Set the level of output produced. Ranges from nothing (Silent) to detailed (Trace). With 'Normal', produce warnings, errors, and some extra information. With 'Quiet', produce only errors and warnings."); |
There was a problem hiding this comment.
The definition of VerbosityLevel is somehow not in these diffs.
Between Normal and Trace there should be a Verbose level which matches whatever the previous --verbose option did. To me Trace connotes even more output - detailed events along the way.
There was a problem hiding this comment.
The previous --verbose option affected only compilation, and was more like verification tracing, so it seemed like it made sense to put it in the same bucket.
There was a problem hiding this comment.
I still would like a level in between. The step from Normal to Trace seems huge. I don't expect anyone to use TRACE as a matter of course -- just when needing to understand what is going wrong with something. Whereas verbose is just a bit more information than normal, but not an overwhelming amount.
For example, I need a way to turn on explanations of error messages on the command-line (like we are putting into hover text in the IDE). Not on by default. But then if accompanied by lots of other 'tracing' information would be too much.
| public static readonly Option<int> VerificationErrorLimit = | ||
| new("--error-limit", () => 5, "Set the maximum number of verification errors to report (0 for unlimited)."); | ||
|
|
||
| public static readonly Option<Boogie.CoreOptions.VerbosityLevel> Verbosity = |
There was a problem hiding this comment.
Let's define our own VerbosityLevel enum. I don't think this is the type of thing we want to import from Boogie. Why would Dafny have the same levels as Boogie?
|
I'm now thinking that I'm going to create a new PR that just updates Boogie. |
|
verbosity (or a better name) should definitely be an option for every dafny command -- even if it doe snot control anything now, it may well in the future. I have some ideas in mind already. |
Sounds good. Let's chat about it and do this properly after 4.0. |
|
Closing in favor of #3943. |
Addresses most of #3468. Additional help flags (for solver options, attributes), control of deprecation, extraction of counterexamples, and something like
/noCheating:0could still potentially be valuable.Bumps the Boogie dependency along the way.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.