idris-hackers
Template creation via <LocalLeader>d not adding patterns for parameters
Test case:
append : Vect n a -> Vect m a -> Vect (n + m) a
Apply \d on append.
Expected something like:
append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys = ?append_rhs
Got that instead:
append : Vect n a -> Vect m a -> Vect (n + m) a
append = ?append_rhs
Version info:
idris 0.9.12 (cabal) idris-vim 25866452141e2ab9ecc642a9682f4a9a76501063 (current HEAD)
Still occurs in 7a0f64d idris-0.9.15 when did this break, has someone bisected yet?
What are the steps to reproduce this? Does it happen every time? Have you tried, for example, deleting all .ibcs and checking that there's no other idris running?
I know there are some issues with interactive editing, but I can't reproduce this one as it is, so I think there must be something different in your environment, and if we can work out what it is then we might be able to fix this. In any case, it is likely an Idris issue rather than a vim mode issue.
This could be related to another plugin interfering with idris-vim. I had a similar issue with syntastic, I fixed it by adding let g:syntastic_check_on_wq = 0 to my .vimrc.
Hopefully fixed in https://github.com/scrooloose/syntastic/pull/1215
OK, after some research this seems to be related to calling idris --check while another idris instance is running. Essentially it looks like non-atomic updates to IBC files from idris --check and idris --client racing one another. Unfortunately I was quickly lost while trying to trace back the function calls in Idris. :/
Hope this is helpful