feat: Dafny Main method to accept optional seq<string> argument

[MikaelMayer]

Fixes #1116

Ability to write in a file program.dfy (it works for all previous cases of main methods)

def Main(args: seq<string>) {
  if |args| == 3 {
    print args[0], " says ", args[1], " and ", args[2];
  } else {
    print "I need two arguments";
  }
}

and then run it, either with

> dafny /compile:3 program.dfy -- hello world
dotnet says hello and world
> dafny /compile:3 /compileTarget:java program.dfy -- hello world
java says hello and world
> dafny /compile:3 /compileTarget:js program.dfy -- hello world
<full path to the javascript file> says hello and world

or by compiling it first

> dafny /compile:1 program.dfy
> dotnet run program.dll -- hello world
dotnet says hello and world

Design decisions:

• The argument's array is truly the arguments passed in the command line, and includes the executable if there is one on position 0. One problem is that in Java and dotnet, there is no executable name passed in arguments, so it's for consistency. with the other languages.
• Support for one seq<string> because in C++, Dafny arrays don't have a length, so we need to handle sequences, otherwise no one would be able to handle arguments in C++
• Dafny's CLI option to input arguments is -- arg1 arg2 in the command line to pass two extra arguments after the option /compile:4
• Internally, the option is named DafnyOptions.MainArgs and is a List<string>, and it has an automatic conversion to string-like arguments for processes using DanfyOptions.ArgsStringExtra
• Support for C#, Java, JavaScript, Go, Python and C++, both with /compile:3 and running the compiled version made with /compile:2
• Added tests for the error message when the type of the argument is not supported
• Added documentation in the options and in the reference manual.

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

[cpitclaudel]

• Should we use a seq instead of an array?
• Can we have /arg:arg1 /arg:arg2 instead of /mainArgs:arg1 arg2? This way there's no separate quoting? Or even /mainArgs arg1 arg2 arg3 …?

DRCok: I would not use : separated arguments because arguments often contain :
I'd prefer comma-separated to :, but I'm OK with space-separated with quotes as needed

[MikaelMayer]

• Should we use a seq instead of an array?

I opened the discussion so feel free to propose arguments. I already succinctly explained my default rationale of picking an array instead of a seq, because

1. It's one less thing to convert (ok, with the loop we could say it would be free to do the conversion)
2. It's easier to convert an array to a seq in Dafny (arr[..] instead of new string[|sequence|](i requires 0 <= i < |sequence| => sequence[i]);)
3. in every language, we get an array, not an immutable vector of arguments. So I think it's more logical to use array to expose what's coming in.
4. as long as we don't mutate the array, it behaves like a sequence, so for usability, there is little difference.

Arguments I can think of in favor of sequence by default are

1. If we need to add default arguments, we can simply concatenate with another sequence. For arrays, we would need to make a conversion to sequence first as arrays aren't extensible
2. sequences are more "Dafny-like" than arrays since they are immutable.

• Can we have /arg:arg1 /arg:arg2 instead of /mainArgs:arg1 arg2? This way there's no separate quoting? Or even /mainArgs arg1 arg2 arg3 …?

The first one is possible. What do other people think about that? I've implemented it.
The second one is hardly possible, because we can't predict the number of arguments.

DRCok: I would not use : separated arguments because arguments often contain : I'd prefer comma-separated to :, but I'm OK with space-separated with quotes as needed

[davidcok]

Usually a repeated CLI option overrules an earlier one. To me that argues (a bit) against /arg
I'm still OK with /mainArgs (or /args) with a quoted list if necessary.

I see the main purpose of this feature being to support creating executables from Dafny that when run standalone can take arguments (like "real" programs). The use case of having arguments when run from "dafny run ..." should be supported, but is less important to me and I'm willing to keep it simple with the quoted argument list.

[MikaelMayer]

Usually a repeated CLI option overrules an earlier one. To me that argues (a bit) against /arg

We already broke this "usually" with plugins. It's possible to specify multiple plugins via repeated /plugin: option.

[cpitclaudel]

This looks odd — what happens if someone has a Dafny module called os?

[MikaelMayer]

Then there will be a compilation failure. What would be the alternative?

[cpitclaudel]

A clean error produced by Dafny; but what is bothering me is the special case on the string os. We could store tuples in the list of modules (maybe ("os", "Args") and (id, DummyTypeName))

[MikaelMayer]

What do you mean by "we could store tuples in the list of modules"?
One could make this error go away by suppressing these dummy calls.
But overall, I think that if this is a problem down the road, the Go compiler will have to compile a Dafny module named "os" to something else, since "os" is a base package in Go anyway.

[cpitclaudel]

This isn't safe; arguments shouldn't be concatenated as strings

[MikaelMayer]

That's unfortunately the only way to launch a ProcessInfo:

https://docs.microsoft.com/en-us/dotnet/api/system.diagnostics.processstartinfo.-ctor?view=net-6.0#system-diagnostics-processstartinfo-ctor(system-string-system-string)

[cpitclaudel]

Thankfully that's not right :) Here's an example of how to do it:

dafny/Source/AutoExtern.Test/Tests.cs

Lines 16 to 31 in 5058d5a

	var startInfo = new ProcessStartInfo("dotnet") {
	UseShellExecute = false,
	WorkingDirectory = minimalDirectory
	};
	startInfo.ArgumentList.Add("../AutoExtern.dll");
	startInfo.ArgumentList.Add("Library.csproj"); // Project file
	startInfo.ArgumentList.Add("NS"); // Namespace
	startInfo.ArgumentList.Add("Library.dfy.template"); // Template
	startInfo.ArgumentList.Add("CSharpModel.dfy"); // Target for CSharpModel.dfy
	startInfo.ArgumentList.Add("Library.dfy"); // Target file
	startInfo.ArgumentList.Add("Library1.cs"); // Source file
	startInfo.ArgumentList.Add("Library2.cs"); // Source file
	var dotnet = Process.Start(startInfo);

[MikaelMayer]

Oh that's very interesting. I changed the existing behavior to also adapt to this.

[cpitclaudel]

Please move this to DafnyRuntime

[cpitclaudel]

Syntax looks good to me, but I would much prefer to add a function each runtime, rather than having ad-hoc code in each compiler

[cpitclaudel]

Don't we need Javascript quoting here (instead of Dafny quoting?)

[cpitclaudel]

And more importantly, can't we pass these arguments on node's command line directly?

[MikaelMayer]

This is JavaScript quoting (ToStringLiteral is a compiler to JavaScript function)
More importantly, the problem is that passing anything in command line (e.g. node arg1 arg2) will attempt to load the file, so this is also why the javascript compiler's run method is pushing everything in the standard input.