sourcedir = "." causes diagnostics to always appear at top of file

[xavierzwirtz]

I am messing about with the lsp inside of emacs, diagnostics are stuck at the top of the file.

Test file:

module Main

test : String
test = "foo"

test2 : String
test2 = 5

lsp output:

{
   "jsonrpc":"2.0",
   "method":"textDocument/publishDiagnostics",
   "params":{
      "uri":"file:///home/xavier/projects/idris-book/chapters/chapter02/Average.idr",
      "diagnostics":[
         {
            "range":{
               "start":{
                  "line":0,
                  "character":0
               },
               "end":{
                  "line":0,
                  "character":0
               }
            },
            "severity":1,
            "source":"idris2",
            "message":"In /home/xavier/projects/idris-book/./chapters/chapter02/Average.idr: While processing right hand side of test2. Can't find an implementation for Num String."
         }
      ]
   }
}

[ShinKage]

Thanks for the report. I suspect this is related to https://github.com/idris-community/idris2-lsp/issues/23. I will investigate further if it is a compiler reporting error or a server issue.

[ShinKage]

@xavierzwirtz I cannot reproduce the issue. From the error message I see a filename called Average.idr but the snippet module name is Main, so the correct error message should be that file name/module name do not correspond and should be thrown at the top of the file, which it does. If I try with the correct file name it puts the error at the exact location, which is the 5 literal. Can you provide more information? There is an ipkg file? Was this same file compiled before or renamed? Is this file imported by another module and the error occured while checking the that?

[xavierzwirtz]

Tried renaming the module to Average, same issue. Yes there is an ipkg file, but it is a couple directories above Average.idr. I don't think I have compiled it or renamed it, just muking about in the editor. Not imported by any other file, just Average.idr.

[xavierzwirtz]

Scratch that, when I rename the module to Average, I instead get the error:

 Average.idr     1   1 error           In /home/xavier/projects/idris-book/./chapters/chapter02/Average.idr: Module name Average does not match file name "/home/xavier/projects/idris-book/chapters/chapter02/Average.idr" (lsp)

[ShinKage]

The last error seems correct, because if you have the ipkg file in some parent folder and you leave the default src file folder option, then the compiler expects that the module name to be namespaced by the subdirectories. In your error, assuming the ipkg is in the idris-book folder, and that there is no custom value for the sourcedir option in the ipkg, the correct declaration would be module chapters.chapter02.Average (I'm not 100% positive about lowercase). However this is really a compiler behaviour, LSP just inherits it. The original error was probably due to the asynchronicity of the protocol or the compiler loading an old/incorrect version of the build artifacts. Again, I will try to investigate further but I don't think it's an issue easily reproducible.

[xavierzwirtz]

You were correct about the decleration needing to be module chapters.chapter02.Average, and correct about lower case causing issues. Fixed that, and still getting same behavior. Also tried moving out of a sub folder adjacent to the ipkg, same behavior.

[ShinKage]

I think I've found the issue and it has to do with non normalised paths. In the error you provided above there is idris-book/./chapters which may cause some issues. I'm working on some improvements to diagnostics, should be fixed by that. I will ping on this issue when it's ready.

[xavierzwirtz]

Very much appreciated, thank you for the quick attention.

[xavierzwirtz]

I reviewed the ipkg, it has sourcedir = ".". Changing that to Chapters and amending the module names makes diagnostics report properly.

[michaelmesser]

I plan on fixing this with the change in how errors and warnings will be reported. I am still trying to figure out the best way to do that. The compiler code is quite complex.

I started on a path normalization function:

normalizePath : Path -> Path
normalizePath (MkPath volume hasRoot body hasTrailSep) = MkPath volume hasRoot (normalizeBody hasRoot body) hasTrailSep
    where
    normalizeBodyHelper : SnocList String -> (hasRoot : Bool) -> List Body -> List Body
    normalizeBodyHelper ys hasRoot [] = if ys == [<] && not hasRoot then [CurDir] else Normal <$> cast ys
    normalizeBodyHelper ys hasRoot (CurDir :: xs) = normalizeBodyHelper ys hasRoot xs
    normalizeBodyHelper ys hasRoot (Normal x :: xs) = normalizeBodyHelper (ys :< x) hasRoot xs
    normalizeBodyHelper [<] False (ParentDir :: xs) = ParentDir :: normalizeBodyHelper [<] False xs
    normalizeBodyHelper [<] True (ParentDir :: xs) = normalizeBodyHelper [<] True xs
    normalizeBodyHelper (ys :< _) hasRoot (ParentDir :: xs) = normalizeBodyHelper ys hasRoot xs

    normalizeBody : (hasRoot : Bool) -> List Body -> List Body
    normalizeBody = normalizeBodyHelper [<] where