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

Error "Request textDocument/documentSymbol failed" appears regularly #446

Closed
tchajed opened this issue Oct 13, 2023 · 3 comments · Fixed by dafny-lang/dafny#4675
Closed
Labels
bug Something isn't working language server Relates to the Dafny LSP server

Comments

@tchajed
Copy link

tchajed commented Oct 13, 2023

While typing out code (so with many intermediate states with invalid code, and possibly due to concurrency) I very often get this error:

[Error - 12:00:38 PM] Request textDocument/documentSymbol failed.
Error: Illegal argument: line must be non-negative
    at w (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/workbench/api/node/extensionHostProcess.js:10:1101)
    at new s (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/workbench/api/node/extensionHostProcess.js:121:4368)
    at new o (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/workbench/api/node/extensionHostProcess.js:121:5884)
    at D (/Users/tchajed/.vscode/extensions/dafny-lang.ide-vscode-3.2.1/dist/extension.js:1:429900)
    at W (/Users/tchajed/.vscode/extensions/dafny-lang.ide-vscode-3.2.1/dist/extension.js:1:435434)
    at W (/Users/tchajed/.vscode/extensions/dafny-lang.ide-vscode-3.2.1/dist/extension.js:1:435547)
    at W (/Users/tchajed/.vscode/extensions/dafny-lang.ide-vscode-3.2.1/dist/extension.js:1:435547)
    at d (/Users/tchajed/.vscode/extensions/dafny-lang.ide-vscode-3.2.1/dist/extension.js:1:473826)
    at Object.t.map (/Users/tchajed/.vscode/extensions/dafny-lang.ide-vscode-3.2.1/dist/extension.js:1:473912)
    at Object.asDocumentSymbols (/Users/tchajed/.vscode/extensions/dafny-lang.ide-vscode-3.2.1/dist/extension.js:1:443428)
    at r (/Users/tchajed/.vscode/extensions/dafny-lang.ide-vscode-3.2.1/dist/extension.js:1:379675)
    at r.provideDocumentSymbols (/Applications/Visual Studio Code.app/Contents/Resources/app/out/vs/workbench/api/node/extensionHostProcess.js:127:37581)

I'm using v3.2.1 of the extension and Dafny v4.3.0, and I'm on macOS.

@keyboardDrummer
Copy link
Member

Any chance you could post a piece of code that causes this? I'm guessing it's a deterministic error.

@keyboardDrummer keyboardDrummer added bug Something isn't working language server Relates to the Dafny LSP server labels Oct 16, 2023
@tchajed
Copy link
Author

tchajed commented Oct 16, 2023

Sure, open up a new Dafny file and type function, then wait for a second.

@keyboardDrummer
Copy link
Member

Sure, open up a new Dafny file and type function, then wait for a second.

Thank you! Fixed on master now

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working language server Relates to the Dafny LSP server
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants