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

Dafny IDE needs restarting every 3-4 minutes #4833

Closed
MikaelMayer opened this issue Dec 1, 2023 · 0 comments · Fixed by #4834
Closed

Dafny IDE needs restarting every 3-4 minutes #4833

MikaelMayer opened this issue Dec 1, 2023 · 0 comments · Fixed by #4834
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@MikaelMayer
Copy link
Member

Dafny version

latest-nightly

Code to produce this issue

Just wait. After a few minutes, nothing works.

Command to run and resulting output

No response

What happened?

Here is more debugging information:

  • It seems that the language server receives only one notification about the current file open, even if there are other files open. So the number of open files for the language server is 1
  • After 3-4 minutes, VSCode sends to the language server a notification of closed files for the files that the language server did not even thought were open.
  • Since the language server keeps track of a number of files open, it decrements that number, gets to 0 and dispose the compilation, which prevents anything else from happening.

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

Windows
@MikaelMayer MikaelMayer added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Dec 1, 2023
@MikaelMayer MikaelMayer mentioned this issue Dec 1, 2023
Merged
MikaelMayer added a commit that referenced this issue Dec 1, 2023
@MikaelMayer
Fix: No more spurious restart needed in the IDE (#4834)
23a083b 
Fixes #4833 

### Description
I replaced the openFileCount by openFiles so that closing a document,
even if unexpected like VSCode does randomly, won't trigger the
Compilation object to be disposed, which crashes the IDE every 3-4
minutes on projects with multiple files open.

### How has this been tested?
I have been enjoying the IDE for 20 minutes straight without restarting
it. It's a fantastic experience. I'm going to turn on "verification on
change" again.

<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
Assignees
No one assigned
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix: No more spurious restart needed in the IDE dafny-lang/dafny
1 participant
@MikaelMayer