If you are on Mac OS X or Windows, you can find a binary distribution of Coq (including CoqIDE) on the Coq GitHub repository. If you wish to install through opam, please read below.

First, install opam (at least version 2) using your package manager. Opam is a package manager for OCaml. If the version provided by your distribution is too old, you can also install opam 2.0.7 using the binaries available here.

Then, run the following commands:

opam init # if you have never initialized opam
eval $(opam env)
 
# replace "my-switch-name" by a name of your choice for this opam environment/switch
# 4.11.1 is the version of the OCaml compiler that is going to be used for this switch
opam switch create my-switch-name 4.11.1
eval $(opam env)
 
opam repo add coq-released https://coq.inria.fr/opam/released # add a repository for Coq
opam update # to refresh the list of available packages
opam install coq.8.12.0 # to install Coq version 8.12.0

Add: eval $(opam env) at the end of your ~/.bashrc file. Then open a new terminal and check that coqc --version shows 8.12.0.

There are users interfaces available for Coq. For users of Visual Studio Code, the simplest to install is the VsCoq extension. The extension works quite well, but is not as mature as other options and has some known issues making it annoying to use.

Another easy to install option is CoqIDE (which you can install using opam install coqide), which is a standalone IDE for Coq. It lacks features of other common IDEs, but does the job.

If you want a user interface integrated into an existing IDE, we recommend using the “Emacs + Proof General + Company-Coq” option. We haven't tried other options such as the ones available for vim, but they appear to be actively maintained so you could try them.

If you plan to use Emacs, install Emacs 27.1 and follow the instructions here to install Proof General and Company-Coq using the package manager inside Emacs.

Below are some configurations options that can be helpful, copy the ones you want in your ~/.emacs file.

;; to copy/paste using the usual keys
(cua-mode 1)
 
(defun proof-retract-buffer-stay ()
  "Call proof-retract-buffer, but retain position"
  (interactive)
  (proof-retract-buffer nil)
  )
 
;; Choose the keybindings that you want to step through the proofs.
;; These keys may conflict with Gnome keybindings for switching desktop
;; Use https://askubuntu.com/a/380462 to change the Gnome keybindings, or
;; change the key bindings for Coq below:
(eval-after-load "proof-script" '(progn
  (define-key proof-mode-map (kbd "C-M-<down>") 'proof-assert-next-command-interactive)
  (define-key proof-mode-map (kbd "C-M-<up>") 'proof-undo-last-successful-command)
  (define-key proof-mode-map (kbd "C-M-<left>") 'proof-retract-buffer-stay)
  (define-key proof-mode-map (kbd "C-M-<right>") 'proof-goto-point)
  (define-key proof-mode-map (kbd "C-c C-v") nil)
  ;; choose the color your want for your proofs
  (set-face-background 'proof-locked-face "#a1ffaf")
))
 
(eval-after-load "coq" '(progn
  (set-face-background 'coq-cheat-face "#ffe87a")
  (set-face-foreground 'coq-cheat-face "#ff141d")
))
 
;; forces hybrid mode for displaying Coq buffers
(setq proof-three-window-mode-policy 'hybrid)
 
;; if you want emacs to start maximized
(toggle-frame-maximized)
 
;; if you want to disable emacs splash screen
(setq inhibit-startup-screen t)
 
;; if you want to disable Proof General splash screen
(setq proof-splash-enable nil)
 
;; if you want to disable "electric mode"
(when (fboundp 'electric-indent-mode) (electric-indent-mode -1))
 
;; MELPA repo to install Proof General and company-coq
(require 'package)
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/") t)
 
;; Add these after installing company-coq
(add-hook 'coq-mode-hook #'company-coq-mode)
(setq company-coq-live-on-the-edge t)
 
;; taken from https://gist.github.com/bradwright/2046593
(defun set-exec-path-from-shell-PATH ()
  "Sets the exec-path to the same value used by the user shell"
  (let ((path-from-shell
         (replace-regexp-in-string
          "[[:space:]\n]*$" ""
          (shell-command-to-string "$SHELL -l -c 'echo $PATH'"))))
    (setenv "PATH" path-from-shell)
    (setq exec-path (split-string path-from-shell path-separator))))