Unexpected behaviour of the ide-mode

[archaeron]

Steps to reproduce

1. have a file test.idr with this content:

   module Test
   
   a

2. start the ide-mode in the command line: idris.exe --ide-mode

3. load the file into the ide-mode:
   00004f((:load-file "C:\Users\Nicolas\Documents\Programming\Idris\Start\test.idr") 1)

4. the ide-mode responds with (note the same output twice):

   000111(:output (:ok (:highlight-source ((((:filename "C:\\Users\\Nicolas\\Documents\\Programming\\Idris\\Start\\test.idr") (:start 1 8) (:end 1 12)) ((:namespace "Test") (:decor :module) (:source-file "C:\\Users\\Nicolas\\Documents\\Programming\\Idris\\Start\\test.idr")))))) 1)
   000111(:output (:ok (:highlight-source ((((:filename "C:\\Users\\Nicolas\\Documents\\Programming\\Idris\\Start\\test.idr") (:start 1 8) (:end 1 12)) ((:namespace "Test") (:decor :module) (:source-file "C:\\Users\\Nicolas\\Documents\\Programming\\Idris\\Start\\test.idr")))))) 1)
   

5. and then closes itself with:

   idris.exe: src\Idris\Parser.hs:(1276,40)-(1279,67): Non-exhaustive patterns in case

Expected behaviour

It would be nice if the ide-mode would tell me that my inputfile is bogus instead of closing/crashing.
Maybe something like:
(:return (:error (13 1 "insert error message here") [HIGHLIGHTING]))

[david-christiansen]

Interestingly, this doens't happen for me. I get the following transcript:

10:35:20 -> ((:load-file "test.idr")
 47)
10:35:20 <- (:output
 (:ok
  (:highlight-source
   ((((:filename "test.idr")
      (:start 1 8)
      (:end 1 12))
     ((:namespace "Test")
      (:decor :module)
      (:source-file "/home/drc/tmp/lkj/test.idr"))))))
 47)
10:35:20 <- (:output
 (:ok
  (:highlight-source
   ((((:filename "test.idr")
      (:start 1 8)
      (:end 1 12))
     ((:namespace "Test")
      (:decor :module)
      (:source-file "/home/drc/tmp/lkj/test.idr"))))))
 47)
10:35:20 <- (:warning
 ("./test.idr"
  (4 1)
  (4 1)
  " error: unexpected\n    EOF, expected: \"with\",\n    argument expression,\n    constraint argument,\n    function right hand side,\n    implicit function argument,\n    with pattern\n<EOF> \n^     " nil)
 47)
10:35:20 <- (:write-string "Type checking ./test.idr" 47)
10:35:20 <- (:set-prompt "*test" 47)
10:35:20 <- (:return
 (:error "didn't load test.idr")
 47)

The function at the line numbers in your error message appears to be a hack to extract error locations produced by Trifecta (see #1575). Its source is:

findFC :: Doc -> (FC, String)
findFC x = let s = show (plain x) in
             case span (/= ':') s of
               (failname, ':':rest) -> case span isDigit rest of
                 (line, ':':rest') -> case span isDigit rest' of
                   (col, ':':msg) -> let pos = (read line, read col) in
                                         (FC failname pos pos, msg)

My guess is that this is related to things like filenames being different on Windows. Would you please try the following steps?

1. Try loading the same file not in IDE mode (e.g., with idris --check test.idr), and see if the same error occurs
2. Try inserting a show as follows, and post here what the actual argument is that triggers the error:

findFC :: Doc -> (FC, String)
findFC x = let s = show (plain x) in trace ("Here's the arg! " ++ s) $
             case span (/= ':') s of
               (failname, ':':rest) -> case span isDigit rest of
                 (line, ':':rest') -> case span isDigit rest' of
                   (col, ':':msg) -> let pos = (read line, read col) in
                                         (FC failname pos pos, msg)

Even better would be to solve #1575 the right way.

/David

[archaeron]

here the output of test 1. (..\idris-win64-0.9.18\idris.exe --check test.idr)

.\test.idr:4:1: error: unexpected                          
    EOF, expected: "with",                                 
    argument expression,                                   
    constraint argument,                                   
    function right hand side,                              
    implicit function argument,                            
    with pattern                                           
<EOF>                                                      

so everything is working as it should here.
I'll try nr 2 if I get Idris to compile again :)

[archaeron]

okay. here the output of nr. 2:

000018(:protocol-version 1 0)                                                                                  
00004f((:load-file "C:\Users\Nicolas\Documents\Programming\Idris\Start\test.idr") 1)                           
000111(:output (:ok (:highlight-source ((((:filename "C:\\Users\\Nicolas\\Documents\\Programming\\Idris\\Start\
\test.idr") (:start 1 8) (:end 1 12)) ((:namespace "Test") (:decor :module) (:source-file "C:\\Users\\Nicolas\\
Documents\\Programming\\Idris\\Start\\test.idr")))))) 1)                                                       
000111(:output (:ok (:highlight-source ((((:filename "C:\\Users\\Nicolas\\Documents\\Programming\\Idris\\Start\
\test.idr") (:start 1 8) (:end 1 12)) ((:namespace "Test") (:decor :module) (:source-file "C:\\Users\\Nicolas\\
Documents\\Programming\\Idris\\Start\\test.idr")))))) 1)                                                       
Here's the arg! C:\Users\Nicolas\Documents\Programming\Idris\Start\test.idr:4:1: error: unexpected             
    EOF, expected: "with",                                                                                     
    argument expression,                                                                                       
    constraint argument,                                                                                       
    function right hand side,                                                                                  
    implicit function argument,                                                                                
    with pattern                                                                                               
<EOF>                                                                                                          
^                                                                                                              
idris.exe: src\Idris\Parser.hs:(1276,40)-(1279,67): Non-exhaustive patterns in case                            

[david-christiansen]

Looks like it's the colon in the filename. That function is such a kludge. I need to think a bit about how to at least improve it, if not fix it.