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

Fix: No more spurious restart needed in the IDE #4834

Merged
merged 1 commit into from
Dec 1, 2023
Merged

Fix: No more spurious restart needed in the IDE #4834

merged 1 commit into from
Dec 1, 2023

Conversation

MikaelMayer
Copy link
Member

@MikaelMayer MikaelMayer commented Dec 1, 2023 •
edited
Loading

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.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@MikaelMayer MikaelMayer enabled auto-merge (squash) December 1, 2023 16:57
atomb
atomb reviewed Dec 1, 2023
View reviewed changes
Source/DafnyLanguageServer/Workspace/ProjectManager.cs
@@ -345,7 +346,7 @@ public class ProjectManager : IDisposable {
}

public void OpenDocument(Uri uri, bool triggerCompilation) {
Interlocked.Increment(ref openFileCount);
openFiles.TryAdd(uri, 1);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What role does the 1 serve here? Could this be a set instead of a map?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The only concurrent set I found in C# is a ConcurrentBag but it curiously does not have a method for removing a specific element.

@MikaelMayer MikaelMayer merged commit 23a083b into master Dec 1, 2023
20 checks passed
@MikaelMayer MikaelMayer deleted the fix-4833-ide-unstable branch December 1, 2023 18:14
@keyboardDrummer
Copy link
Member

Amazing, thanks :)

@MikaelMayer I'm a little concerned that we didn't get to understand how you got the stack trace:

System.ObjectDisposedException: Cannot access a disposed object.
Object name: 'EventLoopScheduler'.
   at System.Reactive.Concurrency.EventLoopScheduler.Schedule[TState](TState state, TimeSpan dueTime, Func`3 action) in /_/Rx.NET/Source/src/System.Reactive/Concurrency/EventLoopScheduler.cs:line 173
   at System.Reactive.ObserveOnObserverNew`1.Schedule() in /_/Rx.NET/Source/src/System.Reactive/Internal/ScheduledObserver.cs:line 486
   at System.Reactive.Subjects.Subject`1.OnNext(T value) in /_/Rx.NET/Source/src/System.Reactive/Subjects/Subject.cs:line 139
   at System.Reactive.Subjects.Subject`1.OnNext(T value) in /_/Rx.NET/Source/src/System.Reactive/Subjects/Subject.cs:line 139
   at Microsoft.Dafny.LanguageServer.Language.ObservableErrorReporter.AddDiagnosticForFile(DafnyDiagnostic dafnyDiagnostic, MessageSource messageSource, Uri uri) in C:\Users\mimayere\Documents\dafny\Source\DafnyLanguageServer\Language\ObservableErrorReporter.cs:line 139

But then again I wouldn't think the exception from this stack trace causes an issue, because it relates to already closed project managers, so we can leave it for now

@MikaelMayer
Copy link
Member Author

Amazing, thanks :)

@MikaelMayer I'm a little concerned that we didn't get to understand how you got the stack trace:

System.ObjectDisposedException: Cannot access a disposed object.
Object name: 'EventLoopScheduler'.
   at System.Reactive.Concurrency.EventLoopScheduler.Schedule[TState](TState state, TimeSpan dueTime, Func`3 action) in /_/Rx.NET/Source/src/System.Reactive/Concurrency/EventLoopScheduler.cs:line 173
   at System.Reactive.ObserveOnObserverNew`1.Schedule() in /_/Rx.NET/Source/src/System.Reactive/Internal/ScheduledObserver.cs:line 486
   at System.Reactive.Subjects.Subject`1.OnNext(T value) in /_/Rx.NET/Source/src/System.Reactive/Subjects/Subject.cs:line 139
   at System.Reactive.Subjects.Subject`1.OnNext(T value) in /_/Rx.NET/Source/src/System.Reactive/Subjects/Subject.cs:line 139
   at Microsoft.Dafny.LanguageServer.Language.ObservableErrorReporter.AddDiagnosticForFile(DafnyDiagnostic dafnyDiagnostic, MessageSource messageSource, Uri uri) in C:\Users\mimayere\Documents\dafny\Source\DafnyLanguageServer\Language\ObservableErrorReporter.cs:line 139

But then again I wouldn't think the exception from this stack trace causes an issue, because it relates to already closed project managers, so we can leave it for now

I got this exception while putting breakpoints on disposed method, which apparently was caught here:

  • DafnyTextDocumentHandler.cs line 102, telemetryPublisher.PublishUnhandledException(e);
    This project was closed but should not as I still had files open.

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

@atomb atomb atomb approved these changes

@keyboardDrummer keyboardDrummer Awaiting requested review from keyboardDrummer

@alex-chew alex-chew Awaiting requested review from alex-chew

@jtristan jtristan Awaiting requested review from jtristan

@robin-aws robin-aws Awaiting requested review from robin-aws

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Dafny IDE needs restarting every 3-4 minutes
3 participants
@MikaelMayer @keyboardDrummer @atomb