Let target be an argument instead of an option for translate

[keyboardDrummer]

Changes

Changes the --target option for dafny translate into a <language> argument, so that users don't accidentally run dafny translate with a target they didn't want. Since there are many targets and only one is correct, accepting a default target likely wastes user's time by letting them wait for dafny translate to finish, inspecting the results, and then discovering it was translated to the wrong language and they should probably look at the options.

Rename --compile-verbose to --verbose

Data

New help:

Description:
  Translate Dafny sources to source and build files in a specified language.

Usage:
  Dafny translate <language> [<file>...] [options]

Arguments:
  <language>  cs - Translate to C#.
              go - Translate to Go.
              js - Translate to JavaScript.
              java - Translate to Java.
              py - Translate to Python.
              cpp - Translate 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.
  <file>      input files

Options:
  -o, --output <file>                          Specify the filename and location for the generated target language files.
  --verbose                                    Print information such as files being written by the compiler to the console
  --include-runtime                            Include the Dafny runtime as source in the target language.
...

Old help:

Description:
  Generate source and build files in a specified target language.

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

Arguments:
  <file>  input files

Options:
  -o, --output <file>                          Specify the filename and location for the generated target language files.
  --compile-verbose                            Print information such as files being written by the compiler to the console
  --include-runtime                            Include the Dafny runtime as source in the target language.
  -t, --target <language>                      cs - Compile to .NET via C#.
                                               go - Compile to Go.
                                               js - Compile to JavaScript.
                                               java - Compile to Java.
                                               py - Compile to Python.
                                               cpp - Compile to C++.

...

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

[davidcok]

The --compile-verbose option would be better named --translate-verbose or even just --verbose

[atomb]

Am I right in understanding that this change is just envisioned for translate and not build or run? I believe that the latter two are most useful if the language is not required, and that there's a notion of building and running a Dafny program that doesn't require the user to care about what intermediate languages are involved. But, for translate, I can see the argument for requiring a target language, because you likely care pretty strongly what that language is (either to read the output or integrate it with some other system).

[keyboardDrummer]

Am I right in understanding that this change is just envisioned for translate and not build or run? I believe that the latter two are most useful if the language is not required, and that there's a notion of building and running a Dafny program that doesn't require the user to care about what intermediate languages are involved. But, for translate, I can see the argument for requiring a target language, because you likely care pretty strongly what that language is (either to read the output or integrate it with some other system).

That's right!

[MikaelMayer]

Could you please add as a follow-up PR an element in docs/dev/* so that we can announce to the world this breaking change? Even if you believe no one actually relied on this command before, we need to announce it.

Also, when we will have project files, the language option should be optional as I believe will be possible to provide it directly in the project file.

[keyboardDrummer]

Could you please add as a follow-up PR an element in docs/dev/* so that we can announce to the world this breaking change? Even if you believe no one actually relied on this command before, we need to announce it.

Sure: #3253

[davidcok]

The text under "New Help" still lists --compile-verbose