idris-hackers/idris-vim

Idris mode for vim

idris-vim's Issues

Syntastic not showing more than first line of error.

When I move the cursor to the line with the error, at the bottom of the screen I see:
When elaborating right hand side of add5:
It's nice to know there's an error at least, but the full error message would be nicer.
Is syntastic appropriate for that, or would maybe a quickfix window work better for longer error messages?

syntax "idrisIdentifier" is never matched outside "idrisTypeDecl"

I'm not sure whether it is intended or not, but this will cause some identifiers spell checked.

I think identifiers should not be spell checked anywhere.

Curly bracket wrongly indents the line it is inserted.

test : Vect n a -> String
test [] {n=Z} = case (Z) of
                     Z => ?fdgf_1
                     (S k) => ?fdgf_2
test (x :: xs) {n=n} = ?test_rhs_2

If you remove the right curly bracket from the second case and put it again, it makes the line to wrongly indent itself.

The result :

test : Vect n a -> String
test [] {n=Z} = case (Z) of
                     Z => ?fdgf_1
                     (S k) => ?fdgf_2
                     test (x :: xs) {n=n} = ?test_rhs_2

Syntax highlighting: prepending 'total' keyword to top-level declaration changes color of binding from declaration color to identifier color

Normally a top level declaration is highlighted like so:

Adding the total keyword changes the highlighting:

The new highlight color is the same as identifiers in patterns and expressions. It may be appropriate to change the color of 'total'-annotated functions, but it should be to something distinct.

<LocalLeader>d handles parenthesis incorrectly

I had something like the following (hypothetical) code snippet:

(++) : Nat -> Nat -> Nat

Then, while hovering over the left parethesis, I hit <LocalLeader>d and got the following:

(++) : Nat -> Nat -> Nat
       Nat k j = ?Nat_rhs

Obviously I was expecting something like:

(++) : Nat -> Nat -> Nat
(++) k j = ?something_rhs

strip ? from hole name before passing it to idris?

It seems like in order to make lemmas and some other things to work we need to cut of ?.

  if word =~ '^?'
    " Cut off '?' that introduces a hole identifier.
    let word = strpart(word, 1)
  endif

Before \l on hole dies with "invalid command":

plus_commutes Z m = ?plus_commutes_rhs_4

After above mentioned snippet is added \l produces

plus_commutes_rhs_4 : m = plus m 0

Doc comments are not formatted correctly

When trying to use :'<,'>gq to wrap doc comments (||| leader) the comment leader is not created on new lines, and may actually be treated as a word and joined into a previous, short line.

In addition, when pressing <Enter> in insert mode when inside a doc comment, the comment lead isn't inserted.

This seems related to e8563c4 which overwrites comments and formatoptions that are set in the main ftplugin/idris.vim with clearly inferior versions. But, based on the commit message was meant to help limit the surface area of a security issue.

case Has the underlying security issue been addressed completely?
Yes good -> Would a patch removing comments and formatoptions from the after script be accepted?
No still_vulnerable -> Anyone have a sketch of what needs to change to address the vulnerability? Do we need more shellescape calls somewhere? <|> Left (still_vulnerable ?exploit)

@raichoo

Syntastic not displaying errors

Using the latest versions of nvim (0.1.1), Syntastic (3.7.0-62), and idris (0.9.20.1), Syntastic isn't showing any errors in my .idr files, even though they show up with the idris --client ':l ' command. :SyntasticInfo shows that the idris checker is active.

vim does not recognize identifiers with '

idris-vim makes use of vim’s concept of a word when determining identifiers to send to idris. This does not by default include ', so, for example, when one has something like

foldl' : (b -> a -> b) -> b -> List' a -> b

and uses \d, this jumps to the beginning of the line, searches for the :, then goes back with b. This places the cursor on the ' of foldl', as for purposes of movement the non-blank non-wordchar sequence ' counts as a word. Then, a word is taken with expand("<cword>"). Since the cursor is not on a word character, this takes the next following word, namely b, which is then used in the idris client command.

The desired behavior is for it to use the identifier foldl' instead.

Unable to connect to a running idris repl

Hi

I'm getting this in Ubuntu (16.04 and 17.10).

I have pathogen installed and set up in my .vimrc, I installed idris-vim, I started idris --ide-mode, idris is in my current PATH, and yet this happens. The same happens if I used a console and run idris --client.

Perhaps someone could, please, add the instructions for any novice vim user to get this to work, from a fresh vim installation?

How do you change the syntax coloring?

Hi,

This is a dumb question, but I can't see where the syntax colors are chosen in the source and I want to change them.

How do I do that?

Cannot import files with a space in path

I am having trouble on Arch Linux with files with spaces in the path. A minimal example:

mkdir Space\ Dir
cd Space\ Dir/test.idr
idris test.idr

try to write a simple function signature and add a clause. Results in:

Can't find import /path/to/space/dir/Space

Thanks,
David Harrison

Can't see the type of some holes in a where block

Given this snippet:

five : Int
five = two + three where
  two : Int
  two = ?two_rhs
  three : Int
  three = 3

This type-checks fine but I can't query the type of ?two_rhs using vim interactive editing (<Leader> + t) by default. When loading in the REPL, :t two_rhs works fine too.

The error:

"Main.idr" 16L, 224C written                                                                              
/home/gpyh/idris-sandbox/Main.idr:10:3: error: not                                                        
    end of block, expected: ")",                                                                          
    "->", ";", "in",                                                                                      
    ambiguous use of a left-associative operator,                                                         
    ambiguous use of a non-associative operator,                                                          
    ambiguous use of a right-associative operator,                                                        
    declaration, end of input,                                                                            
    matching application expression,                                                                      
    where block                                                                                           
  three : Int                                                                                             
  ^                                                                                                       
/home/gpyh/idris-sandbox/Main.idr:10:3: error: not                                                        
    end of block, expected: ")",                                                                          
    "->", ";", "in",                                                                                      
    ambiguous use of a left-associative operator,                                                         
    ambiguous use of a non-associative operator,                                                          
    ambiguous use of a right-associative operator,                                                        
    declaration, end of input,                                                                            
    matching application expression,                                                                      
    where block                                                                                           
  three : Int                                                                                             
  ^                                                                                                       

However, querying the type of ?three_rhs in this snippet works fine:

five : Int
five = two + three where
  two : Int
  two = 2
  three : Int
  three = ?three_rhs

Expose functions as commands instead of only leader keybindings

Hello!

It'd be convenient (and more standard) to expose the functions provided by this plugin as commands that can be used without the supplied leader mappings.

e.g. the IdrisShowType function could be mapped to a command with the same name so it can be either invoked with :IdrisShowType<CR> or easily bound to another key mapping.

Cheers,
Louis

Module needs reloading on any command

Hi,

I am new to Idris and idris-vim. I am trying to test the functionality provided by the plugin like show type an case split. When I try it in a fresh open file it works perfectly, but after I made any change to the code all commands result in this message:

"hello.idr" 4L, 50C written

Loading /home/nil/hello.ibc failed: Module needs reloading:
        SRC : "/home/nil/hello.idr"
        Modified at: 2019-10-12 10:55:16.873346829 UTC
        IBC : "/home/nil/hello.ibc"
        Modified at: 2019-10-12 10:53:44.870012464 UTC


Loading /home/nil/hello.ibc failed: Module needs reloading:
        SRC : "/home/nil/hello.idr"
        Modified at: 2019-10-12 10:55:16.873346829 UTC
        IBC : "/home/nil/hello.ibc"
        Modified at: 2019-10-12 10:53:44.870012464 UTC

I tried reloading the file with <LocalLeader>r, but the same message appears.

The only solution I found is close vim and REPL, remove the .idc file and open everything again.

I am missing something or is this a bug?

My Idris version is Version 1.3.2-git:PRE, btw.

Thank you!

REPL for lidr ?

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?

TypeCheck Failure Printout is unexpected

Hi,

when a typecheck fails, vim-idris prints a less understandable error message than the standard idris repl.

It's the "Specifically" section that get's messed up.

As an example let's take the (wronlgy typed) ++ Function for Vect from the tutorial at

http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html

idris repl prints exactly what is also printed in the tutorial:
Specifically: Type mismatch between plus k k and plus k m

But in vim I get

Specifically: Type mismatch between plus k k and plus k mUnification failure

Is this just a missing newline before "Unification failure"?

Mention default localleader in README

It'd help if the default <LocalLeader> binding \ was mentioned in the README to lessen the friction on beginners.

Idris response window empty,

As the title says, really.
i response window is empty.
Vim 74, Idris 0.9.19, Idris-vim commit#5c36a164c220

Idris not started?

It seems that idris is not beeing started by vim. Instead I get Uncaught error: connet: dies not exist (Connection refused) whenever I try to use one of the idris-mode commands

<LocalLeader>t resets cursor location to beginning of line

Example:

blah : a -> a
blah x = ?foo

Typing \t on foo resets the cursor location to the start of the line, the b in blah.

syntastic interferes w/ interactive functionality when .ibc files present

Basically, the fun I had here:
idris-lang/Idris-dev#954
If the change described on #6 is made, I can get a proper definition from \d, and \c, but can't \t or \o.
Removing syntastic 3.3.0_113_g0de089b entirely seems to fix everything.
This became a bigger issue after idris-lang/Idris-dev@2df0a7f, as .ibcs weren't being saved for files w/ metavars before that.
syntastic may not be that useful given #1 - \r can be used instead.

What about lifting/extracting holes?

Appearantly you can "Lift a hole to the top level as a new function declaration" (from the Idris Book) with Ctrl-Alt-L in the Atom editor.

The Emacs package seems to have that implemented too:

from https://github.com/idris-hackers/idris-mode:
C-c C-e: Extract a hole or provisional definition name to an explicit top level definition.

I could not find this functionality in this package.

Is there any way to evaluate an expression?

Title.

Syntastic 3.2 support

Things go a bit wonky w/ the Syntastic check on 3.2.0. Syntastic 3.2.0 doesn't work as nicely for Haskell, either; I'm sticking w/ 3.1.0 for now.

Undo not working with idris response window

Hi,

The undo command works as expected as long as I don't open the idris response window _i

When I do it still works as long as i don't reload the file _r. When I do the history is lost. Any ideas?

Disclaimer: I'm new to vim

Unable to connect to a running Idris repl

I assume this is due to the ambiguous line in the readme:

If you need a REPL I recommend using Vimshell.

On vimshell, it says

Note: Active developement on vimshell.vim has stopped. The only future changes will be bug fixes.

Is a REPL needed? If so, what do people use today and how does one set it up?

Syntastic is not enabled

Hi I'm not getting Syntastic to work for idris, where it works for other languages

I can invoke the checker manually

:SyntasticCheck idris 

and it reports errors but the SyntasticInfo command tells me that it is not enabled

:SyntasticInfo 

Syntastic version: 3.8.0-110 (Vim 800, Neovim, Darwin)
Info for filetype: idris
Global mode: active
Filetype idris is active
The current file will be checked automatically
Available checker: idris
Currently enabled checkers: -

I activated some debug and I get the information that

syntastic: 0.052995: CacheErrors: no checkers available for idris

The full debug information can be found at

"enum.idr" 16L, 215C
syntastic: 0.049073: g:syntastic_version = '3.8.0-110 (Vim 800, Neovim, Darwin)'
syntastic: 0.049318: &shell = '/bin/zsh', &shellcmdflag = '-c', &shellpipe = '2>&1| tee', &shellquote = '', &shellredir = '>%s 2>&1', &shelltemp = 1, &shellxquote = '', &autochdir = 0, &shellxescape = ''
syntastic: 0.050125: UpdateErrors (auto): default checkers
syntastic: 0.050556: CacheErrors: default checkers
syntastic: 0.051391: g:syntastic_aggregate_errors = 0
syntastic: 0.051762: $TERM = 'xterm-256color'
syntastic: 0.051992: $TMPDIR = '/var/folders/s8/snh3nx3n1xx7jdmjh7qsbqh00000gp/T/'
syntastic: 0.052160: $PATH = '/Users/johan/.nvm/versions/node/v8.4.0/bin:/usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin:/Applications/MacVim.app/Contents/bin'
syntastic: 0.052521: getcwd() = '/Users/johan/workspace/idris'
syntastic: 0.052995: CacheErrors: no checkers available for idris

I'm pretty new to vi so please bear with my limited understanding.

String literal not processed correctly

When the cursor is under the word "Sausage" -- which is part of the string literal -- and you put \t then this plugin will tell you No such variable Sausage, it suggests that the word "Sausage" is recongnized as an identifier by this plugin.

Odd <LocalLeader>d Behavior

The use of d on keyNotInLeaf' fills in decEq x1 x2 = ?DecEq_rhs_1 in the following code:

data Tree : Type -> Type where
  Node : v -> Tree v -> Tree v -> Tree v
  Leaf : Tree v

Map : Type -> Type -> Type
Map k v = Tree (k,v)

data KeyInMap : DecEq key => key -> Map key value -> Type where
  Here  : DecEq key => (k = k') -> KeyInMap k (Node (k',v) l r)
  Left  : DecEq key => KeyInMap k l -> KeyInMap k (Node v l r)
  Right : DecEq key => KeyInMap k r -> KeyInMap k (Node v l r)

keyNotInLeaf' : DecEq key => (m = Leaf) -> KeyInMap k m -> Void
                    decEq x1 x2 = ?DecEq_rhs_1

Thanks,
David Harrison

Redundant parentheses in case split

Before case splitting:

No contra => case isElem value xs of
                  case_val => ?isElem_rhs_3

After it:

No contra => case isElem value xs of
                  (Yes prf) => ?isElem_rhs_1
                  (No contra) => ?isElem_rhs_2

Couldn't these parentheses be omitted automatically?

Retrieving type of holes is broken

Retrieving the type of a hole with \t has been broken, seemingly by a8f9fad, with the REPL outputting (input):IncompleteTerm. Reverting the commit makes it work again.

'dirty' error message ([idris/idris])

when getting a type error, my error message in vim looks like this:

|| datastore.idr:62:48-49: [idris/idris]
|| When checking right hand side of Main.case block in case block in parsePrefix at datastore.idr:57:8 at datastore.idr:60:14 with expected type [idris/idris]
||         Maybe (Char, String) [idris/idris]
|| When checking argument a to constructor Builtins.MkPair: [idris/idris]
||         Type mismatch between [idris/idris]
||                 (A, B) (Type of (a, b)) [idris/idris]
||         and [idris/idris]
||                 Char (Expected type) [idris/idris]
|| datastore.idr:108:1-8:When checking left hand side of display: [idris/idris]
|| When checking an application of Main.display: [idris/idris]
||         Type mismatch between [idris/idris]
||                 (A, B) (Type of (a, b)) [idris/idris]
||         and [idris/idris]
||                 Char (Expected type) [idris/idris]

Is it possible to get those error messages without having [idris/idris] written all over the place? (is it perhaps my vim setup that's causing all this noise in the output?)

Documentation issue with <LeaderKey> instead of "\"

It took me a long time to find out why I thought vim-idris was not working although the plugin was loaded:

• In vim I've configured my LeaderKey as Space! It is not anti-slash \

As a consequence none of the commands in the documentation were working.

So I tend to think you should modify the documentation and replace LeaderKey by back-slash \

Document \b command

Adds definitions when declaring new typeclass instances, apparently.

Toward Idris2 support on Vim, could use advice and help

Hi. I started working on Vim8/Idris2 modification that interacts through --ide-mode. I've gotten things working badly, but there are few odd things about the function of the IDE mode that I don't figure out.

https://github.com/cheery/idris-vim
https://github.com/cheery/idris-vim/blob/master/ftplugin/idris.vim

What am I supposed to do when I reload a file through idris-mode? Sometimes it's giving me 'return' response and other times it's not doing that. The IDE protocol documentation doesn't tell me what kind of choreography should the editor carry out.

The another question is with the "make-case". It's giving me a nice "fill-this-in" structure. How do I properly do the replacement though?

Also interested what do you think of the code. It's asyncronously running and I tie it up together with guard functions that retry on a task when progress is made.

Wrong highlighting

I'm using jellybeans color scheme, neovim, archlinux, latest idris-vim

As you can see, module name, %access private and many other things are not highlighted as on demo picture

Wrong type generated by `\l`

When following the tutorial here I was told to press \l to generate plus_commutes_S. This generated a function of the wrong type:

plus_commutes_S : (k : Nat) -> (m : Nat) -> (plus m k = plus k m) -> S (plus m k) = plus m (S k)

instead of

plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k).

\t gives the right type of ?plus_commutes_S before doing this. Any idea what's happening?

Case splitting results in error message "Elaborating Builtins.Pair arg A: CantUnify False ....."

Trying to case split on x at the second case of the belongs function...

import Data.Vect

data Node : String -> Type where
  MkNode : (s : String) -> Node s

belongs : ((s : String ** Node s), Nat) -> Vect n ((s : String ** Node s), Nat) -> Bool
belongs x [] = False
belongs x (y :: xs) = ?belongs_rhs_2

gets me this error message:

(val):Elaborating Builtins.Pair arg A: CantUnify False (Builtins.DPair {a1016} {P1017},Just (SourceTerm Builtins.MkDPair {a1016} {P1017} {x1018} {pf1019})) and (Type 0,Just ExpectedType) CantUnify False (Builtins.DPair {a1016} {P1017},Nothing) and (Type 0,Nothing)  in [({p
f1019},{P1017} {x1018}),({x1018},{a1016}),({P1017},{a1016} -> Type 0),({a1016},Type 0),(x,Builtins.Pair (Builtins.DPair String (\ s : String => Main.Node s)) Prelude.Nat.Nat),({k509},Prelude.Nat.Nat)] 0 in [({pf1019},{P1017} {x1018}),({x1018},{a1016}),({P1017},{a1016} -> T
ype 0),({a1016},Type 0),(x,Builtins.Pair (Builtins.DPair String (\ s : String => Main.Node s)) Prelude.Nat.Nat),({k509},Prelude.Nat.Nat)] 0

Unable to connect to a running Idris repl

The funcionality is broken. Whenver I send a conmmand, the message shows up.

Unable to connect to a running Idris repl 

I built idris from source (using stack), does it cause the problem?

<Leader>p over hole generates code that should not be

I upgraded to Idris 0.12.2 recently from 0.9.x (on a brand new machine) and had to rewrite a few things due to the interface and related changes between those versions. I do not believe my version of this vim plugin changed (which is likely the problem). I am not much of a vim plugin developer (though I have dabbled in the black arts), so if you provide pointers to me, I might be able to provide a PR if it is still a problem on the master HEAD.

I have detailed out my environment's versions here:
https://gist.github.com/mbbx6spp/6fe833d300b1492f9373864be3cae396#file-versions-txt

module Predicates

import Data.Vect

isElem : DecEq a => (value : a) -> (xs : Vect n a) -> Dec (Elem value xs)
isElem value [] = ?bug -- with cursor over ?bug hole if you <Leader>p it will complete with `Yes ?bug1`
isElem value (x :: xs) = ?irrelevant

Now put cursor over the ?bug hole above and then do <Leader>p in vim. This will complete with the code Yes ?bug1. See below.

module Predicates

import Data.Vect

isElem : DecEq a => (value : a) -> (xs : Vect n a) -> Dec (Elem value xs)
isElem value [] = Yes ?bug1
isElem value (x :: xs) = Yes (There ?isElem_rhs_5)

In another pane I have idris REPL running.

I am sure I have done something incredibly silly but it wasn't behavior I noticed on my old laptop with Idris v0.9.x.

I assume this is perhaps searching for the case in the line below where the hole actually is?

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 2586645 (current HEAD)

Using the asynchronous support in Vim 8

Can that help bring more ide-mode features in?

Syntastic integration generates bogus command lines

(idris-vim commit 45680a3, Idris 0.9.19.)

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.

Multiple loads of file during add-clause

I happened to be logging the arguments the idris process to a log file while testing the interactive features with vim. It seems that when you do a case-split, the file is loading 3 times.

args = ["--client",":l  test/interactive001/test032.idr "]
args = ["--client",":l  test/interactive001/test032.idr "]
args = ["--client",":l /Users/steshaw/Projects/idris/test/interactive001/test032.idr"]
args = ["--client",":ac! 6 f"]

This makes things feel quite sluggish.

I had a peek at ftplugin.vim but I'm not that familiar with Vim Script. Looks like at least one of the loads comes from a call to w (but I don't see how w calls back to IdrisReload).

Note that originally, I was outputting the idris args to stderr but it seemed to interfere with idris-vim. If you want to set up your idris like I did, a minimal code change to main/Main.hs is to update your main to something like this:

main = do
  args <- getArgs
  appendFile "idris.log" ("args = " ++ show args ++ "\n")
  opts <- runArgParser
  runMain (runIdris opts)

Connect to existing REPL (as when using tmux)

My ideal workflow would involve having the Idris REPL running in one tmux window and Vim running in another. When I do this and reload the file in Vim it seems to start its own internal REPL somehow which is in no way connected to the existing one.

Is there a way to force Vim to connect to the existing REPL?

Add unicode concealing?

I maintain vim-IdrisConceal and it was brought up that it might make sense to integrate that with this repository (japesinator/vim-IdrisConceal#3).

Wrong indentation of clauses on <LocalLeader>m

The indentation of clauses added by <LocalLeader>m depends on the position of the cursor at the time of invocation. Given the following example,

data Foo = Bar
         | Baz
         | Quux

foo : Foo -> Foo
foo Bar = ?foo_rhs

placing the cursor on the 'B' of the Bar pattern, followed by invoking <LocalLeader>m results in this

foo : Foo -> Foo
foo Bar = ?foo_rhs
    foo Quux = ?Bar_rhs_1
    foo Baz = ?Bar_rhs_2

Invoking the command at the beginning of the line works as expected, placing the latter two equations in the first column.

Change syntastic to use idris --client?

Should we change syntax_checkers/idris/idris.vim to run "idris --client :l" rather than idris --check? It's remarkably quicker to run the former way, but then that requires an idris repl to be fired up in that dir.

Would we want to make this configurable? Perhaps, even better would be if it could note the failure of idris --client, from a REPL not running, and fallback to idris --check.

Case split using <LocalLeader>c does not work

Test case (written manually, due to #10):

Case split on xs:

append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys = ?append_rhs

Idris internal error:
Internal error: "xs is not a pattern variable"

Versions:

idris 0.9.12 (cabal)
idris-vim 2586645 (current HEAD)