Skip to content
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

The ide-mode closes when the idris code contains an error #13

Closed
archaeron opened this issue May 23, 2015 · 10 comments
Closed

The ide-mode closes when the idris code contains an error #13

archaeron opened this issue May 23, 2015 · 10 comments
Labels

Comments

@archaeron
Copy link
Member

the ide-mode closes when the idris code contains an error

Minimal example:

module Test

a
@cnd
Copy link
Member

cnd commented May 23, 2015

@archaeron or if .ibc is created with another idris version

@archaeron
Copy link
Member Author

@Heather cool, thanks. I haven't had that bug :)

@archaeron
Copy link
Member Author

@david-christiansen could you take a look at this?

setup:

file test.idr

module Test

a

start idris in ide mode:

..\idris-win64-0.9.18\idris.exe --ide-mode

load the file:

000018(:protocol-version 1 0)
00004f((:load-file "C:\Users\UserName\Documents\Programming\Idris\Start\test.idr") 1)
000111(:output (:ok (:highlight-source ((((:filename "C:\\Users\\UserName\\Documents\\Programming\\Idris\\Start\\test.idr") (:start 1 8) (:end 1 12)) ((:namespace "Test") (:decor :module) (:source-file "C:\\Users\\UserName\\Documents\\Programming\\Idris\\Start\\test.idr")))))) 1)
000111(:output (:ok (:highlight-source ((((:filename "C:\\Users\\UserName\\Documents\\Programming\\Idris\\Start\\test.idr") (:start 1 8) (:end 1 12)) ((:namespace "Test") (:decor :module) (:source-file "C:\\Users\\UserName\\Documents\\Programming\\Idris\\Start\\test.idr")))))) 1)
idris.exe: src\Idris\Parser.hs:(1276,40)-(1279,67): Non-exhaustive patterns in case

and then the compiler closes

archaeron added a commit that referenced this issue May 23, 2015
@david-christiansen
Copy link
Member

david-christiansen commented May 23, 2015 via email

@archaeron
Copy link
Member Author

https://gist.github.com/archaeron/46ff50b5ecf5ef53d4e0

this is all I need to crash the ide-mode :)

and I'm not doing this from the editor, but directly from the terminal

@archaeron
Copy link
Member Author

@david-christiansen would you lke me to open an issue on idris-dev with a step by step guide on how to reproduce the error and what I expected to happen?

@david-christiansen
Copy link
Member

david-christiansen commented May 24, 2015 via email

@archaeron
Copy link
Member Author

done: idris-lang/Idris-dev#2317

@david-christiansen
Copy link
Member

The underlying Idris issue should be fixed in master. Would you please confirm that it's now fixed?

@archaeron
Copy link
Member Author

I can confirm that it's working with a freshly built idris from master.

thanks, this helps a lot!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

3 participants