|
1 | 1 | # Upcoming |
2 | 2 |
|
3 | | -- feat: The IDE will show verification errors for a method immediately after that method has been verified, instead of after all methods are verified. |
4 | | -- feat: The Dafny CLI, Dafny as a library, and the C# runtime are now available on NuGet. You can install the CLI with `dotnet tool install --global Dafny`. The library is available as `DafnyPipeline` and the runtime is available as `DafnyRuntime`. |
5 | | -- feat: New syntax for quantified variables, allowing per-variable domains (`x <- C`) and ranges (`x | P(x), y | Q(x, y)`). See [the quantifier domain section](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-quantifier-domains) of the Reference Manual. |
6 | | -- fix: Various improvements to language server robustness |
7 | | -- fix: No more display of previous obsolete verification diagnostics if newer are available. (https://github.com/dafny-lang/dafny/pull/2142) |
8 | | -- feat: Live verification diagnostics for the language server (https://github.com/dafny-lang/dafny/pull/1942) |
9 | | -- fix: Prevent the language server from crashing and not responding on resolution or ghost diagnostics errors (https://github.com/dafny-lang/dafny/pull/2080) |
| 3 | +# 3.7.0 |
| 4 | + |
| 5 | +- feat: The Dafny CLI, Dafny as a library, and the C# runtime are now available on NuGet. You can install the CLI with `dotnet tool install --global Dafny`. The library is available as `DafnyPipeline` and the runtime is available as `DafnyRuntime`. (https://github.com/dafny-lang/dafny/pull/2051) |
| 6 | +- feat: New syntax for quantified variables, allowing per-variable domains (`x <- C`) and ranges (`x | P(x), y | Q(x, y)`). See [the quantifier domain section](https://dafny.org/dafny/DafnyRef/DafnyRef#sec-quantifier-domains) of the Reference Manual. (https://github.com/dafny-lang/dafny/pull/2195) |
| 7 | +- feat: The IDE will show verification errors for a method immediately after that method has been verified, instead of after all methods are verified. (https://github.com/dafny-lang/dafny/pull/2142) |
10 | 8 | - feat: Added "Resolving..." message for IDE extensions (https://github.com/dafny-lang/dafny/pull/2234) |
| 9 | +- feat: Live verification diagnostics for the language server (https://github.com/dafny-lang/dafny/pull/1942) |
11 | 10 | - fix: Correctly specify the type of the receiver parameter when translating tail-recursive member functions to C# (https://github.com/dafny-lang/dafny/pull/2205) |
12 | 11 | - fix: Added support for type parameters in automatically generated tests (https://github.com/dafny-lang/dafny/pull/2227) |
| 12 | +- fix: No more display of previous obsolete verification diagnostics if newer are available (https://github.com/dafny-lang/dafny/pull/2142) |
| 13 | +- fix: Prevent the language server from crashing and not responding on resolution or ghost diagnostics errors (https://github.com/dafny-lang/dafny/pull/2080) |
| 14 | +- fix: Various improvements to language server robustness (https://github.com/dafny-lang/dafny/pull/2254) |
| 15 | + |
13 | 16 |
|
14 | 17 | # 3.6.0 |
15 | 18 |
|
|
39 | 42 | - fix: Fix `(!new)` checks (https://github.com/dafny-lang/dafny/issues/1419) |
40 | 43 | - fix: multiset keyword no longer crashes the parser (https://github.com/dafny-lang/dafny/pull/2079) |
41 | 44 |
|
| 45 | + |
42 | 46 | # 3.5.0 |
43 | 47 |
|
44 | 48 | - feat: `continue` statements. Like Dafny's `break` statements, these come in two forms: one that uses a label to name the continue target and one that specifies the continue target by nesting level. See section [19.2](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-break-continue) of the Reference Manual. (https://github.com/dafny-lang/dafny/pull/1839) |
|
0 commit comments