Dafny 4.1.0

[fabiomadge]

New features

• Added support for .toml based Dafny project files. For now the project file only allows specifying which Dafny files to include and exclude, and what options to use.
  The CLI commands that take Dafny files as input, such as build, run, translate, will now also accept Dafny project files.
  When using an IDE based on dafny server, such as the Dafny VSCode extension, the IDE will look for a Dafny project file by traversing up the file tree from the currently opened file, until it finds it dfyconfig.toml. The project file will override options specified in the IDE.
  (Enable configuring Dafny options through a project file #2907)

• Recognize the {:only} attribute on assert statements to temporarily transform other assertions into assumptions ([Feature request]: {:only} on assertions #3095)

• Exposes the --output and --spill-translation options for the dafny test command (dafny test and --output option #3612)

• The dafny audit command now reports instances of the {:concurrent} attribute, intended to flag code that is intended, but can't be proven, to be safe for use in a concurrent setting. (Add auditor support for the :concurrent attribute #3660)

• Added option --no-verify for language server (feat: no-verify for language server #3732)

• • Added .GetDocstring(DafnyOptions) to every AST node
  • Plugin support for custom Docstring formatter,
  • Activatable plugin to support a subset of Javadoc through --javadoclike-docstring-plugin
  • Support for displaying docstring in VSCode
    (Feat: Documenting Dafny Entities (Adding Docstring) #3756)

• Documentation of the syntax for docstrings added to the reference manual (Documentation on docstrings #3773)

• Labelled assertions and requires in functions (Support for labelled assertions and requires in functions #3804)

• API support for obtaining the Dafny expression that is being checked by each assertion (Feat: Support for expressions in proof obligation descriptions #3888)

• Added a "Dafny Library" backend, which produces self-contained, pre-verified .doo files ideal for distributing shared libraries.
  .doo files are produced with commands of the form dafny build -t:lib ....
  (feat: Build artifacts ("library" backend and .doo files) #3913)

• Semantic interpretation of dots in names for {:extern} modules when compiling to Python (feat: Semantics for dots in {:extern} module names in Python #3919)

• Code actions in editor to explicit failing assertions.
  In VSCode, place the cursor on a failing assertion that support being made explicit and either

  • Position the caret on a failing assertion, press CTRL+; and then ENTER
  • Hover over the failing division by zero, click "quick fix", press ENTER
    Both scenarios will explicit the failing assertion.
    If you don't see a quick fix, it means that the assertion cannot be automatically made explicit for now.

  Here is a initial list of assertions that can now be made explicit:

  • Division by zero
  • "out of bound" on sequences index, sequence slices, or array index
  • "Not in domain" on maps
  • "Could not prove unicity" of var x :| ... statement
  • "Could not prove existence" of var x :| ... statement
    (Feat: 10 more implicit assertions made explicit #3940)

Bug fixes

• dafny test accepts a --methods-to-test option whose value is a regular expression selecting which tests to include in the test run (--tests option for dafny test #3221)

• The deprecated attributes :dllimport, :handle, and :heapQuantifier are no longer recognized. (Post 4.0, remove all code associated with :handle and :dllimport #3398)

• While using dafny translate --target=java, the --include-sources option works as intended, while before it had no affect. (dafny build with extern declarations #3611)

• Tested support for paths with spaces in them (Space in the current directory crashes "dafny run" #3683)

• Crash related to the override check for generic functions (fix: Crash related to the override check for generic functions #3692)

• Opaque functions guaranteed to be opaque until revealed (opaque function called within lambda is not opaque! #3719)

• Support for Corretto tests (dafny build/test/run fails on Java + Windows #3731)

• Right shift on native byte has the same consistent semantics even in Java (Incorrect right shift operation for byte in Java #3734)

• • Main and {:test} methods may now be in the same program (Cannot put tests and Main in same file #3744)

• The formatter now produces the same output whether invoked on the command-line or from VSCode (Dafny formatter produces incorrect indentation with match statement and :| #3790)

• The --solver-log option is now hidden from help unless --help-internal is used. (Hide --solver-log option #3798)

• Highlight "inconclusive" as errors in the gutter icons (Ignored or could not reach conclusion not highlighted in gutter #3821)

• Docstring for functions with ensures (Missing docstring in predicate #3840)

• Prevent a compiler crash that could occur when a datatype constructor was defined that has multiple parameters with the same name. (Dictionary Error With Object Update Syntax #3860)

• Improved rules for nameonly parameters and parameter default-value expressions (Improve rules for nameonly/positional/nameless and required/optional … #3864)

• Fixes several compilation issues, mostly related to subset types defined by one of its type parameter (fix: Compilation of subset types constrained by type parameter #3893)

• Explicitly define inequality of multisets in Python for better backwards compatibility (fix: Explicitly define inequality of multisets in Python for better backwards compatibility #3904)

• Format for comprehension expressions (Formater should have a continuation indent  #3912)

• Formatting for parameter default values (Formatter bug #3944)

• Formatting issue in forall statement range (Formatting issue in forall statements #3960)

• Select alternative default calc operator only if it doesn't clash with given step operators (fix: Select alternative default calc operator more carefully #3963)

---

This discussion was created from the release Dafny 4.1.0.