Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

IDE can't resolve more than once with --standard-libraries #5187

Closed
robin-aws opened this issue Mar 13, 2024 · 1 comment · Fixed by #5189
Closed

IDE can't resolve more than once with --standard-libraries #5187

robin-aws opened this issue Mar 13, 2024 · 1 comment · Fixed by #5189
Assignees
@keyboardDrummer
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label release-blocker Must be resolved before the next release

Comments

@robin-aws
Copy link
Member

Dafny version

master (not present in 4.4.0)

Code to produce this issue

(Doesn't matter)

Command to run and resulting output

1. Specify `--standard-libraries`, either with "Dafny: Language Server Launch Args" or a dfyconfig.toml project file.
2. Load any file, which should trigger successful resolution.
3. Make an edit to the file (e.g. adding a space), which should trigger resolution again.
4. At the top-left corner of file (or of the project file if using):

the referenced file DafnyStandardLibraries-notarget.dfy contains error(s) but is not owned by this project. The first error is:
a replaceable module may only be replaced once

What happened?

Likely caused by #4891 somehow (which was a good change but likely just needed to adjust how the standard library doo files are handled in the language server)

What type of operating system are you experiencing the problem on?

Mac
@robin-aws robin-aws added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label release-blocker Must be resolved before the next release labels Mar 13, 2024
@keyboardDrummer keyboardDrummer mentioned this issue Mar 13, 2024
Merged
keyboardDrummer added a commit that referenced this issue Mar 13, 2024
@keyboardDrummer
Fix bug that occurred when using resolution caching and replaceable m…
b144df2 
…odules (#5189)

Fixes #5187

### Description
Fix bug that occurred when using resolution caching in combination with
replaceable modules

### How has this been tested?
Added a language server 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>
@MikaelMayer
Copy link
Member

Oh yeah thanks for fixing that! I had this issue every day as well but did not realize it could be reproducible as other issues prevented the code from resolving anyway.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@keyboardDrummer keyboardDrummer

Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label release-blocker Must be resolved before the next release
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix bug that occurred when using resolution caching and replaceable modules keyboardDrummer/dafny
3 participants
@keyboardDrummer @MikaelMayer @robin-aws