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

Idris exits when parsing malformed code file #4013

justjoheinz opened this Issue Aug 22, 2017 · 2 comments


None yet
4 participants
Copy link

justjoheinz commented Aug 22, 2017

Steps to Reproduce

Place this into a file ops.idr


Expected Behavior

idris should hint that there is a parse error, but it should not quit. Especially in ide-mode as this kills the process without the application being potentially aware of it. In ide-mode it should also send parseable error information.

Observed Behavior

~/Projects/idris/idris-sandbox/issue$ idris ops.idr
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 1.1.1
  _/ // /_/ / /  / (__  )      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
idris: user error (./ops.idr:4:1: error: unexpected
    EOF, expected: end of comment
^     )

Idris simply quits.

@jfdm jfdm changed the title Idris exists when parsing malformed code file Idris exits when parsing malformed code file Aug 22, 2017


This comment has been minimized.

Copy link

jfdm commented Aug 22, 2017

Hi @justjoheinz thanks for the issue report. I've fixed the typo in the title. Nested comments are one of those tricky things, however, I think it is more important if Idris' behaviour across the different modes is made more expected. If I find time, I'll try to have a look at it.


This comment has been minimized.

Copy link

melted commented Aug 22, 2017

The file can be simplified to {- :-)

Try to put it under some code and Idris doesn't quit.

The reason for the behavior is in the import parsing code (parseImports in Idris/Parser.hs:1563), where it calls fail if the parsing doesn't succeed. The fix would be to handle a parse failure like it is in the parseProg function. The main problem would be to handle failure in the callers of parseImports that now assumes it succeeds.

melted added a commit to melted/Idris-dev that referenced this issue Sep 2, 2017

@melted melted closed this in #4043 Sep 3, 2017

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment