-
Notifications
You must be signed in to change notification settings - Fork 256
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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:0
could 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.