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

New-style options are not supported in the :options attribute #3245

Closed
davidcok opened this issue Dec 22, 2022 · 0 comments · Fixed by #3252
Closed

New-style options are not supported in the :options attribute #3245

davidcok opened this issue Dec 22, 2022 · 0 comments · Fixed by #3252
Assignees
@keyboardDrummer
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@davidcok
Copy link
Collaborator

Dafny version

3.10.0+dev

Code to produce this issue

module {:options "--function-syntax:4"} M {
  ghost function f(): int { 4 }
}

Command to run and resulting output

dafny resolve test.dfy

What happened?

I expected the above to work. Instead it says

/Users/davidcok/projects/dafny/dafny/docs/HowToFAQ/tmp.dfy(1,9): Error: Option --function-syntax unrecognized or unsupported in ':options' attributes.
/Users/davidcok/projects/dafny/dafny/docs/HowToFAQ/tmp.dfy(1,9): Error: Option 4 unrecognized or unsupported in ':options' attributes.
Use /help for available options
/Users/davidcok/projects/dafny/dafny/docs/HowToFAQ/tmp.dfy(2,2): Error: a function cannot be declared 'ghost' (it is 'ghost' by default)
3 parse errors detected in /Users/davidcok/projects/dafny/dafny/docs/HowToFAQ/tmp.dfy

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

Mac
@davidcok davidcok added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Dec 22, 2022
@davidcok davidcok changed the title New-0style options are not supported in the :options attribute New-style options are not supported in the :options attribute Dec 22, 2022
@keyboardDrummer keyboardDrummer mentioned this issue Dec 22, 2022
Merged
keyboardDrummer added a commit that referenced this issue Dec 22, 2022
@keyboardDrummer
Enable new style options in the :options attribute (#3252)
48b01e2 
Fixes #3245

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
RustanLeino pushed a commit to RustanLeino/dafny that referenced this issue Dec 29, 2022
@keyboardDrummer @RustanLeino
Enable new style options in the :options attribute (dafny-lang#3252)
cb95beb 
Fixes dafny-lang#3245

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@keyboardDrummer keyboardDrummer

Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Enable new style options in the :options attribute keyboardDrummer/dafny
2 participants
@keyboardDrummer @davidcok