idris2-vim
idris2-vim copied to clipboard
File error in --no-color: File Not Found
When I reach for \t on a hole I get this error followed by an idris error that doesn't make sense like undefined name...

What version of idris2 are you using?
I am using Idris2 v0.2.1 btw, this very same file works just fine in Atom. The problem I have seems to be with the vim plugin. I reproduced this issue in Manjaro as well as OSX.11. It seems fine in Atom in both OS.
Same error with nearly all commands save \t which puts the cursor on the :
character of the type decl (claim?). Just installed idris2 from AUR and this plugin via Vundle. idris2
is on the PATH
.
Idris versions is 'Idris 2, version 0.2.1-2cd7350fb' and plugin version 964cebee493c85f75796e4f4e6bbb4ac54e2da9e. Running on Arch Linux.
Hi, I have the same issue. I think the issue originates from this line
function! s:IdrisCommand(...)
let idriscmd = shellescape(join(a:000))
" Vim does not support ANSI escape codes natively, so we need to disable
" automatic colouring
return system("idris2 --no-color --find-ipkg " . shellescape(expand('%:p')) . " --client " . idriscmd)
endfunction
From looking at the help and doing some testing I think that it would be enough to move --no-color after the filename and that should be enough
That didn't really work for me. I didn't look into the problem a lot, but pinning to an earlier commit seems to make at least reloading work:
# ...
(idris2-vim.overrideAttrs ({ ... }: {
src = fetchGit {
url = "https://github.com/edwinb/idris2-vim.git";
ref = "master";
rev = "099129e08c89d9526ad092b7980afa355ddaa24c";
};
}))
# ...
@jumper149 this worked for me (also using nix). Thank you!