Validate language argument of translate command

[keyboardDrummer]

Validate language argument of translate command, so that an error is reported instead of crashing when the argument is specified incorrectly.

Old behavior:

dafny translate -t:cs test.dfy
Crash

New behavior:

dafny translate -t:cs test.dfy
No compiler found for language "-t=cs"; expecting one of 'cs' (C#), 'js' (JavaScript), 'go' (Go), 'java' (Java), 'py' (Python), 'cpp' (C++)

Partial fix for #3259

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

[davidcok]

I would find the proposed error message confusing. If the invalid argument begins with -t or --target, it should say something like

No compiler found for compileTarget "-t=cs" (use just a language name, not a -t or --target option); expecting one of

[keyboardDrummer]

I would find the proposed error message confusing. If the invalid argument begins with -t or --target, it should say something like

No compiler found for compileTarget "-t=cs" (use just a language name, not a -t or --target option); expecting one of

I don't think having custom code for that is not worth the effort/maintenance. I think the one in this PR provides ample help to guide the customer to the right path. And why would anyone use -t, assuming they were not already used to doing this with dafny translate because that's how it worked before?

In any case, can we merge this PR since it is a strict improvement over the old behavior?

[MikaelMayer]

I would find the proposed error message confusing. If the invalid argument begins with -t or --target, it should say something like
No compiler found for compileTarget "-t=cs" (use just a language name, not a -t or --target option); expecting one of

I don't think having custom code for that is not worth the effort/maintenance. I think the one in this PR provides ample help to guide the customer to the right path. And why would anyone use -t, assuming they were not already used to doing this with dafny translate because that's how it worked before?

Please listen to David's advice. I deeply care about new Dafny users, and the discrepancy between Dafny commands that you are introducing does require some explanation. This scenario will happen, so I really think it's worth the effort/maintenance. Why would anyone use -t? Simply because they might have used this option for build and run, and now they would like to translate to have fine-grain access, and they will try it.
For my part, I have argued that you should accept "-t " and "--target " as well as just "langage". It's ok not to like this idea and force users to use a single syntax, but at least I wouldn't make it more sound like we haven't thought that users would try "-t". They will.

[keyboardDrummer]

Please listen to David's advice. I deeply care about new Dafny users, and the discrepancy between Dafny commands that you are introducing does require some explanation. This scenario will happen, so I really think it's worth the effort/maintenance. Why would anyone use -t? Simply because they might have used this option for build and run, and now they would like to translate to have fine-grain access, and they will try it. For my part, I have argued that you should accept "-t " and "--target " as well as just "langage". It's ok not to like this idea and force users to use a single syntax, but at least I wouldn't make it more sound like we haven't thought that users would try "-t". They will.

Maybe, I'd like to think about it a little more. In the mean time, could we merge this PR? It improves the current behavior. I've updated this PR so it won't close issue #3259 that triggered this PR.

[MikaelMayer]

Here is what @davidcok and I have in mind.

Suggested change

	options.Printer.ErrorWriteLine(Console.Error, $"No compiler found for language \"{options.CompilerName}\"; expecting one of {known}");
	options.Printer.ErrorWriteLine(Console.Error, $"No compiler found for language \"{options.CompilerName}\"{(options.CompilerName.StartsWith("-t") || options.CompilerName.StartsWith("--") ? " (use just a language name, not a -t or --target option)" : "")}; expecting one of {known}");

If you accept that or a variation, I'll approve this PR and you can even ensure this PR closes issue #3274

[keyboardDrummer]

Thanks for writing the code :)

To add some context to my hesitation:

I'm planning on letting run/build/test auto detect the -t argument when you pass in any external source files, and probably also on renaming it to -l/--language.

I would also like dafny run to accept the outputs of dafny build, such as .jar and .dll files, and then attempt to auto-detect which CLI to call to run that output.

I would also like to consider at some point to add an additional argument runtime to dafny build, that lets you pick different values like dotnet, jdk, python, node, which could be useful when you're not passing in external sources, you don't care about the intermediate language, but you only have some specific runtimes installed so you want it to run on that. The runtime argument could also be passed to dafny run when you're passing a .dll, .jar, etc file, to let it decide how to run the file.

[MikaelMayer]

Wonderful, thanks for your flexibility !