dafny 4.2.0

[ZhongRuoyu]

Created by brew bump

---

Created with brew bump-formula-pr.

release notes

## New features


The --show-snippets options is implemented for errors printed to the console (--show-snippets does not work for parse errors dafny-lang/dafny#3304)



{:error} now accepts success messages
Better hover messages when using the IDE
Harmonized language to use more "could not prove" rather than "might not hold"

(Feat: Better format in hover messages dafny-lang/dafny#3687)



Unicode representations of mathematical symbols (such as logical implies, and, and or) are no longer recognized by the parser. (Deprecate recognizing unicode versions of logical and relational symbols in the parser dafny-lang/dafny#3755)


Allow the Dafny IDE to publish 'Parsing' and 'Preparing Verification' messages to let the user better understand what they're waiting for. (Add additional IDE status messages dafny-lang/dafny#4031)


Removed obsolete options /mimicVerificationOf, /allowGlobals (Removing obsolete options /mimicVerificationOf, /allowGlobals dafny-lang/dafny#4062)


Allow the {:only} attribute to be used on members in addition to assert statements ({:only} should also work on single declarations dafny-lang/dafny#4074)


The obsolete and unsound option /allocated is removed; the behavior of dafny is locked to the case of /allocated:4. (Removing allocated option and locking in allocated=4 dafny-lang/dafny#4076)


When using the Dafny CLI, error messages of the form "the included file  contains error(s)" are no longer reported, since the actual errors for these included files are shown as well. When using the Dafny server, errors like these are still shown, since the Dafny server only shows errors for currently opened files. In addition, such errors are now also shown for files that are indirectly included by an opened file. (Pure parse function dafny-lang/dafny#4083)


When using the Dafny IDE, parsing is now cached in order to improve performance when making changes in multi-file projects. (Cache parsing dafny-lang/dafny#4085)


Errors issued in command-line mode now show source code context by default; this behavior can be disabled using the option --show-snippets:false. (--show-snippets with default true and off in tests dafny-lang/dafny#4087)


Reduced resolution time by up to 50%. Measurements on large codebases show a 35% average reduction in resolution time.


After generating Python code we run the byte-code compiler to surface possible issues earlier, if it's not subsequently run. (feat: Run Python byte-code compiler during /compile:1 dafny-lang/dafny#4155)


Improve the responsiveness of the Dafny language server when making changes while it is in the 'Resolving...' state. (Add basic support for cancellation of resolution dafny-lang/dafny#4175)


It is now possible to reveal an instance function of a class by a static reveal, without the need of an object of that class. (Dafny crashing when revealing a non-static class method from outside the class dafny-lang/dafny#4176)


Support for the --bprint option for language server arguments (Feat: Support for --bprint in language server. dafny-lang/dafny#4206)


Improve printing of real numbers to use decimal notation more often (Improve printing of real numbers dafny-lang/dafny#4235)


When translated to other languages, Dafny module names no longer have the suffix _Compile appended to them. This may cause issues with existing code from non-Dafny languages in your codebase, if that code was previously referencing modules with _Compile in the name. You can migrate either by removing the _Compile part of references in your codebase, or by using the backwards compatibility option --compile-suffix when using translate, build, or run. (Add the compile suffix option dafny-lang/dafny#4265)


Counterexample parsing now supports both the 'Arguments' and 'Predicates' polymorphism encoding in Boogie. (Various fixes for project aware mode dafny-lang/dafny#4299)


Bug fixes


Removed wrong "related position" precision when dealing with regrouped quantifiers (Wrong conjunct mentioned in "related location" under a quantifier dafny-lang/dafny#2211)


Fixed crash on an empty filename (Dafny crashes with empty command-line argument dafny-lang/dafny#3549)


Fixes crash if solver-path is not found (Crash if cannot find given solver-path dafny-lang/dafny#3572)


Avoid infinite recursion when trying to construct a potentially self-referential object during test generation ((Test Generation) Fix #3726 bug leading to stack overflow during test generation dafny-lang/dafny#3727)


Better error message when incorrect number of out parameters (Confusing message for out parameters for new users dafny-lang/dafny#3835)


Compilation of continue labels no longer crashing in Go (Go "continue" miscompilation error dafny-lang/dafny#3978)


The terminology 'opaque type' is changed to 'abstract type (for uninterpreted type declarations), to avoid ambiguity with used of the 'opaque' keyword and revealing declarations (Changing opaque type to abstract type dafny-lang/dafny#3990)


Ensures override checks have access to fuel constant equivalences (Opaque insufficiently revealing - Verification issue dafny-lang/dafny#3995)


No more crash when using constant in pattern (Case constant causing Crash? dafny-lang/dafny#4000)


Remove multiset cardinality cap in Python (fix: Remove multiset cardinality cap in Python dafny-lang/dafny#4014)


Wrong statement order in generated code for certain for-loops (fix: Correctly update wStmts dafny-lang/dafny#4015)


Making assertion explicit work for nested statements (Making assertions explicit fails for nested statements dafny-lang/dafny#4016)


Use type antecedent in Type/Allocation axioms for const fields

Don't generate injectivity axioms for export-provided types

(Make the Boogie representation of the Dafny heap use only Box dafny-lang/dafny#4020)


Added a new CLI option --warn-deprecation, which is on by default

Extraneous semicolons are now warned about by default; the warning can be disabled using --warn-deprecation:false

(Adding a new CLI option for deprecation; changing deprecation of OldSemi dafny-lang/dafny#4041)


Regression in the subset check of the function override check (Framing problem with recursive reads-clause dafny-lang/dafny#4056)


Fix function to function-by-method transformation pass in test generation that could previously lead to parsing errors ([Test Generation] Fix bug in function to function-by-method transformation dafny-lang/dafny#4067)


Modules verified in the correct order to prevent Boogie Crash (Regression: dafny run not working with include dafny-lang/dafny#4139)


In VSCode, resource units are now always displayed with 3 digit precision.

Moreover, they can now display values greater than MAX_INT without displaying a negative result.

(Resource unit's precision is not constant dafny-lang/dafny#4143)


Remove redundant code in the test generation project ([Test Generation] Remove redundant code dafny-lang/dafny#4146)


Generate type axioms in the absence of explicit constraints for newtypes (fix: Generate dummy constraint for newtypes to enable axiom generation dafny-lang/dafny#4190)


Support for opaque function handles (Opaque functions passed as arguments causes type checking errors dafny-lang/dafny#4202)


Traits with opaque functions can now be extended without errors (Extending a trait with an opaque function causes error, but only on the commandline and not on VSCode. dafny-lang/dafny#4205)


Disabled --show-snippets CLI option, which is otherwise on by default, during test generation

Test generation modifies Boogie AST resulting from Dafny, and is, therefore, incompatible with --show-snippets

(Disable ShowSnippets during Test Generation dafny-lang/dafny#4216)


Select proper division for real-based newtypes (fix: division for newtypes in JS and PY dafny-lang/dafny#4234)


Formatting in the IDE consistent again with the CLI (Format lemma in the IDE dafny-lang/dafny#4269)


Fixes invalid declaration errors when verifying directly from Dafny using /typeEncoding:m. (fix: Invalid declaration errors with /typeEncoding:m dafny-lang/dafny#4275)


Make gutter icons more robust to document changes (Fix 4287 gutter highlight before project pr dafny-lang/dafny#4308)

[github-actions]

🤖 An automated task has requested bottles to be published to this PR.