Dafny 4.2.0

[keyboardDrummer]

New features

• The --show-snippets options is implemented for errors printed to the console (--show-snippets does not work for parse errors #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 #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 #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 #4031)

• Removed obsolete options /mimicVerificationOf, /allowGlobals (Removing obsolete options /mimicVerificationOf, /allowGlobals #4062)

• Allow the {:only} attribute to be used on members in addition to assert statements ({:only} should also work on single declarations #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 #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 #4083)

• When using the Dafny IDE, parsing is now cached in order to improve performance when making changes in multi-file projects. (Cache parsing #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 #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 #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 #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 #4176)

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

• Improve printing of real numbers to use decimal notation more often (Improve printing of real numbers #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 #4265)

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

Bug fixes

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

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

• Fixes crash if solver-path is not found (Crash if cannot find given solver-path #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 #3727)

• Better error message when incorrect number of out parameters (Confusing message for out parameters for new users #3835)

• Compilation of continue labels no longer crashing in Go (Go "continue" miscompilation error #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 #3990)

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

• No more crash when using constant in pattern (Case constant causing Crash? #4000)

• Remove multiset cardinality cap in Python (fix: Remove multiset cardinality cap in Python #4014)

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

• Making assertion explicit work for nested statements (Making assertions explicit fails for nested statements #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 #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 #4041)

• Regression in the subset check of the function override check (Framing problem with recursive reads-clause #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 #4067)

• Modules verified in the correct order to prevent Boogie Crash (Regression: dafny run not working with include #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 #4143)

• Remove redundant code in the test generation project ([Test Generation] Remove redundant code #4146)

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

• Support for opaque function handles (Opaque functions passed as arguments causes type checking errors #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. #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 #4216)

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

• Formatting in the IDE consistent again with the CLI (Format lemma in the IDE #4269)

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

• Make gutter icons more robust to document changes (Fix 4287 gutter highlight before project pr #4308)

---

This discussion was created from the release Dafny 4.2.0.