From c8a4896b54a89385b0a7a539be952c3dc3493821 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 30 Aug 2018 11:51:04 +0200 Subject: README.md: Update installation instructions --- README.md | 55 +++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file 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 M-x package-refresh-contents RET followed by +M-x package-install RET proof-general RET 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 +M-x package-list-packages RET then r (**r**efresh the package list), U (mark **U**pgradable packages), and x (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: -- cgit v1.2.3 From 461417d3ecced06f67f8fd535e4028174069b3cc Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 30 Aug 2018 13:06:54 +0200 Subject: Update the section of supported PAs --- README.md | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 491f600a..bf6fdae5 100644 --- a/README.md +++ b/README.md @@ -115,12 +115,17 @@ Links: Supported proof assistants: -* Full support for latest versions of: [Coq](https://coq.inria.fr/) -* Support for previous versions of: - [Isabelle](http://www.cl.cam.ac.uk/research/hvg/Isabelle/), - [LEGO](http://www.dcs.ed.ac.uk/home/lego), - [PhoX](http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html) -* Experimental (less useful): CCC, ACL2, HOL98, Hol-Light, Lambda-Clam, Shell, Twelf +* [Coq](https://coq.inria.fr/) +* [EasyCrypt](http://www.easycrypt.info/) +* [PhoX](http://www.lama.univ-savoie.fr/pagesmembres/raffalli/phox.html) + +Proof General used to support other proof assistants, but those +instances are no longer maintained nor available in the MELPA package: + +* Legacy support of + [Isabelle](http://www.cl.cam.ac.uk/research/hvg/Isabelle/) and + [LEGO](http://www.dcs.ed.ac.uk/home/lego) +* Experimental support of: CCC, ACL2, HOL98, Hol-Light, Lambda-Clam, Shell, Twelf * Obsolete instances: Demoisa, Lambda-Clam, Plastic A few example proofs are included in each prover subdirectory. -- cgit v1.2.3 From ff1cb6c2c355082076d99de1f560fa0c4bbcd86c Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 30 Aug 2018 21:01:06 +0200 Subject: Add MELPA badge --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index bf6fdae5..95c73b43 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,7 @@ # Proof General — Organize your proofs! [![Build Status](https://travis-ci.org/ProofGeneral/PG.svg?branch=master)](https://travis-ci.org/ProofGeneral/PG) +[![MELPA](http://melpa.org/packages/proof-general-badge.svg)](https://melpa.org/#/proof-general) ## Overview -- cgit v1.2.3