Add top-level commands to Dafny and redesign the CLI UI V2

[keyboardDrummer]

Fixes #2036
Fixes #2360

Changes

• Introduce three commands for the Dafny CLI: verify, integrate, run, as defined in Introduce top level commands commands for Dafny #2036
• When commands are used, use a redesigned UI for the CLI
  • Use proper GNU options
    • (- and -- for short and long names, instead of - and / for long names)
    • Use = instead of : for specifying the value of an option in a single term
  • boolean options take true and false instead of 1 and 0 as arguments.
  • --<option> will mean the same as --<option>:true for boolean options
  • Boogie options can only be specified through the option --boogie="/loopUnroll:3 /overlookTypeErrors"
  • Some Boogie options are exposed at the Dafny level:
    • vscCores is exposed as cores
    • useBaseNameForFileName is exposed
    • timeLimit is exposed as verificationTimeLimit
  • Rename several options
    • compileTarget is renamed to target
    • dprint is renamed to print
    • print is renamed to bprint
    • compileVerbose has been inverted and renamed to quiet
  • Some options have been hidden, so they don't show up in help:
    • print (previously named dprint), rprint, bprint, printMode, useBaseNameForFileName
• There is a new mechanism for adding options, that allows adding options to both the new and old CLI UI. showSnippets is an existing option that has been refactored to make use of this new mechanism.
• Disable the use of compile, spillTargetCode and dafnyVerify when using commands.
• dafny <command> --help shows which options there are for that specific command.
• Many existing options are still missing in the new commands. The plan is to add them gradually while we convert our usage over to these commands, and to at the same time refactor some of these options.

Output from dafny --help:

Description:
  The Dafny CLI enables working with Dafny, a verification-aware programming language.

Usage:
  Dafny [command] [options]

Options:
  --version       Show version information
  -?, -h, --help  Show help and usage information

Commands:
  verify <file>     Verify the program.
  run <file>        Run the program.
  build <file>      Produce an executable binary.
  integrate <file>  Generate source and build files in a specified target language.

Output from dafny verify --help:

Description:
  Verify the program.

Usage:
  Dafny verify [<file>...] [options]

Arguments:
  <file>  input files

Options:
  --cores <count>                    Run the Dafny CLI using <n> cores. Defaults to 1. [default: 1]
  --verificationTimeLimit <seconds>  Limit the number of seconds spent trying to verify
                                     each procedure [default: 0]
  --showSnippets                     0 (default) - don't show source code snippets for Dafny messages
                                     1 - show a source code snippet for each Dafny message [default: False]
  --plugin <path to one assembly>    (experimental) One path to an assembly that contains at least one
                                     instantiatable class extending Microsoft.Dafny.Plugin.Rewriter.
                                     It can also extend Microsoft.Dafny.Plugins.PluginConfiguration to receive arguments
                                     More information about what plugins do and how define them:
                                     https://github.com/dafny-lang/dafny/blob/master/Source/DafnyLanguageServer/README.md#about-plugins []
  --boogie <boogie>                  arguments to boogie
  --prelude <file>                   choose Dafny prelude file
  -?, -h, --help                     Show help and usage information

Output from dafny run --help

Description:
  Run the program.

Usage:
  Dafny run [<file>...] [options]

Arguments:
  <file>  input files

Options:
  -t, --target <language>            cs (default) - Compilation to .NET via C#
                                     go - Compilation to Go
                                     js - Compilation to JavaScript
                                     java - Compilation to Java
                                     py - Compilation to Python
                                     cpp - Compilation to C++
  
                                     Note that the C++ backend has various limitations (see Docs/Compilation/Cpp.md).
                                     This includes lack of support for BigIntegers (aka int), most higher order
                                     functions, and advanced features like traits or co-inductive types. [default: cs]
  --noVerify                         Skip verification [default: False]
  --cores <count>                    Run the Dafny CLI using <n> cores. Defaults to 1. [default: 1]
  --verificationTimeLimit <seconds>  Limit the number of seconds spent trying to verify
                                     each procedure [default: 0]
  --showSnippets                     0 (default) - don't show source code snippets for Dafny messages
                                     1 - show a source code snippet for each Dafny message [default: False]
  --plugin <path to one assembly>    (experimental) One path to an assembly that contains at least one
                                     instantiatable class extending Microsoft.Dafny.Plugin.Rewriter.
                                     It can also extend Microsoft.Dafny.Plugins.PluginConfiguration to receive arguments
                                     More information about what plugins do and how define them:
                                     https://github.com/dafny-lang/dafny/blob/master/Source/DafnyLanguageServer/README.md#about-plugins []
  --boogie <boogie>                  arguments to boogie
  --prelude <file>                   choose Dafny prelude file
  -?, -h, --help                     Show help and usage information

Future work

• Expose --boogie="/print=<file" as dafny build --target=boogie
• Expose more Boogie options as first class Dafny options, so they don't require using --boogie
• Change --noVerify so it does not translate to and invoke Boogie.

Testing

• comp/separateCompilation/usesTimesTwo.dfy and git-issues/github-issue-305.dfy use dafny build
• comp/Arrays.dfy and comp/AsIs-Compile use dafny verify and dafny run
• Most of the tests using commands use longname options, and comp/AsIs-Compile also uses shortname options
• dafny0/AssumptionVariables1 uses boogie options through --boogie-<optionName>
• git-issue-2197.dfy tests the boolean option showSnippets without explicit truthy value, while ShowSnippets.dfy tests it with explicit thruthy value.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[keyboardDrummer]

@robin-aws Could we leave the --args discussion for another PR? I don't think merging this PR will immediately lock us into anything. This PR is 2k lines of changes and I would like to get it merged to prevent further conflicts, and make it easier to review further changes.

The follow-up of merging this PR can be looking at --args again, but will also include checking with Dafny users whether they can migrate to these commands; potentially making changes due to problems found during that migration; making more updates on the documentation side; so this PR is surely not the end of it.

[robin-aws]

@keyboardDrummer I can live with that. It does mean that we'll be stuck with carefully deprecating --args in favour of -- later on, instead of dropping it from the start in this new UI. But given you've already done the work to support --args here, that doesn't seem like a high maintenance burden.

I split off #2807 to track that improvement separately.

[MikaelMayer]

@cpitclaudel Thanks for the pointer to the previous discussion. I'm still not convinced by it though. I would happily disagree and commit since it's already implemented, but since we have an opportunity to change it with the new top level commands I will be annoying and push back, at least until I understand the reasoning better if that's all it takes. :)

-- was already used in some cases to unambiguously distinguish dotnet options from dotnet arguments

Isn't that an argument for -- being the least surprising syntax, since it's exactly what dotnet run does, and many other similar CLIs?

Are we worried about the case of invoking Dafny through dotnet like this?

dotnet run --no-build --project Source/Dafny/Dafny.csproj -- run MainWithArgs.dfy -- --print 42

The semantics of that should be unambiguous: the Dafny project's main method in C# receives ["run", "MainWithArgs.dfy", "--", "--print", "42"], and the MainWithArgs.dfy Dafny program receives ["--print", "42"].

If there is a way to change to --, I would accept it. What were the reasons again @cpitclaudel ?

[cpitclaudel]

Adressing feedback on -- from @seebees and @robin-aws:

Isn't that an argument for -- being the least surprising syntax, since it's exactly what dotnet run does, and many other similar CLIs?

I'll jump on too. -- is a standard way to express this.

I thought so too at first, but we ended up concluding the opposite and going with --args.

POSIX specifies that -- should be used to indicate the end of options (aka flags), i.e. to force a program to treat all that follows it as operands (non-option arguments). In that convention, -- is not used to set apart certain arguments. E.g. from POSIX:

Guideline 10:
The first -- argument that is not an option-argument should be accepted as a delimiter indicating the end of options. Any following arguments should be treated as operands, even if they begin with the '-' character.

What this means is that adding -- anywhere should not change the meaning of a command if none of the arguments start with -.

This is not the semantic that is being proposed here, since Dafny run a.dfy --args b.dfy c.dfy means something different from Dafny run a.dfy b.dfy --args c.dfy. This is what led us to reject -- as inadequate: -- is an escape character, not a separator.

Another illustration of this might be: how do you run a Dafny file called --print=.dfy? You would write Dafny run -- --print=.dfy --args foo bar baz. -- escapes what follows and prevents --print=.dfy from being treated as an option. --args then delimits arguments to the command.

This is the reason why GNU parallel uses --, not :::, I believe (but I could be wrong, since it also has :::: and :::+ etc).

Other tools use explicitly named arguments, like find -exec (which takes a terminator, ; or +).

Btw, tools like dotnet run get to use -- because they don't have operands; only options: you write dotnet run --project=blah.csproj arg1 arg2, not dotnet run blah.csproj arg1 arg2. But note that for most of these tools, the -- is optional (as it "should" be).

If Dafny run were changed to use an implicit project file instead of a .dfy, then using -- would be reasonable. (Note that it would not be enough to require exactly one .dfy file, because of the escaping remark above.)

We could also decide to repurpose -- as a delimiter instead of an escape character. The argument would be that we don't need escapes, because one can always use ./ as a quoting mechanism: Dafny run ./--print=.dfy -- foo bar baz. It looks pretty for sure.

[keyboardDrummer]

POSIX specifies that -- should be used to indicate the end of options (aka flags), i.e. to force a program to treat all that follows it as operands (non-option arguments).

Would this be a scenario where it would be better to deviate from POSIX and adhere to what the npm/npx and dotnet are doing? The behavior of those tools seems to be what several people (me, @MikaelMayer, @seebees , @robin-aws ) were expecting.

[cpitclaudel]

Would this be a scenario where it would be better to deviate from POSIX and adhere to what the npm/npx and dotnet are doing?

I think I'm missing something. As far as I can tell, both npm and dotnet (mostly) adhere to POSIX. How can we deviate from one and adhere to the other?

What I'm saying is: dotnet run foo is the same as dotnet run -- foo, and npm run blah.js -- arg is the same as npm run blah.js arg. That's not how --args works in Dafny: Dafny blah.dfy --args foo.dfy doesn't mean the same thing as Dafny blah.dfy foo.dfy.

So using -- instead of --args would deviate from both POSIX and dotnet run and npm run, right?

Or maybe I misunderstand the proposal and/or the way dotnet run works.

[cpitclaudel]

I would suggest renaming EmitBinary, but otherwise great :)

[cpitclaudel]

I think the previous one was a bit better, since in other cases we use verbs for things that Dafny does (e.g. "print information")

[cpitclaudel]

Never mind the comment above, looks like we use verbs for non-verbs things as well.

[cpitclaudel]

Is this rewrapped to 72 chars?

[robin-aws]

I ❤️ this so much. The streamlined help messages are a breath of fresh air, and I especially love the fact that we are better encapsulating Dafny's dependency on Boogie by not just allowing arbitrary passthrough options.

Based on playing around locally I couldn't find a way to display the old --help text, which we do need for users that haven't migrated to the new UI yet. I'd suggest having a --legacy-help option on the root command that prints that text, and perhaps adding a trailing line to draw attention to that ("Use --legacy-help to display help and usage information for using the CLI without commands")

[robin-aws]

Was this added accidentally or is it needed?

[robin-aws]

Better as a code comment than a PR comment :)

I've used CommandLineParser in a couple of other projects (TestDafny and XUnitExtensions), would you mind just adding a comment somewhere in the code base on what we're using in System.CommandLine that isn't in that library?

[robin-aws]

When I try just dafny on this branch I get:

$ dafny
*** Error: No input files were specified in command-line .

I think we can safely break that behavior so we get a better default help message.

[robin-aws]

AFAICT we standardized on hyphen-separated names (--no-verify, --verification-time-limit, etc), is there a reason this isn't --show-snippets?

[robin-aws]

This looks like a useful change, but can you document what actual types are supported as substitution values? AFAICT it's either string or IEnumerable<string>.

[robin-aws]

Based on playing around locally I couldn't find a way to display the old --help text, which we do need for users that haven't migrated to the new UI yet. I'd suggest having a --legacy-help option on the root command that prints that text, and perhaps adding a trailing line to draw attention to that ("Use --legacy-help to display help and usage information for using the CLI without commands")

I stand corrected, I didn't realize /help was and is still the way to get the old help text. I still say --help and /help should mention each other's existence though.