dafny icon indicating copy to clipboard operation
dafny copied to clipboard

Add `dafny migrate` to support migration and reduce backwards compatibility requirements

Open keyboardDrummer opened this issue 2 months ago • 1 comments

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.

keyboardDrummer avatar May 06 '24 10:05 keyboardDrummer