Don't expand stdin.dfy as a path

[jaylorch]

Fixes #1109

[robin-aws]

Personally I wasn't even aware this was possible before! :) For the record I'm definitely not a fan of using such a magic file name, and would prefer an explicit switch like /stdin instead. Assuming this broke between 2.3 and 3.0, now would be the time to fix that since the major version bump allows the breaking change.

Regardless of what we decide there, we also badly need a regression test for this.

[davidcok]

Or use what other command-line tools do, namely ‘-‘ for stdin (e.g. diff)

…

On Feb 6, 2021, at 11:30 AM, Robin Salkeld ***@***.***> wrote: @robin-aws requested changes on this pull request. Personally I wasn't even aware this was possible before! :) For the record I'm definitely not a fan of using such a magic file name, and would prefer an explicit switch like /stdin instead. Assuming this broke between 2.3 and 3.0, now would be the time to fix that since the major version bump allows the breaking change. Regardless of what we decide there, we also badly need a regression test for this. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#1110 (review)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABITDQAMXTSPUMYYPJCXEBLS5VVCTANCNFSM4XFZWPQQ>.

[robin-aws]

I almost suggested - as well. I slightly prefer the switch since it's more "portable": - is more of a *nix system convention AFAIK, and I imagine it would feel a little strange on Windows.

[davidcok]

I could go with -stdin /stdin and - as equivalent alternatives

…

On Feb 6, 2021, at 12:07 PM, Robin Salkeld ***@***.***> wrote: I almost suggested - as well. I slightly prefer the switch since it's more "portable": - is more of a *nix system convention AFAIK, and I imagine it would feel a little strange on Windows. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#1110 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABITDQAQ5G3F72OSMWZ2NHLS5VZO7ANCNFSM4XFZWPQQ>.

[jaylorch]

I agree that the magic name stdin.dfy is a bit weird as the way to do read from stdin. I wasn't even aware of this Dafny feature until, when I was updating rise4fun.com/dafny to use Dafny 3.0.0, I discovered it relied on it. And I definitely agree that a regression test is needed.

[jaylorch]

I want to use a different branch for this, so I'm closing this pull request.