Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Dafny 4.0 suggestion: Compiled Dafny programs should accept command-line arguments, return an exit code #1116

Closed
davidcok opened this issue Feb 12, 2021 · 3 comments · Fixed by #2594
Closed

Dafny 4.0 suggestion: Compiled Dafny programs should accept command-line arguments, return an exit code #1116

davidcok opened this issue Feb 12, 2021 · 3 comments · Fixed by #2594
Assignees
@MikaelMayer
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny

Comments

@davidcok
Copy link
Collaborator

Compiled Dafny programs should accept command-line arguments. To do so, the allowed Main methods should be permitted to take a string[] argument.
@keyboardDrummer keyboardDrummer added the kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny label Jul 19, 2021
@robin-aws
Copy link
Member

While we're at it let's support returning an exit code as well.

@davidcok davidcok mentioned this issue Jul 15, 2022
Closed
@davidcok davidcok changed the title Compiled Dafny programs should accept command-line arguments Dafny 4.0 suggestion: Compiled Dafny programs should accept command-line arguments Jul 18, 2022
@robin-aws robin-aws changed the title Dafny 4.0 suggestion: Compiled Dafny programs should accept command-line arguments Dafny 4.0 suggestion: Compiled Dafny programs should accept command-line arguments, return an exit code Jul 28, 2022
@robin-aws robin-aws mentioned this issue Jul 28, 2022
Closed
@cpitclaudel
Copy link
Member

Note for future implementers: string[] would be a reasonable choice with the current definition of the type string, but we might need to use a different type when we switch to unicode strings.

@MikaelMayer MikaelMayer self-assigned this Aug 9, 2022
@robin-aws
Copy link
Member

I'd say string[] (or even better seq<string> :) should definitely be the default choice, but we may want support for some kind of OsString a.l.a. Rust to handle edge cases of OS-native strings that aren't valid UTF code unit sequences.

Also I don't see a breaking change so I don't think this is relevant for Dafny 4.0.

@MikaelMayer MikaelMayer mentioned this issue Aug 16, 2022
Merged
@robin-aws robin-aws mentioned this issue Sep 6, 2022
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@MikaelMayer MikaelMayer

Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

feat: Dafny Main method to accept optional seq<string> argument dafny-lang/dafny
5 participants
@keyboardDrummer @MikaelMayer @davidcok @cpitclaudel @robin-aws