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
|
Compatibility of Proof General
==============================
This version of Proof General has been tested with these Emacs versions
on recent Linux systems:
Emacs 22.2.1 -- recommended and supported
Emacs 23.0.X -- CVS/beta snapshots, use time of PG release
Emacs 21.4.1 -- tested; poorer X-Symbol sub/superscript support
XEmacs 21.5 (beta28) -- tested; PG has workarounds for several bugs
XEmacs 21.4.XX -- tested
and (main) prover versions:
Coq 8.0, 8.1
Isabelle2005, Isabelle2007, Isabelle2008
See below for notes about other operating systems.
Maintaining compatibility across proof assistant versions, Emacs
versions and operating systems is virtually impossible. Backward
compatibility has to be sacrificed. Some old version compatibility
has been removed here, specifically affecting:
Coq 7
Isabelle 2004
Earlier buggy versions of GNU Emacs 21
*******************************************************************
*** IMPORTANT NOTE: XEmacs compatibility may be dropped soon, ***
*** switching to GNU Emacs is recommended. ***
*******************************************************************
Running on Windows
------------------
For tips, please see here:
http://proofgeneral.inf.ed.ac.uk/wiki/PG/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 thoroughly tested by the
maintainers. If you discover problems, please send a report and/or
fix to the address above.
Running on Mac OS X
-------------------
For tips, please see here:
http://proofgeneral.inf.ed.ac.uk/wiki/PG/PGEmacsOnMacOSX
We recommend the 22.X based Carbon Emacs, here:
http://homepage.mac.com/zenitani/emacs-e.html
This works with X-Symbol using the supplied TrueType font
x-symbol/etc/fonts-ttf/XSymb1.ttf, which you should install in Font
Book, or copy directly to /Library/Fonts or ~/Library/Fonts.
Note: Emacs.app looks set to become the future supported Mac port of
GNU Emacs, but being based on GNU Emacs 23, it has recently become
incompatible with X-Symbol because of API changes. (A fix would be
welcome; may be simple). If you do not care about X-Symbol, or
can use the Unicode Symbols mode, Emacs.app works just as well.
Note that Mac compatibility isn't thoroughly tested by the
maintainers. If you discover problems, please send a report and/or
fix to the address above.
|
