Steps for installing HoTT Coq and VIM on OSX
VIM: If you're using Vundle, get the plugin:
Bundle 'def-lkb/vimbufsync'
Bundle 'tbelaire/coquille'
Otherwise go to github.com/trefis/coquille and get it yourself. There is a dependancy on the vimbufsync plugin, so make sure to get that too.
I do
au FileType coq call coquille#FNMapping()
" Maps Coquille commands to <F2> (Undo), <F3> (Next), <F4> (ToCursor)
Edit a coq file, and do :CoqLaunch, then go below some proof and do :CoqToCursor (F4), to send a proof to Coq.
If the coloring sucks, you can fix it at ~/.vim/bundle/coqille/autoload/coquille.vim in the function function! coquille#Register() you can change to background hex codes directly. If I knew more vim, I'd try and make them respect your color scheme, but for now, you can just put a new hex code in, and it'll be readable.
brew install opam
opan init
# Answer questions
# Make sure that $PATH has the opam dir early in it, before brew's
# restart bash
opam switch 4.01.0
# restart bash
git clone [email protected]:HoTT/HoTT.git
cd HoTT
cd coq-HoTT; make clean; cd ..
# I manually built coq-HoTT
# You might be able to do:
# etc/install_coq.sh
# instead.
cd coq-HoTT
./configure -local
make
cd ..
# or just do
# The bindir
./configure COQBIN=coq-HoTT/bin/
make
make install
./hoqtop
# Works from that directory.
# I needed to edit /usr/local/bin/hoq-config
# and set all the paths to the location I built HoTT in,
# and now I think it works everywhere.
# Be happy
I'm just fixing up the vim dependancy