1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
|
# Proof General — Organize your proofs!
[](https://github.com/ProofGeneral/PG/actions?query=workflow%3ACI)
[](https://melpa.org/#/proof-general)
## Overview
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.5 of Proof General.
## About Proof General branches
Two editions of Proof General are currently available:
* the (standard) REPL-based, stable version of Proof General,
gathered in the
[master](https://github.com/ProofGeneral/PG/tree/master) branch;
* the (unmaintained) Coq-specific, experimental version of Proof General,
supporting asynchronous proof processing,
gathered in the
[async](https://github.com/ProofGeneral/PG/tree/async) branch.
## Installing Proof General
Proof General requires GNU Emacs `25.2` or later.
The current policy aims at supporting multiple Emacs versions,
including those available in [Debian Stable](https://packages.debian.org/stable/emacs)
as well as in [Ubuntu LTS](https://packages.ubuntu.com/emacs) distributions
until their [End-Of-Support](https://wiki.ubuntu.com/Releases).
### 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)
;; (setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3") ; see remark below
(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
(package-initialize)
```
**Remark:** If you have Emacs 26.1 (which is precisely
[the packaged version in Debian 10](https://packages.debian.org/emacs)),
you may get the error message `Failed to download 'melpa' archive`
during the package refresh step. This is a known bug
([debbug #34341](https://debbugs.gnu.org/cgi/bugreport.cgi?bug=34341))
which has been fixed in Emacs 26.3 and 27.1, while a simple workaround
consists in uncommenting the line
`(setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3")` above in your
`.emacs`.
**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
cd ~/.emacs.d/lisp/PG
make
```
Then add the following to your `.emacs`:
```elisp
;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")
```
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
```sh
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:
* [INSTALL](INSTALL) for installation details
* [COPYING](COPYING) for license details
* [COMPATIBILITY](COMPATIBILITY) for version compatibility information
* [FAQ.md](FAQ.md) for frequently asked questions
* [coq/README](coq/README) for additional notes specific to the Coq prover
Links:
* [https://proofgeneral.github.io/doc](https://proofgeneral.github.io/doc) for online documentation of Proof General
* [https://coq.zulipchat.com](https://coq.zulipchat.com/) for chatting with PG maintainers and developers on the Zulip chat of Coq (in streams [Proof General devs](https://coq.zulipchat.com/#narrow/stream/304020-Proof-General.20devs) and [Proof General users](https://coq.zulipchat.com/#narrow/stream/304019-Proof-General.20users))
* [https://coq.gitlab.io/zulip-archive](https://coq.gitlab.io/zulip-archive) for the corresponding public Zulip archive (read-only, no authentication required)
Supported proof assistants:
* [Coq](https://coq.inria.fr/)
* [EasyCrypt](https://www.easycrypt.info/)
* [PhoX](https://raffalli.eu/phox/)
* [qrhl-tool](https://github.com/dominique-unruh/qrhl-tool/#readme)
Proof General used to support other proof assistants, but those
instances are no longer maintained nor available in the MELPA package:
* Experimental support of: Shell
* Obsolete instances: Demoisa
* Removed instances: Twelf, CCC, Hol-Light, ACL2, Plastic, Lambda-Clam, HOL98,
[LEGO](http://www.dcs.ed.ac.uk/home/lego),
[Isabelle](https://www.cl.cam.ac.uk/research/hvg/Isabelle/)
A few example proofs are included in each prover subdirectory.
|
