Wrong line numbers (all [1, 1])

[iacore]

Bug: The "Problems" tab have the wrong line numbers. The squiggle underlines are in the wrong place too.

In the above screenshot, the problem is that right side of main doesn't match IO (), but the underline is at line 1.

[bamboo]

Hi @locriacyber, thanks for taking the time to report the issue.

This extension doesn't control the line numbers as it only serves as a bridge between Visual Studio and the Idris2 language server.

Would you mind reporting this issue in the idris2-lsp issue tracker?

[iacore]

I don't know about LSP. Do you know how to test a language server? I won't report this issue to idris2-lsp if I haven't reproduced it.

[michaelmesser]

I cannot reproduce the issue.

[iacore]

I tried with latest idris-lsp from main branch with this vscode extension from marketplace, version 0.7.0. Same behavior. I tried your vscode extension from main branch. Same behavior.

I'm using it on Linux.

Same code for reproducing the bug

reverse : List a -> List a
reverse xs = revAcc [] xs where
  revAcc : List a -> List a -> List a
  revAcc acc [] = acc
  revAcc acc (x :: xs) = revAcc (x :: acc) xs

main : IO ()
main = ()

[iacore]

I modified this extension to see what's wrong. (https://github.com/locriacyber/idris2-lsp-vscode/tree/issue-6) Error message I got from logging stdout:

LOG DEBUG:Communication.Channel: Received message: {"jsonrpc":"2.0","method":"textDocument/didSave","params":{"textDocument":{"uri":"file:///home/user/computing/test/idris/Reverse.idr"},"text":"reverse : List a -> List a\nreverse xs = revAcc [] xs where\n  revAcc : List a -> List a -> List a\n  revAcc acc [] = acc\n  revAcc acc (x :: xs) = revAcc (x :: acc) xs\n\nmain : IO ()\nmain = ()\n\n"}}
LOG INFO:Communication.Channel: Received notification for method "textDocument/didSave"
LOG INFO:Communication.Channel: Received didSave notification for file:///home/user/computing/test/idris/Reverse.idr
LOG INFO:Server: Loading file file:///home/user/computing/test/idris/Reverse.idr
LOG INFO:Notification.Diagnostic: Sending diagnostic message for file:///home/user/computing/test/idris/Reverse.idr
LOG INFO:Communication.Channel: Sent notification message for method "textDocument/publishDiagnostics"
LOG DEBUG:Communication.Channel: Notification sent: {"jsonrpc":"2.0","method":"textDocument/publishDiagnostics","params":{"uri":"file:///home/user/computing/test/idris/Reverse.idr","diagnostics":[{"range":{"start":{"line":0,"character":0},"end":{"line":0,"character":0}},"severity":1,"source":"idris2","message":"In /home/user/computing/test/idris/./Reverse.idr: While processing right hand side of main. Sorry, I can't find any elaboration which works. All errors:\nIf Unit: When unifying Type and IO ().\nMismatch between: Type and IO ().\nIf MkUnit: When unifying () and IO ().\nMismatch between: () and IO ()."}]}}

Note the {"line":0,"character":0}

[michaelmesser]

No need to modify the extension it already logs by default. What is the content of your .ipkg? /home/user/computing/test/idris/./Reverse.idr looks odd to me

[michaelmesser]

Does idris2 --check --find-ipkg work on Reverse.idr?

[michaelmesser]

I would recommend changing your source directory to src. I'm not sure if this is a bug in idris2-lsp or Idris2, but this is not a bug in idris2-lsp-vscode.

[iacore]

No need to modify the extension it already logs by default. What is the content of your .ipkg? /home/user/computing/test/idris/./Reverse.idr looks odd to me

It didn't log stdout

[iacore]

Does idris2 --check --find-ipkg work on Reverse.idr?

No