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.

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

Change default values of CLI options for Dafny 4.0 #2548

Closed
robin-aws opened this issue Aug 4, 2022 · 3 comments
Closed

Change default values of CLI options for Dafny 4.0 #2548

robin-aws opened this issue Aug 4, 2022 · 3 comments
Assignees
Labels
breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) part: documentation Dafny's reference manual, tutorial, and other materials
Milestone

Comments

@robin-aws
Copy link
Member

robin-aws commented Aug 4, 2022

This is the primary proposed breaking change for Dafny 4.0. The changes are currently planned to be (with the PRs that add/affect the new functionality):

This will also involve documentation changes, not just on these options but also to have examples in the reference manual and other places to use the new defaults (especially to remove function method!)

#3466 has the first three changes applied and adjusts all tests to pass, but the others will need similar tweaks (although touching far fewer files). The plan is to merge that into a main-4.x branch once it's approved, and we can incrementally apply other 4.x-only changes like these onto that branch, while preferring any other changes that should be in both 3.Last and 4.0 go into master.

As new changes are merged to master that imply these kinds of changes, please add to the list above, and preferably drop a comment for visibility!

@robin-aws robin-aws added part: documentation Dafny's reference manual, tutorial, and other materials breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) labels Aug 4, 2022
@robin-aws robin-aws added this to the Dafny 4.0 milestone Aug 4, 2022
@atomb
Copy link
Member

atomb commented Aug 5, 2022

Do you mean \quantifierSyntax:3 -> \quantifierSyntax:4 above?

@robin-aws
Copy link
Member Author

Do you mean \quantifierSyntax:3 -> \quantifierSyntax:4 above?

Yup :) Thanks! Fixed.

@robin-aws robin-aws self-assigned this Feb 21, 2023
robin-aws added a commit that referenced this issue Feb 23, 2023
…har to Dafny 4.0 defaults (#3623)

Partially addresses #2548 (more default switches still coming).

CI is not fully enabled on the target branch yet.

Co-authored-by: davidcok <[email protected]>
Co-authored-by: Robin Salkeld <[email protected]>
@RustanLeino
Copy link
Collaborator

The /allocated:3 -> /allocated:4 change is in PR #3637 against the main-4.0 branch.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability) part: documentation Dafny's reference manual, tutorial, and other materials
Projects
None yet
Development

No branches or pull requests

3 participants