Dafny 3.12.0

[alex-chew]

New features

• Implements error detail information and quick fixes:

  • An error catalog with error message explanations is at https://dafny.org/latest/HowToFAQ/Errors
  • In VSCode, when hovering over an error, the hover information shows additional explanation and
    an error id, which is also a link to the error explanation page
  • Where a Quick Fix is available, the Quick Fix link is active
    (Implementing errorIDs #3299)

• opaque is now a modifier, though still allowed, but deprecated as an identifier; it replaces the {:opaque} attribute (Deprecating :opaque as an attribute, introducing it as a modifier #3462)

• The value of the --library option is allowed to be a comma-separated list of files or folders (Issue#3513 -- allow value of library option to be list #3540)

Bug fixes

• Exclude verifier's type information for “new object” allocations (fix: Exclude type information for “new object” allocations #3450)

• The Dafny scanner no longer treats lines beginning with # (even those in strings) as pragmas. (The Dafny scanner no longer recognizes lines beginning with # as pragmas #3452)

• The attribute :heapQUantifier is deprecated and will be removed in the future. (Deprecating :heapQuantifier; small documentation tasks #3456)

• Fixed race conditions in the language server that made gutter icons behave abnormally (Flacky test because of race condition #3502)

• No more crash when hovering assertions that reference code written in other smaller files (CI tests for issue 1435 #3585)

---

This discussion was created from the release Dafny 3.12.0.