Dafny 4.7.0

[atomb]

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. (Out of resources error reporting #5281)

• Support newtypes based on map and imap (feat: Add newtype support for 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. (Allow using project files together with --library #5297)

• Experimental Dafny-to-Rust compiler development

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

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

• Deprecated the unicode-char option (Deprecate unicode-char #5302)

• Warn when passing a Dafny source file to --library (Warn when using non doo file as a 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.
    (feat: Translation records #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. (Implement decreases to expressions #5367)

• The new assigned expression makes it possible to explicitly assert that a variable, constant, out-parameter, or object field is definitely assigned. (feat: Implement assigned(e) expression #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 (IDE throws exception related to code actions #5355, Prevent LSP server from crashing on code actions #5543, Fix null ref in covered tokens #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
  (Improve code navigation #5419)

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

• Fix bug that could lead to an unresponsive IDE when working with project files (Fix bugs 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 (Reserved name in go not escaped #4181)

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

• Ability to cast a datatype to its trait when overriding functions (New type system refresh issue #4823)

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

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

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

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

• Avoid name clashes with Go built-in modules (Reserved keywords in Go in need of escape #5283)

• Invalid Python code for nested set and map comprehensions (fix: 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" (Error: 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 (Rename --coverage-report to --expected-coverage-report #5301)

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

• No new resolver crash when datatype update expressions are partially resolved (Internal Error: System.NullReferenceException #5331)

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

• Unguarded enumeration of bound variables in set and map comprehensions (fix: 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 (fix: 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 (fix: Apply name mangling to datatype names in Python more often #5476)

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

• Compiled disjunctive nested pattern matching no longer crashing (Disjunctive pattern matching not correctly handled #5572)

---

This discussion was created from the release Dafny 4.7.0.