no-verify should imply --allow-warnings

[kjx]

no-verify should imply--allow-warnings

cos if I say dafny run --no-verify I want to run it WITHOUT verification.
If I'm about do to that, I likely don't care about warnings, do i?

[keyboardDrummer]

If I'm about do to that, I likely don't care about warnings, do i?

I don't know. Don't you? Maybe you just want to skip the thing that is time consuming.

[kjx]

It's not that I mind seeing the warnings:
but without --allow-warnings then the thing won't run if there's even one warning...

[keyboardDrummer]

I think you could argue that the default for dafny run should be --allow-warnings=true, but I'm careful with changing options that might lead to less safe behavior, and having different defaults across different commands is tricky as well.

[kjx]

I could, but I wouldn't.

although we don't seem to have a native interpreter, dafny run means... to run the program. Usually that means: run only if verified. If it's doing that, it should certainly report the warnings.

but we've said "--no-verify" so we don't want it to be verified.
so we'd better be doing development, aka testing.
at which point, I don't see why I wouldn't want to run the program, whatever warnings I've got.