dafny-lang/dafny v4.7.0

Dafny 4.7.0

on GitHub

New features

• Add the option --find-project that given a Dafny file traverses up the file tree until it finds a Dafny project that includes that path. This is useful when developing a particular file and doing CLI invocations as part of your development workflow.

• Improved error reporting when verification times out or runs out of resources, so that when using --isolate-assertions, the error message points to the problematic assertion. (#5281)

• Support newtypes based on map and imap (#5175)

• To enable smoothly working with multiple projects inside a single repository, Dafny now allows using a Dafny project file as an argument to --library. When using dafny verify, Dafny ensures that any dependencies specified through a project are verified as well, unless using the flag --dont-verify-dependencies. (#5297)

• Experimental Dafny-to-Rust compiler development

  • Supports emitting code even if malformed with option --emit-uncompilable-code.
  • Supports for immutable collections and operators
    (#5081)

• Allow for plugins to add custom request handlers to the language server. (#5161)

• Deprecated the unicode-char option (#5302)

• Warn when passing a Dafny source file to --library (#5313)

• Add support for "translation records", which record the options used when translating library code.

  • --translation-record - Provides a .dtr file from a previous translation of library code. Can be specified multiple times.
  • --translation-record-output - Customizes where to write the translation record for the current translation. Defaults to the output directory.
    Providing translation records is necessary to handle options such as --outer-module that affect how code is translated.
    (#5346)

• The new decreases to expression makes it possible to write an explicit assertion equivalent to the internal check Dafny does to prove that a loop or recursive call terminates. (#5367)

• The new assigned expression makes it possible to explicitly assert that a variable, constant, out-parameter, or object field is definitely assigned. (#5501)

• Greatly reduced the size of generated code for the backends: C#, Python, GoLang and JavaScript.

• Introduce additional warnings that previously only appeared when running the dafny audit command. Two warnings are as follows:

  • Emit a warning when exporting a declaration that has requires clauses or subset type inputs
  • Emit a warning when importing a declaration that has ensures clauses or subset type outputs
    Those two can be silenced with the flag --allow-external-contracts. A third new warning occurs when using bodyless functions marked with {:extern}, and can be silenced using the option --allow-external-function.

• Enable project files to specify another project file as a base, which copies all configuration from that base file. More information can be found in the reference manual.

Bug fixes

• Fix a common memory leak that occurred when doing verification in the IDE that could easily consume gigabytes of memory.

• Fix bugs that could cause the IDE to become unresponsive

• Improve the performance of the Dafny IDE by fixing bugs in its caching code

• No longer reuse SMT solver processes between different document version when using the IDE, making the IDE verification behavior more inline to that of the CLI

• Fix bugs that caused Dafny IDE internal errors (#5355, #5543, #5548)

• Fix bugs in the Dafny IDEs code navigation and renaming features when working with definition that are not referred to.

• Fix a code navigation bug that could occur when navigating to and from module imports

• Fix a code navigation bug that could occur when navigating to and from explicit types of variables
  (#5419)

• Let the IDE no longer show diagnostics for projects for which all files have been closed (#5437)

• Fix bug that could lead to an unresponsive IDE when working with project files (#5444)

• Fix bugs in Dafny library files that could cause them not to work with certain option values, such as --function-syntax=3

• Fix a bug that prevented building Dafny libraries for Dafny projects that could verify without errors.

• Reserved module identifiers correctly escaped in GoLang (#4181)

• Fix a soundness issue that could be triggered by calling ensures fresh in the post-condition of a constructor (#4700)

• Ability to cast a datatype to its trait when overriding functions (#4823)

• Fix crash that could occur when using a constructor in a match pattern where a tuple was expected (#4860)

• No longer emit an incorrect internal error while waiting for verification message (#5209)

• More helpful error messages when read fields not mentioned in reads clauses (#5262)

• Check datatype constructors for bad type-parameter instantiations (#5278)

• Avoid name clashes with Go built-in modules (#5283)

• Invalid Python code for nested set and map comprehensions (#5287)

• Stop incorrectly emitting the error message "Dafny encountered an internal error while waiting for this symbol to verify" (#5295)

• Rename the dafny generate-tests option --coverage-report to --expected-coverage-report (#5301)

• Stop giving an incorrect warning about a missing {:axiom} clause on an opaque constant. (#5306)

• No new resolver crash when datatype update expressions are partially resolved (#5331)

• Optional pre-type won't cause a crash anymore (#5369)

• Unguarded enumeration of bound variables in set and map comprehensions (#5402)

• Reference the correct this after removing the tail call of a function or method (#5474)

• Apply name mangling to datatype names in Python more often (#5476)

• Only guard this when eliminating tail calls, if possible (#5524)

• Compiled disjunctive nested pattern matching no longer crashing (#5572)