First of all, this is a guide for MacOS users. I’m sorry, but I am physically unable to create a manual for other operating systems.
Disclamer – I hope you know what homebrew is.
We have to install coq on our machine. Best way to do it – opam. I didn’t even know about it until I had to contact Coq, btw.
Let’s install it.
brew install opam
Getting the Coq (not funny).
opam install coq
Coq code writing environment. We have several options here.
- The first is CoqIDE, a terrible choice, we won’t make it.
- The second is Emacs and its ProofGeneral. Not a bad choice, we’ll look at how to set it up.
- Final one is Visual Studio Code and its VSCoq. Good one too.
My personal choice is Visual Studio Code.
Let’s start with Emacs.
brew install emacs- Install.
touch ~/.emacs- Create a configuration file.
vi ~/.emacs- Open configuration file.
- Paste this
(load "~/.emacs.d/lisp/PG/generic/proof-site") (setq exec-path (append exec-path '("/usr/local/bin"))) # here you just have to call `which coqtop` and get the path. (custom-set-variables '(coq-prog-name "PATH/TO/coqtop") '(proof-three-window-enable t))
- Google.com to find out how to get out of VIM.
- Restart a terminal.
You’re ready to go.
Visual Studio Code
- Install Visual Studio Code
- Install VSCoq plugin
which coqctopand copy the path without
/coqtopat the end of the path.
- Open settings of VSCode and set
- Restart the VSCode.
You’re ready to go
Now you can be that guy.
If you find a mistake or just want to ask a question, write in the comments!