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.

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

CompleteOnNothingAtLineStartReturnsEmptyList: Microsoft.Dafny.Compilation[0] System.ObjectDisposedException: The semaphore has been disposed #5863

Open
MikaelMayer opened this issue Oct 28, 2024 · 0 comments
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label kind: language development speed Slows down development of Dafny the language, flaky tests

Comments

@MikaelMayer
Copy link
Member

Seen here, only for Windows https://github.com/dafny-lang/dafny/actions/runs/11516350526/job/32058868043?pr=5846

[xUnit.net 00:00:24.34]     Microsoft.Dafny.LanguageServer.IntegrationTest.Completion.DotCompletionTest.CompleteOnNothingAtLineStartReturnsEmptyList [FAIL]
[xUnit.net 00:00:24.34]       OmniSharp.Extensions.JsonRpc.Server.InternalErrorException : Internal error. 
[xUnit.net 00:00:24.34]       Stack Trace:
[xUnit.net 00:00:24.34]            at OmniSharp.Extensions.JsonRpc.ResponseRouter.ResponseRouterReturnsImpl.Returning[TResponse](CancellationToken cancellationToken)
[xUnit.net 00:00:24.34]            at OmniSharp.Extensions.LanguageServer.Protocol.Progress.ProgressManager.<>c__DisplayClass22_0`1.<<MakeRequest>b__0>d.MoveNext()
[xUnit.net 00:00:24.34]         --- End of stack trace from previous location ---
[xUnit.net 00:00:24.34]         D:\a\dafny\dafny\dafny\Source\DafnyLanguageServer.Test\Completion\DotCompletionTest.cs(16,0): at Microsoft.Dafny.LanguageServer.IntegrationTest.Completion.DotCompletionTest.RequestCompletionAsync(TextDocumentItem documentItem, Position position)
[xUnit.net 00:00:24.34]         D:\a\dafny\dafny\dafny\Source\DafnyLanguageServer.Test\Completion\DotCompletionTest.cs(90,0): at Microsoft.Dafny.LanguageServer.IntegrationTest.Completion.DotCompletionTest.CompleteOnNothingAtLineStartReturnsEmptyList()
[xUnit.net 00:00:24.34]         --- End of stack trace from previous location ---
fail: Microsoft.Dafny.Compilation[0]
      Caught error in statusUpdates observable.
      System.ObjectDisposedException: The semaphore has been disposed.
         at System.Threading.SemaphoreSlim.WaitAsync(Int32 millisecondsTimeout, CancellationToken cancellationToken)
         at System.Threading.SemaphoreSlim.WaitAsync(CancellationToken cancellationToken)
         at VC.CheckerPool.FindCheckerFor(Program program, Split split, CancellationToken cancellationToken)
         at Microsoft.Boogie.VerificationTask.StartRun(CancellationToken cancellationToken)+MoveNext()
         at Microsoft.Boogie.VerificationTask.StartRun(CancellationToken cancellationToken)+System.Threading.Tasks.Sources.IValueTaskSource<System.Boolean>.GetResult()
         at System.Linq.AsyncEnumerable.ToObservableObservable`1.<>c__DisplayClass2_0.<<Subscribe>g__Core|0>d.MoveNext() in /_/Ix.NET/Source/System.Linq.Async/System/Linq/Operators/ToObservable.cs:line 50
  Failed Microsoft.Dafny.LanguageServer.IntegrationTest.Completion.DotCompletionTest.CompleteOnNothingAtLineStartReturnsEmptyList [82 ms]
  Error Message:
   OmniSharp.Extensions.JsonRpc.Server.InternalErrorException : Internal error. 
  Stack Trace:
     at OmniSharp.Extensions.JsonRpc.ResponseRouter.ResponseRouterReturnsImpl.Returning[TResponse](CancellationToken cancellationToken)
   at OmniSharp.Extensions.LanguageServer.Protocol.Progress.ProgressManager.<>c__DisplayClass22_0`1.<<MakeRequest>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Dafny.LanguageServer.IntegrationTest.Completion.DotCompletionTest.RequestCompletionAsync(TextDocumentItem documentItem, Position position) in D:\a\dafny\dafny\dafny\Source\DafnyLanguageServer.Test\Completion\DotCompletionTest.cs:line 16
   at Microsoft.Dafny.LanguageServer.IntegrationTest.Completion.DotCompletionTest.CompleteOnNothingAtLineStartReturnsEmptyList() in D:\a\dafny\dafny\dafny\Source\DafnyLanguageServer.Test\Completion\DotCompletionTest.cs:line 90
--- End of stack trace from previous location ---
@MikaelMayer MikaelMayer added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label kind: language development speed Slows down development of Dafny the language, flaky tests labels Oct 28, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label kind: language development speed Slows down development of Dafny the language, flaky tests
Projects
None yet
Development

No branches or pull requests

1 participant