-
Notifications
You must be signed in to change notification settings - Fork 50
Open
Labels
kind: bugSomething isn't workingSomething isn't working
Description
Describe the bug
If you try to create a file with an invalid name the LSP silently get an error but do not report it
To Reproduce
Steps to reproduce the behavior:
- Create a file with didOpen with an invalid name (begin with a number, no '.v' at the end for example)
- The LSP returns nothing in the promise even though using LogTraceNotification it sees there is a problem
Expected behavior
The LSP should return an error through the promise of the request
Desktop (please complete the following information):
- Operating system: Arch
- coq-lsp version : https://github.com/ejgallego/rocq-lsp/actions/runs/19231026459/artifacts/4518852242 (i'm using the worker)
Additional context
I did not check for any invalid way to create a file_name / uris but i assume the same problem occurs
Metadata
Metadata
Assignees
Labels
kind: bugSomething isn't workingSomething isn't working