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
147
148
149
150
151
152
153
154
155
156
157
158
|
Instructions for installing Proof General
=========================================
Proof General runs on a variety of platforms and with a variety of
Emacs versions; see notes below for particular hints. Please send us
additional hints for alternative platforms/Emacsen not mentioned.
To install, unpack the distribution somewhere. It will create a
top-level directory containing Proof General, called
Proof-General-<something>. Put this line in your .emacs file:
(load-file "<proofgeneral-home>/generic/proof-site.el")
Where <proofgeneral-home> is replaced by the full path name to
Proof-General-<something>. If you prefer not to edit .emacs,
you can use the script in bin/proofgeneral to launch Emacs with
Proof General loaded.
The command above will set the Emacs load path and add auto-loads for
proof assistants, for example, visiting a file ending in .v will start
Coq Proof General, and a file ending in .thy will start
Isabelle/Isar Proof General. See the manual for a full list of file
extensions and proof assistants, and the note below for how to disable
those you don't need.
In case of difficulty, please check the documentation in doc/, the
notes below, the README file for each prover, and the file BUGS.
If none of these files help, then contact us via the address below.
Proof General maintainer <support@proofgeneral.org>
LFCS,
Division Of Informatics,
University of Edinburgh.
Edinburgh.
http://www.proofgeneral.org
----------------------------------------------------------------------
Detailed installation Notes for Proof General
=============================================
RPM package.
------------
If you have the RPM file, this is the line you should add to your
.emacs file:
(load-file "/usr/share/emacs/ProofGeneral/generic/proof-site.el")
Running on Windows
------------------
We recommend XEmacs compiled for Windows, see http://www.xemacs.org.
Some Isabelle users have reported better operation with cygwin XEmacs.
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 XEmacs in, e.g.
c:\Program Files\XEmacs\.emacs
Dependency on Other Emacs Packages
----------------------------------
Proof General relies on several other Emacs packages, which are
probably already supplied with your version of Emacs. If not, you
will need to find them. XEmacs is sometimes unbundled, so you may
need to select packages (or package groups) specially. These are the
packages that you need to use Proof General:
ESSENTIAL:
* cl-macs
* comint
* custom
* font-lock
OPTIONAL:
* outline
* func-menu
* X Symbol
Byte Compilation.
-----------------
Compilation of the Emacs lisp files improves efficiency but can
sometimes cause compatibility problems. It is not properly supported
in this release, because testing for these compatibility problems
takes too much time. If you want to experiment nonetheless, you can
compile Proof General by typing 'make' in the directory where you
installed it. This will result in lots of warnings and error messages
most of which can be ignored. Some files cannot be properly
byte-compiled at the moment because they contain settings which depend
on run-time; these will be deleted by the Makefile. Use 'make clean'
to remove all .elc files in case of problems. Check the Makefile sets
EMACS to your Emacs executable.
Site-wide Installation
----------------------
If you are installing Proof General site-wide, you can put the
components in the standard directories of the filesystem if you
prefer, providing the variables in proof-site.el are adjusted
accordingly. Make sure that the generic and assistant-specific elisp
files are kept in subdirectories of `proof-home-directory' so that the
autoload directory calculations are correct.
To save every user needing the line in their .emacs file, you can put
that into a site-wide file like default.el. Read the Emacs manual for
details.
Removing support for unwanted provers
-------------------------------------
You cannot run more than one instance of Proof General at a time in
the same Emacs process: e.g. if you're using Coq, you won't be able to
run LEGO scripts.
If there are some assistants supported that you never want to use, you
can remove them from the variable `proof-assistants' to prevent Proof
General autoloading for files with particular extensions. This may be
useful if you want to use other modes for those files, for example,
you may want sml-mode for .ML files or Verilog mode for .v files.
The easiest way to do this (and other customization of Proof General)
is via the Customize mechanism, see the menu:
Options -> Customize -> Emacs -> External -> Proof General
or, after loading Proof General, in a proof script buffer
Proof-General -> Customize
You may need extra customization depending on the proof assistant (for
example, the name of the proof assistant binary). See the menu
Proof-General -> Customize -> <Name of Assistant>
and the manual for more details.
$Id$
|
