What is Proof General?
Proof General is a generic frontend for proof assistants (also known as interactive theorem provers), based on the customizable text editor Emacs. Proof General has been developed at the LFCS in the University of Edinburgh with contributions from other sites. It is distributed under the conditions of the GNU General Public License. The manager and main developer is David Aspinall. Other contributors are listed below and in the AUTHORS file.
Proof General offers a full support for latest versions of the Coq proof assistant:

Coq Proof General,
for Coq
by Healfdene Goguen, Patrick Loiseleur, David Aspinall, and Pierre Courtieu.
Proof General also supports previous versions of the following other proof assistants:

Isabelle Proof General,
for Isabelle (up to Isabelle2014)
by David Aspinall and Makarius. 
PhoX Proof General,
for PhoX
by Christophe Raffalli, Paul Roziere and JeanRoch Sotty.  LEGO Proof General, for LEGO
 HOL Proof General, for HOL98/HOL4
 ACL2 Proof General, for ACL2
These instances may be incomplete or not work with the latest theorem prover versions.
Proof General is ready to be customized to new proof assistants. It can be very easy to get basic support working. Full documentation on configuration is provided. We welcome offers to support, extend and improve Proof General instances. Please get in touch if you plan major work.
If you are considering supporting (or implementing) a new prover, please read about the Proof General Kit architecture. The idea is that proof assistants should support PGIP, a uniform protocol for interaction, rather than use systemspecific customization inside interfaces. The main research prototype using PGIP is an experimental Eclipse plugin, although Emacs Proof General supports some PGIP configuration.
Quick installation instructions
Remove old versions of Proof General, then download and install the new release from GitHub:
git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
cd ~/.emacs.d/lisp/PG
make
Then add the following to your .emacs
:
;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proofsite")
If Proof General complains about a version mismatch, make sure that the shell’s emacs
is indeed your usual Emacs. If not, run the Makefile again with an explicit path to Emacs. On macOS in particular you’ll probably need something like
make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs
For more information, see the README and INSTALL files on the GitHub repo.