Release Dafny 3.11.0 #3432
Merged
Release Dafny 3.11.0 #3432
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
stefan-aws
reviewed
Feb 1, 2023
stefan-aws
reviewed
Feb 1, 2023
RELEASE_NOTES.md
Outdated
| - Unless `--enforce-determinism` is used, no errors are given for arrays that are allocated without being initialized. | ||
| (https://github.com/dafny-lang/dafny/pull/3311) | ||
|
|
||
| - Enable passing a percentage value to the --cores option, to use a percentage of the total number of logical cores on the machine for verification. (https://github.com/dafny-lang/dafny/pull/3328) |
There was a problem hiding this comment.
I believe we prefer linking to the issue, and the issue itself also links to the PR. I think this can be useful when the issue contains a better description of the what than the PR. Sometimes the PR may also link to the issue to describe the what. In this case however the PR seems more informative.
stefan-aws
reviewed
Feb 1, 2023
RELEASE_NOTES.md
Outdated
|
|
||
| - Remove an infeasible assertion in the Dafny Runtime for Java (https://github.com/dafny-lang/dafny/pull/3280) | ||
|
|
||
| - Language server displays more relevant informations on hovering assertions (https://github.com/dafny-lang/dafny/pull/3281) |
There was a problem hiding this comment.
Suggested change
| - Language server displays more relevant informations on hovering assertions (https://github.com/dafny-lang/dafny/pull/3281) | |
| - Language server now displays more relevant information on hovering assertions (https://github.com/dafny-lang/dafny/pull/3281) |
stefan-aws
reviewed
Feb 1, 2023
RELEASE_NOTES.md
Outdated
|
|
||
| - Any `(==)` inferred for a type parameter of an iterator is now also inferred for the corresponding non-null iterator type. (https://github.com/dafny-lang/dafny/pull/3284) | ||
|
|
||
| - the otherwise ambiguous program fragment `export least predicate` is parsed such that `least` (or `greatest`) is the export identifier (https://github.com/dafny-lang/dafny/pull/3291) |
There was a problem hiding this comment.
Suggested change
| - the otherwise ambiguous program fragment `export least predicate` is parsed such that `least` (or `greatest`) is the export identifier (https://github.com/dafny-lang/dafny/pull/3291) | |
| - The otherwise ambiguous program fragment `export least predicate` is parsed such that `least` (or `greatest`) is the export identifier (https://github.com/dafny-lang/dafny/pull/3291) |
stefan-aws
reviewed
Feb 1, 2023
RELEASE_NOTES.md
Outdated
|
|
||
| - the otherwise ambiguous program fragment `export least predicate` is parsed such that `least` (or `greatest`) is the export identifier (https://github.com/dafny-lang/dafny/pull/3291) | ||
|
|
||
| - The parser generated bad `Token`s when invoked through `/library` (https://github.com/dafny-lang/dafny/pull/3301) |
There was a problem hiding this comment.
The other points are written in a positive manner, i.e. emphasise the current status after fixing. Can we do the same here? Something like The parser does not anymore generate bad ...?
stefan-aws
reviewed
Feb 1, 2023
RELEASE_NOTES.md
Outdated
|
|
||
| - Settings `--cores=0` will cause Dafny to use half of the available cores. (https://github.com/dafny-lang/dafny/pull/3276) | ||
|
|
||
| - Remove an infeasible assertion in the Dafny Runtime for Java (https://github.com/dafny-lang/dafny/pull/3280) |
There was a problem hiding this comment.
Suggested change
| - Remove an infeasible assertion in the Dafny Runtime for Java (https://github.com/dafny-lang/dafny/pull/3280) | |
| - Removed an infeasible assertion in the Dafny Runtime for Java (https://github.com/dafny-lang/dafny/pull/3280) |
stefan-aws
reviewed
Feb 1, 2023
RELEASE_NOTES.md
Outdated
|
|
||
| ## Bug fixes | ||
|
|
||
| - Nonexistent files passed on the CLI result in a graceful exit (https://github.com/dafny-lang/dafny/pull/2719) |
There was a problem hiding this comment.
Suggested change
| - Nonexistent files passed on the CLI result in a graceful exit (https://github.com/dafny-lang/dafny/pull/2719) | |
| - Nonexistent files passed on the CLI now result in a graceful exit (https://github.com/dafny-lang/dafny/pull/2719) |
stefan-aws
reviewed
Feb 1, 2023
stefan-aws
reviewed
Feb 1, 2023
stefan-aws
reviewed
Feb 1, 2023
stefan-aws
requested changes
Feb 1, 2023
Co-authored-by: Stefan Zetzsche <[email protected]>
davidcok
previously requested changes
Feb 1, 2023
RELEASE_NOTES.md
Outdated
Comment on lines
59
to
75
| - `dafny build` for Java now creates a library or executable jar file. | ||
| - If there is a Main method, the jar is an executable jar. So a simple A.dfy can be built as `dafny build -t:java A.dfy` | ||
| and then run as `java -jar A.jar` | ||
| - If there is no Main entry point, all the generated class files are assembled into a library jar file that can be used on a | ||
| classpath as a java library. | ||
| - In both cases, the DafnyRuntime library is included in the generated jar. | ||
| - In old and new CLIs, the default location and name of the jar file is the name of the first dfy file, with the extension changed | ||
| - In old and new CLIs, the path and name of the output jar file can be given by the --output option, with .jar added if necessary | ||
| - As before, the compilation artifacts (.java and .class files) are placed in a directory whose name is the same as the jar file | ||
| but without the .jar extension and with '-java' appended | ||
| - With the new CLI, the generated .java artifacts are deleted unless --spill-translation=true and the .class files are deleted in any case; | ||
| both kinds of files are retained with the legacy CLI for backwards compatibility. | ||
| - If any other jar files are needed to compile the dafny/java program, they must be on the CLASSPATH; | ||
| the same CLASSPATH used to compile the program is needed to run the program | ||
|
|
||
| Having a library or executable jar simplifies the user's task in figuring out how to use the built artifacts. | ||
| (https://github.com/dafny-lang/dafny/pull/3355) |
There was a problem hiding this comment.
Move this section on jar files to new features, rather than a bug (my fault for miscategorizing the news file)
stefan-aws
reviewed
Feb 1, 2023
Co-authored-by: Stefan Zetzsche <[email protected]>
Co-authored-by: Stefan Zetzsche <[email protected]>
stefan-aws
approved these changes
Feb 1, 2023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.