README.md: Update installation instructions

1 files changed, 53 insertions, 2 deletions

diff --git a/README.md b/README.md
index d5d99d91..491f600a 100644
--- a/README.md
+++ b/README.md
@@ -24,9 +24,41 @@ Two editions of Proof General are currently available:
   [async](https://github.com/ProofGeneral/PG/tree/async) branch, and
   licensed under GPLv3+.
 
-## Setup
+## Installing Proof General
 
-Remove old versions of Proof General, then download and install the new release from GitHub:
+### Using MELPA (recommended procedure)
+
+[MELPA](https://melpa.org/) is a repository of Emacs packages. Skip
+this step if you already use MELPA. Otherwise, add the following to
+your `.emacs` and restart Emacs:
+
+```elisp
+(require 'package)
+(let* ((no-ssl (and (memq system-type '(windows-nt ms-dos))
+                    (not (gnutls-available-p))))
+       (proto (if no-ssl "http" "https")))
+  (add-to-list 'package-archives
+               (cons "melpa" (concat proto "://melpa.org/packages/")) t))
+(package-initialize)
+```
+
+**Note:** If you switch to MELPA from a previously manually-installed
+Proof General, make sure you removed the old versions of Proof General
+from your Emacs context (by removing from your `.emacs` the line
+loading `PG/generic/proof-site`, or by uninstalling the proofgeneral
+package provided by your OS package manager).
+
+Then, run <kbd>M-x package-refresh-contents RET</kbd> followed by
+<kbd>M-x package-install RET proof-general RET</kbd> to install and
+byte-compile `proof-general`.
+
+You can now open a Coq file (`.v`), an EasyCrypt file (`.ec`), or a
+PhoX file (`.phx`) to automatically load the corresponding major mode.
+
+### Using Git (manual compilation procedure)
+
+Remove old versions of Proof General, clone the PG repo from GitHub
+and byte-compile the sources:
 
 ```sh
 git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
@@ -47,6 +79,25 @@ If Proof General complains about a version mismatch, make sure that the shell's
 make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs
 ```
 
+## Keeping Proof General up-to-date
+
+### Using MELPA
+
+As explained in the [MELPA documentation](https://melpa.org/#/getting-started), updating all MELPA packages in one go is as easy as typing
+<kbd>M-x package-list-packages RET</kbd> then <kbd>r</kbd> (**r**efresh the package list), <kbd>U</kbd> (mark **U**pgradable packages), and <kbd>x</kbd> (e**x**ecute the installs and deletions).
+
+### Using Git
+
+Assuming you have cloned the repo in `~/.emacs.d/lisp/PG`, you would
+have to run:
+
+```sh
+cd ~/.emacs.d/lisp/PG
+make clean
+git pull
+make
+```
+
 ## More info
 
 See: