edwinb/idris2-vim

Vim mode for Idris 2

idris2-vim's Issues

I do not even get syntax highlighting

I have done exactly the steps

cd ~/.vim/bundle
git clone https://github.com/edwinb/idris2-vim.git

But after opening some idris file, I do not even get syntax highlighting.

Note: I do not understand what you meant by recommend use of pathogen.

Maybe additional steps have to be done.

Not working at all

When ever I to do anything it throws a parse error about symbols that are not even it the file. Here is my file, called test.idr.

module test

test : a -> ()

If i put my cursor any where on the line with the test function and do '\a' I get this output on the '\i' screen and my cursor is set to the colon.

Parse error: Unrecognised command (next tokens: [identifier ac, symbol !, end of input])

Syntastic does not work out of the box

managed to make it work

installed idris2 and syntastic with pathogen

inside ~/.vim/bundle/idris2/syntax_checkers/idris2/idris2.vim

idris2-vim/syntax_checkers/idris2/idris2.vim

Line 26 in 099129e

function! SyntaxCheckers_idris_idris_GetLocList() dict

changed to

function! SyntaxCheckers_idris2_idris2_GetLocList() dict

in vimrc

let g:syntastic_idris_checkers = ['idris']
let g:syntastic_idris2_checkers = ['idris2']

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...

Link to `Interactive Idris editing with vim` goes to private wordpress page

Link to Interactive Idris editing with vim instructions goes to private wordpress page. Can't find the editing instructions elsewhere

Case splitting inserts invalid code that uses "$resolvedXXX" as an identifer.

There's almost certainly a smaller example, but this is the one I have and it's fairly small.

data BNat = BZ | O BNat | E BNat

data BLT : BNat -> BNat -> Type where
  BLT_ZO : BLT BZ (O bn)
  BLT_ZE : BLT BZ (E bn)
  BLT_OO : BLT bn bm -> BLT (O bn) (O bm)
  BLT_OE : BLT bn bm -> BLT (O bn) (E bm)
  BLT_OE_Eq : BLT (O bn) (E bn)
  BLT_EO : BLT bn bm -> BLT (E bn) (O bm)
  BLT_EE : BLT bn bm -> BLT (E bn) (E bm)

notLtz : BLT bn BZ -> Void
notLtz x = ?notLtz_rhs

Then do a case-split on x in the last line and you get:

notLtz : BLT bn BZ -> Void
notLtz $resolved123 impossible
notLtz $resolved124 impossible
notLtz ($resolved125 x) impossible
notLtz ($resolved127 x) impossible
notLtz $resolved126 impossible
notLtz ($resolved128 x) impossible
notLtz ($resolved129 x) impossible

(the numbers at the end of "resolved" may vary.)

MakeWith is broken

When I'm on a hole and I use <LocalLeader>w, it prints the with syntax, but it doesn't actually modify the buffer at all.

Plugin does not load correctly on neovim / vim-plug

This might be specific to my setup, I've installed the plugin using Vim-Plug and I'm running the nightly build of NeoVim.

The plugin would not load and no Idris2-Vim commands / functions were available.

Without loading any plugins ( commenting out the plugins ) except for the Idris2-Vim plugin, the plugin still would not work.

When calling set runtimepath? within an Idris2 buffer the idris2-vim/after folder is listed within the runtime variable.

After installing the plugin using Vim-Plug and without exiting NeoVim the plugin would work as expected on Idris2 buffers.

[ Solution ]

Moving the following line to above the plug#begin function within my init.vim configuration file allows the plugin to work as expected:

filetype plugin indent off

Hopefully this description can help others in a similar predicament.

MakeLemma doesn't transport erasable implicit arguments that must be explicitly bound for type checking

data BNat = BZ | O BNat | E BNat

bnat_ind : {0 p : BNat -> Type}
        -> p BZ
        -> ((bn : BNat) -> p bn -> p (O bn))
        -> ((bn : BNat) -> p bn -> p (E bn))
        -> (bn : BNat) -> p bn
bnat_ind pbz po pe = go
 where
  go : (bn : BNat) -> p bn
  go BZ = ?pbz_hole
  go (O x) = po x (go x)
  go (E x) = pe x (go x)

Using MakeLemma <LocalLeader>l on the ?pbz_hole in the above results in:

pbz_hole : ((bn : BNat) -> p bn -> p (E bn)) -> ((bn : BNat) -> p bn -> p (O bn)) -> p BZ -> p BZ

being created, but that doesn't type check:

file:loc:While processing type of pbz_hole at talia.idr:16:1--18:1:                                                                              
Undefined name p

(and then further failures since pbz_hole ends up not bound in the global context.)