pic

First of all, this is a guide for macOS users. I’m sorry: I am physically unable to create a manual for other operating systems.

Disclaimer – I hope you know what homebrew is.

First step

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

Second step

Getting the Coq (not funny).

opam install coq

Third step

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.
  • The 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
  • Execute which coqctop and copy the path without /coqtop at the end of the path.
  • Open settings of VSCode and set "coqtop.binPath": "path/from/previos/step",
  • Restart the VSCode.

You’re ready to go

Congrats!

Now you can be that guy.

pic

If you find a mistake or just want to ask a question, write in the comments!