dafny
dafny copied to clipboard
Add `dafny migrate` to support migration and reduce backwards compatibility requirements
Currently this document that contains guidelines for the development of Dafny, reads As rule, Dafny features must be marked as deprecated, including migration instructions, at least one release before they are removed.
This requirement adds unnecessary effort to developing Dafny and prevents backwards incompatible updates from being done in a single release.
The reason for the requirement is that it allows users that test their codebase against nightly releases of Dafny, to always be able to fix their codebase so it remains compatible with an upcoming Dafny. However, if we add a dafny migrate
command that is fully automatic, then users can use this in their test against the nightly Dafny, and then Dafny changes can be made that are not backwards compatible with the latest release.