Update README

3 files changed, 42 insertions, 33 deletions

diff --git a/COMPATIBILITY b/COMPATIBILITY
index 6af37517..4bf5de0b 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -4,21 +4,17 @@ Compatibility of Proof General
 This version of Proof General has been tested with these Emacs versions
 on recent Linux systems:
 
- Emacs 23.4             -- recommended and supported
- Emacs 23.3,23.2        -- previous versions, should work
- Emacs 24 (development) -- next version, should work
- Emacs 23.1, earlier    -- obsolete versions, do NOT work
+ Emacs 24.5          -- recommended and supported
+ Emacs 24.3, 24.4    -- previous versions, should work
+ Emacs 25 (dev)      -- next version, should work
+ Emacs 23.2, earlier -- obsolete versions, do NOT work
 
-and (main) prover versions:  Coq 8.3, Isabelle2011[-1]
+and (main) prover versions:  Coq 8.4, Coq 8.5
 
 See below for notes about other operating systems.
 
-Maintaining compatibility across proof assistant versions, Emacs
-versions and operating systems is virtually impossible.  
-
 In the major 4.0 release ** XEmacs compatibility was dropped **
 
-
 Running on Mac OS X
 -------------------
 
@@ -26,14 +22,14 @@ For tips, please see here:
 
    http://proofgeneral.inf.ed.ac.uk/wiki/PGEmacsOnMacOSX
 
-We recommend the 23.2 build of GNU Emacs, which builds natively on Mac
+We recommend the 24.5 build of GNU Emacs, which builds natively on Mac
 OS X (based on the NextStep port).  Binaries are available at various
 websites (e.g., http://emacsformacosx.com), or you can build your own
 by compiling from the FSF CVS. See the Emacs Wiki at
 http://www.emacswiki.org/emacs/EmacsForMacOS for more.
 
 Note that Mac compatibility isn't thoroughly tested.  If you discover
-problems, please send a report and/or fix to the PG trac.  Please
+problems, please send a report and/or fix to the PG tracker.  Please
 add tips to the wiki page above.
 
 
@@ -44,19 +40,6 @@ For tips, please see here:
 
    http://proofgeneral.inf.ed.ac.uk/wiki/PGEmacsOnWindows
 
-We recommend EmacsW32 available at:
-
-   http://www.ourcomments.org/Emacs/EmacsW32.html
-
-Unpack the Proof General tar or zip file, and rename the folder to
-"ProofGeneral" to remove the version number.  Put a line like this:
-
-   (load-file "c:\\ProofGeneral\\generic\\proof-site.el")
-
-into .emacs.  You should put .emacs in value of HOME if you set that,
-or else in directory you installled Emacs in, e.g.  
-c:\Program Files\Emacs\.emacs
-
 Note that Windows compatibility isn't tested by the maintainers.  If
 you discover problems, please add notes on the Wiki page above, and
 submit patches to http://proofgeneral.inf.ed.ac.uk/trac
diff --git a/INSTALL b/INSTALL
index 92ba16ca..31331c2f 100644
--- a/INSTALL
+++ b/INSTALL
@@ -1,3 +1,18 @@
+From GitHub
+===========
+
+Download and install Proof General from GitHub:
+
+  git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
+  make -C ~/.emacs.d/lisp/PG
+
+Then add the following to your .emacs:
+
+  ;; Open .v files with Proof General's Coq mode
+  (require 'proof-site "~/.emacs.d/lisp/PG/generic/proof-site")
+
+This should be enough. Instructions for previous releases are below.
+
 Short Instructions for installing Proof General (details below)
 ===============================================================
 
diff --git a/README b/README.md
index d60f4d78..c508bcf1 100644
--- a/README
+++ b/README.md
@@ -1,16 +1,28 @@
-	    Proof General --- Organize your proofs! 
+# Proof General — Organize your proofs! 
 
 Proof General is a generic Emacs interface for proof assistants.
 The aim of the Proof General project is to provide a powerful, generic
 environment for using interactive proof assistants.
 
-This is version 4.2 (prerelease) of Proof General.  See About for exact version.
-It is built for Emacs 23.3.
+This is version 4.4 of Proof General.
 
-The code *may* also work with previous emacs versions, back as far as
-Emacs 22.3.  But you will need to regenerated the byte-compiled files
-with "make clean; make compile".  Backward compatibility cannot be
-guaranteed.
+## Setup
+
+Download and install Proof General from GitHub:
+
+```
+git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
+make -C ~/.emacs.d/lisp/PG
+```
+
+Then add the following to your .emacs:
+
+```
+;; Open .v files with Proof General's Coq mode
+(require 'proof-site "~/.emacs.d/lisp/PG/generic/proof-site")
+```
+
+## More info
 
 See
     INSTALL	     for installation details.
@@ -18,12 +30,11 @@ See
     COMPATIBILITY    for version compatibility information.
     REGISTER	     for registration information (please register).
     FAQ, doc/	     for documentation of Proof General.
- 
+
     <prover>/README  for additional prover-specific notes
 
 Links:
 
-    Bug/feature reports:  http://proofgeneral.inf.ed.ac.uk/trac 
     Wiki:		  http://proofgeneral.inf.ed.ac.uk/wiki
     Lists:		  http://proofgeneral.inf.ed.ac.uk/mailinglist