dafny 4.1.0

[tchajed]

Created with brew bump-formula-pr.

release notes

## 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 dafny-lang/dafny#2907)


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


Exposes the --output and --spill-translation options for the dafny test command (dafny test and --output option dafny-lang/dafny#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 dafny-lang/dafny#3660)


Added option --no-verify for language server (feat: no-verify for language server dafny-lang/dafny#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) dafny-lang/dafny#3756)



Documentation of the syntax for docstrings added to the reference manual (Documentation on docstrings dafny-lang/dafny#3773)


Labelled assertions and requires in functions (Support for labelled assertions and requires in functions dafny-lang/dafny#3804)


API support for obtaining the Dafny expression that is being checked by each assertion (Feat: Support for expressions in proof obligation descriptions dafny-lang/dafny#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) dafny-lang/dafny#3913)


Semantic interpretation of dots in names for {:extern} modules when compiling to Python (feat: Semantics for dots in {:extern} module names in Python dafny-lang/dafny#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 dafny-lang/dafny#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 dafny-lang/dafny#3221)


The deprecated attributes :dllimport, :handle, and :heapQuantifier are no longer recognized. (Post 4.0, remove all code associated with :handle and :dllimport dafny-lang/dafny#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 dafny-lang/dafny#3611)


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


Crash related to the override check for generic functions (fix: Crash related to the override check for generic functions dafny-lang/dafny#3692)


Opaque functions guaranteed to be opaque until revealed (opaque function called within lambda is not opaque! dafny-lang/dafny#3719)


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


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



Main and {:test} methods may now be in the same program (Cannot put tests and Main in same file dafny-lang/dafny#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 :| dafny-lang/dafny#3790)


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


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


Docstring for functions with ensures (Missing docstring in predicate dafny-lang/dafny#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 dafny-lang/dafny#3860)


Improved rules for nameonly parameters and parameter default-value expressions (Improve rules for nameonly/positional/nameless and required/optional … dafny-lang/dafny#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 dafny-lang/dafny#3893)


Explicitly define inequality of multisets in Python for better backwards compatibility (fix: Explicitly define inequality of multisets in Python for better backwards compatibility dafny-lang/dafny#3904)


Format for comprehension expressions (Formater should have a continuation indent  dafny-lang/dafny#3912)


Formatting for parameter default values (Formatter bug dafny-lang/dafny#3944)


Formatting issue in forall statement range (Formatting issue in forall statements dafny-lang/dafny#3960)


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

[tchajed]

I'm trying a couple fixes to this formula:

• I don't believe Dafny requires dotnet 6, so let's try bumping it to dotnet 7 (the latest). I opened Does Dafny support dotnet 7? dafny-lang/dafny#3992 to get confirmation on this.
• There shouldn't be any real dependence on Java unless you're compiling from Dafny to Java. At best this is an optional dependency. It could also be bumped to openjdk@19, and that formula would need to be added to Homebrew.

If these fixes shouldn't be mixed in with a version bump I'm happy to open a separate PR (we should be able to do the version bump first).

[tchajed]

Looks like these changes fail in CI (though they seemed to work locally) so I've reverted them.

Changes made

[github-actions]

🤖 An automated task has requested creation of a replacement PR.

Replacement PR dispatched

[github-actions]

✅ Replacement PR created at #130730.