Adjustments to options for dafny resolve

[davidcok]

Summary

The current options for dafny resolve are not all appropriate. Here are suggested changes.

Background and Motivation

The options for each command in the new CLI are in flux (and will be based on user needs as well). But some current ones are inappropriate.

Proposed Feature

Remove these options from dafny resolve:

--boogie (just for --verify and other commands that do verification)

--disable-nonlinear-arithmetic (just for --verify and other commands that do verification)

--relax-definite-assignment (just for --verify and other commands that do verification)

--plugin (only applies in legacy mode at present)

Perhaps the default for the following should be true in the new CLI
--warn-missing-constructor-parentheses Emits a warning when a constructor
name in a case pattern is not
followed by parentheses.
Also

--unicode-char needs a default stated

Alternatives

No response

[keyboardDrummer]

Why wouldn't you expect --plugin for dafny resolve ? Plugins can effect resolution behavior.

[keyboardDrummer]

#3227 resolves most of this except the defaults for warnings.

[davidcok]

I was thinking of --plugin as a standalone tool, like audit or doc. But you are right. They could just change some functionality for a phase of the compiler.