search

snu-sf-class / pl2016

14 stars 17 forks source link

Coq with vim #11

Open swchoi06 opened 8 years ago

swchoi06 commented 8 years ago

I downloaded CoqIDE on mac, and as everybody knows it's CRAP! So I tried to use vim instead of CoqIDE, and I just want to share.

There is vim plugin named 'Coquille'. You should install vim package manager pathogen and vimbufsync to run Coquille.

To launch Coquille on your Coq file, run :CoqLaunch which will make the commands : CoqNext CoqToCursor CoqUndo CoqKill

Check the details here. https://github.com/the-lambda-church/coquille

However, it is still uncomfortable because vim command is too complicate. Everytime you open Coq file, you should enter :CoqLaunch to launch coq. If you want to execute next three lines... you should type :CoqNext three times. It's really annoying. If you try it, you will know what I mean.

So I added following codes in my .vimrc file.


" Coquille plugin for coq in vim
:map J :CoqNext<Enter>
:map K :CoqUndo<Enter>
:map H :CoqToCursor<Enter>
autocmd BufNewFile,BufRead *.v CoqLaunch

First, I mapped CoqNext, CoqUndo, CoqToCurser commands to 'J', 'K', 'H'. You can use J, K to execute and undo line by line. Similar to j, k which is vim's default arrow keys. Second, I made CoqLaunch command to execute automatically if *.v file (which is coq file) is open. So you don't have to enter it every time.

I hope this might help you.

jeehoonkang commented 8 years ago

Thank you soooo much!

jeehoonkang commented 8 years ago

If you don't mind, I would like to add this material in the repository.

Thank you, Jeehoon

swchoi06 commented 8 years ago

Sure. Feel free to use it!

By the way, I misspelled :CoqToCursor to :CoqToCurser. I just edited my original code.

Thanks

nolsigan commented 8 years ago

Thank you for sharing!

I followed instructions in coquille's github page but I get an error : 

Error: Coqtop isn't running. Are you sure you called :CoqLaunch?

but I did :CoqLaunch and when I redo it, it says 'Coq is already running'.

If you experienced similar error, it will be really helpful if you share it!

Found out why.. silly mistake..

If anyone is trying this on mac, you have to first install coq in terminal by

brew install coq
jeehoonkang commented 8 years ago

"Install Coq for OS X": https://github.com/snu-sf-class/pl2016#coq