See diff of cache resolution without refactoring changing #2
Conversation
This file contains hidden or 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
…ny into removeCompileModules
Refactorings that are part of the resolution caching PR. If commits are reviewed separately it shouldn't be much work since this is almost purely renames and automatic code moves. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Adjusts the tests so that if --show-snippets is on by default, the tests do not fail. Also sets --show-snippets on by default. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: davidcok <[email protected]>
### Changes In the language server, do not run translation if there are resolution errors ### Testing Add XUnit test <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
…y-lang#4172) Fixes dafny-lang#3949 <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Remy Willems <[email protected]>
Fixes dafny-lang#4176 by making generated reveal lemmas be static. <!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md --> <!-- Is this a bug fix? Remember to include a test in Test/git-issues/ --> <!-- Is this a bug fix for an issue introduced in the latest release? Mention this in the PR details and ensure a patch release is considered --> <!-- Does this PR need tests? Add them to `Test/` or to `Source/*.Test/…` and run them with `dotnet test` --> <!-- Are you moving a large amount of code? Read CONTRIBUTING.md to learn how to do that while maintaining git history --> <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Fixes dafny-lang#3686 - Added the trace of proof even in successes - Replaced intermediate "Could not prove" and "Did prove" by "Inside " to indicate this is just a trace - Use backticks to indicate quoted code - Better error message instead of "error is impossible: This is the precondition that might not hold" - First-class support of {:error} in hover messages. - BONUS: Not described in the issue: Hover support for `{:error}` in failed postconditions. Acts as a precursor to dafny-lang#3324 by harmonizing the change made in boogie "might not hold" => "could not be proved" in preconditions and postconditions ``` before: function precondition might not hold after: function precondition could not be proved before: the calculation step between the previous line and this line might not hold after: the calculation step between the previous line and this line could not be proved before: This postcondition might not hold on a return path. after: this postcondition could not be proved on a return path ``` The screenshots of the issue are now fixed w.r.t. the described errors.   With support for `{:error}` in postconditions  <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
…to cacheResolution
This PR fixes dafny-lang#4202 I added the corresponding test. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
…#4169) This PR fixes dafny-lang#4016 I added the corresponding test. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
keyboardDrummer
added a commit
that referenced
this pull request
Mar 6, 2025
### What was changed? Change the error reporting related to refinement, so it behaves more like the existing reporting, and the IDE and CLI are now consistent in how they report refinement related diagnostics. In particular, the IDE can now jump to both the refining and refined symbol. Change #1: instead of `[<RefiningModuleName>]`, use a related location to report refinement related issues. ``` - Termination.dfy[TerminationRefinement1](441,5): Error: decreases clause might not decrease + Termination.dfy(441,5): Error: decreases clause might not decrease +Termination.dfy(446,7): Related location: refining module ``` Change #2: slighly changed the wording when overriding skeleton propositions: ``` Refinement.dfy(198,6): Error: assertion might not hold -Refinement.dfy[IncorrectConcrete](122,18): Related location: this proposition could not be proved +Refinement.dfy(122,18): Related location: refined proposition ``` ### How has this been tested? - Updated existing tests <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
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.