The idris-vim Syntastic integration is generating command lines of the form
idris --client :l filename.idr
which causes Idris to bomb out with a usage message. (Unfortunately it returns 0 when it does so, so vim provides no indication that something's wrong.)
The command line needs to be of the form
idris --client ":l filename.idr"
because Idris appears to be processing individual argument strings as commands, not the entire set of arguments.
I've managed to fake this in the current version by abusing args and post_args to surround the command with quotes. This works only because Idris is tolerant of whitespace before and after filenames; it isn't clear how it would work with a filename e.g. containing whitespace.
(idris-vim commit 45680a3c412f2cc8d40aff512e5e9ace44002922, Idris 0.9.19.)
The idris-vim Syntastic integration is generating command lines of the form
which causes Idris to bomb out with a usage message. (Unfortunately it returns 0 when it does so, so vim provides no indication that something's wrong.)
The command line needs to be of the form
because Idris appears to be processing individual argument strings as commands, not the entire set of arguments.
I've managed to fake this in the current version by abusing
args
andpost_args
to surround the command with quotes. This works only because Idris is tolerant of whitespace before and after filenames; it isn't clear how it would work with a filename e.g. containing whitespace.