REPL for lidr ?

[TimRichter]

I'm not sure whether this is an issue with idris-vim or just with my setup, please bear with me.

When editing .lidr (literate idris) files, and doing the key combinations that should call
the REPL, i.e. r , nothing happens. What am I doing wrong?

[ctford]

I have the same problem. To work around it, try :set filetype=idris when you're editing a .lidr file. It looks like idris-vim isn't recognising the filetype.

[melted]

Hmmm, there is support: https://github.com/idris-hackers/idris-vim/blob/master/ftdetect/lidris.vim

[ctford]

That sets filetype to "lidris" not "idris". Seems that the repl depends on "idris".

[ctford]

When I try :set filetype=idris I can evaluate the buffer once, but when I do it a second time I get the following error popping up in the REPL:

Idris> Symbol "idris_mkFileError" not found
idris: user error (Could not call foreign function "idris_mkFileError" with args [prim__vm (prim__TheWorld)])

I guess that simply forcing vim to see literate files as regular ones gets it confused somehow, perhaps because the .ibc file isn't properly created.