dafny 4.11.0

[botantony]

Created by brew bump

---

Created with brew bump-formula-pr.

release notes

 ## New features


Stabilize verifications by automatically computing triggers for the quantified proof obligations associated with :| constructs.

Manually specified triggers and warning-suppressing attributes are also supported (and mentioned in warning messages, as for other quantifiers and comprehensions).

Enhance witness guessing for the proof obligation associated for :| assignments.

(feat: Compute triggers for such-that operations dafny-lang/dafny#6023)


Four new Dafny standard libraries:

Std.Actions - utilities for abstract imperative actions, including enumerating and streaming values
Std.Frames - utilities related to working with dynamic framing, often related to reads and modifies clauses
Std.Ordinal - operations and properties of the ORDINAL type
Std.Termination - a datatype for representing Dafny decreases clauses and extensions

(feat: Actions, Frames, Termination, and Ordinal standard libraries dafny-lang/dafny#6074)



Support using --standard-libraries with --enforce-determinism. Removed Std.Collections.Seq.SetToSeq since it was slow and not compatible with this mode. (https://github.com/dafny-lang/daf

ny/pull/6137)


With --standard-libraries you can now read an UTF-8 text files from the disk using Std.FileIO.ReadUTF8FromFile(path: string): Result<string, string>.

To write some content to the disk, use Std.FileIO.WriteUTF8ToFile(path: string, content: string): Outcome<string>.

Standard library breaking change: All UnicodeEncodingForm versions of FromUTF8Checked, FromUTF16Checked and DecodeCodeUnitSequenceChecked now return a Result instead of an Option  so that the error message is clearer. Migration is easy: Use .ToOption() if you really prefer an option. Affected refining modules: Utf8EncodingForm and Utf16EncodingForm

(Feat: Std.FileIO.ReadFile and WriteFile dafny-lang/dafny#6198)


The Dafny standard libraries now include a powerful parser combinators framework, available through Std.Parsers.StringBuilders.
Key Features

Guaranteed Termination: All parsers, including those built with recursive combinators, are proven to terminate
Mutual Recursion Support: Build complex parsers that can reference each other (demonstrated in the Polynomial example)
Rich Error Reporting: Failed parsing attempts combine their error messages to provide meaningful feedback
Developer-Friendly Tools: Built-in debugging utilities for inspecting parser inputs and outputs
Memory-Efficient Recursion: Advanced implementations avoid stack overflow in recursive parsers
Elegant DSL: Compact, datatype-based combinators designed for readability and composition
Flexible Backtracking: Optional backtracking available through .??() (DSL) or ?(...) (standard syntax)
Comprehensive Toolkit: Rich set of combinators including lookahead, negation, folding, and binding operations
The library includes several practical examples, including JSON and SMT parsers, each implemented in about 50 lines of code.

(Reinstate "Feat: Verified and easy-to-use parser combinators (#6143)" dafny-lang/dafny#6243)



Dafny classes and traits can now redeclare methods defined by traits they inherit from. (Allow redeclaring trait methods dafny-lang/dafny#6280)


Real literals now support scientific notation using lowercase e to denote the exponent (like 1.23e5 for 123000.0 or 5e-2 for 0.05). Real literals also support convenient trailing-dot

shorthand (like 1. for 1.0) and leading-dot shorthand (like .5 for 0.5 or .5e2 for 50.0). Note that explicit + signs in exponents are not supported; use 5e2 instead of 5e+2. (ht

tps://github.com/dafny-lang/dafny/pull/6286)


Bug fixes


Fix soundness issue that could occur when using an opaque block and old or fresh in its ensures clause (Opaque blocks allow proving false dafny-lang/dafny#6060)


Correctly display project files errors when using build command (Error does not mention faulty dfyconfig.toml file dafny-lang/dafny#6107)


Fix crash that could occur when a forall statement was used inside a match case (fix: Fix crash when a simple forall statement was placed inside a match dafny-lang/dafny#6121)


Fix a case where a forall statement would cause Dafny to crash (Unable to cast object of type 'Microsoft.Dafny.BinaryExpr' to type 'Microsoft.Dafny.QuantifierExpr' dafny-lang/dafny#6129)


Fix @VerifyOnly and migrated the new code to use it (@VerifyOnly not working dafny-lang/dafny#6146)


Java lambdas now accepting boxing/unboxing (Java equality between chars fails if one is unboxed. dafny-lang/dafny#6149)


Fix crash in resolution of structural-inclusion greater-than operator (fix: Fix crash in resolution of structural-inclusion greater-than operator dafny-lang/dafny#6155)


Generate alloc consequence axiom only for functions that read the heap (fixes unsoundness) (Soundness issue with constructors? dafny-lang/dafny#6164)


Made the language server compliant with the LSP protocol so that it can be used with other editors, such as Helix (Non-compliant LSP message prevents wider editor support dafny-lang/dafny#6172)


No more compilation issue when using bitvector shifts in Rust with the new resolver (Bitvector issue with --type-system-refresh dafny-lang/dafny#6196)


Fix handling of opaque blocks in the Dafny IDE (Opaque blocks not working in VSCode extension dafny-lang/dafny#6203)


JSON serialization now properly encodes unicode characters with 0 pre-pend instead of space-append.

Also, string literals ending with escaped characters are now supported as well.

(Standard Library serialization and deserialization error dafny-lang/dafny#6227)


Fail more gracefully when reusing names (fix: Fail more gracefully when reusing names dafny-lang/dafny#6262)


Escape user string literals in error messages (fix: Escape string literals in error messages dafny-lang/dafny#6273)


Compilation of type conversion from a newtype-based on char to int (fix: C# compilation of newtype-char to int conversion dafny-lang/dafny#6296)


Fix LSP bug that cause IDE exceptions during invalid parse states (Fix LSP bug that returned a invalid range for documentSymbol dafny-lang/dafny#6299)


Fix two resolver crashes involving datatypes and traits (Fixes resolver crashes related to datatypes and traits dafny-lang/dafny#6321)

View the full release notes at https://github.com/dafny-lang/dafny/releases/tag/v4.11.0.

---

[botantony]

requires deprecated gradle 7 to build

[cho-m]

requires deprecated gradle 7 to build

Upstream uses gradle 8 - https://github.com/dafny-lang/dafny/blob/v4.11.0/Source/DafnyRuntime/DafnyRuntimeJava/gradle/wrapper/gradle-wrapper.properties

[github-actions]

@daeho-ro has requested bottles to be published to this PR.

Caution

Please do not push to this PR branch before the bottle commits have been pushed, as this results in a state that is difficult to recover from. If you need to resolve a merge conflict, please use a merge commit. Do not force-push to this PR branch.