dafny run file.dfy --include file.cs does not raise errors

[MikaelMayer]

Dafny version

latest-nightly

Code to produce this issue

Have a file.dfy and a file.cs

Command to run and resulting output

dafny run file.dfy --include file.cs does not raise errors

What happened?

--include is parsed as an argument to main. It should be detected that it's an option and required that it's after a --

What type of operating system are you experiencing the problem on?

Windows

[codyroux]

+1

[robin-aws]

--include isn't a Dafny CLI option though, you want --input :)

[codyroux]

Indeed, but Dafny does not say this, it simply does not include the C# file. Lost a good hour to this.

[keyboardDrummer]

Indeed, but Dafny does not say this, it simply does not include the C# file. Lost a good hour to this.

How could it detect that you don't mean --include to mean an option of the user program?

That would mean we'd have to change how dafny run accept user program arguments, to something more explicit, like --arguments "x y z"

[codyroux]

Git just does git command --flags -- user_input possibly including flags. Would that be an option? (note the space after the --)

[keyboardDrummer]

Git just does git command --flags -- user_input possibly including flags. Would that be an option? (note the space after the --)

Can you provide a concrete example?

I'm guessing git treats -- the same as Dafny does, because we're following the POSIX standard and I'd be surprised if git does not. https://www.gnu.org/software/libc/manual/html_node/Argument-Syntax.html

[MikaelMayer]

Is the documentation wrong, or did something change? Either way, we documented something untested:

dafny run A.dfy --no-verify – builds the Main program in A.dfy using the --no-verify option, and then runs the program with no command-line arguments
dafny run A.dfy -- --no-verify – builds the Main program in A.dfy (not using the --no-verify option), and then runs the program with one command-line argument, namely --no-verify

https://dafny.org/latest/DafnyRef/DafnyRef#sec-dafny-run

Either way, with this issue raised and my awareness being more acute, my preference would be that any thing not starting with "-" after the file name be recognized as an argument for the main function, and anything starting with "-", if not after a "--", be considered as an option for Dafny and, if not recognized, says something like "If you want to pass this as an argument to the Dafny program, resolve the ambiguity by adding the special argument "--" before it"

[codyroux]

Here is git's behavior:

git status foo.dfy --some-bogus-flag bar.dfy

raises an error (unrecognized flag).

git status foo.dfy -- --some-bogus-flag bar.dfy

does not. I'd like identical behavior.

I think that's what POSIX says? I'm not sure.

[keyboardDrummer]

Here is git's behavior:

git status foo.dfy --some-bogus-flag bar.dfy

raises an error (unrecognized flag).

git status foo.dfy -- --some-bogus-flag bar.dfy

does not. I'd like identical behavior.

I think that's what POSIX says? I'm not sure.

POSIX convention says that -- causes anything after it to always be an argument instead of an option. I don't see how that explains the behavior above. It seems git status rejects arguments as input files if they start with --, but only if that happens before a -- token, which would not follow the POSIX convention.

I don't think you can follow the POSIX convention and get the behavior you want: that --some-invalid-option gives an error if it occurs before --, and is accepted as an argument otherwise.

If we want to stay within the convention, the only option I see is to require the user program inputs to be passed using an option, as I described before, so you would have to write --program-argument=....

Alternatively, we would deviate from the POSIX convention. A small deviation we could do is emit a warning on stderr when you have a --<something> value that is not a Dafny option which occurs before a --. Made a PR here: #5120