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
159
|
Instructions for installing Proof General
=========================================
This file describes what to do to run Proof General.
Please let us know if you have problems trying to install it.
Unpack this 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>.
The command above will set the Emacs load path and add auto-loads for
the assistants below:
.v Coq files
.l LEGO files
.thy,.ML Isabelle files
When you load a file with one of these extensions, the corresponding
Proof General mode will be entered.
In case of difficulty, please check the documentation in doc/, the
notes below, and the file BUGS. If this doesn't help, then contact us
via the address below.
- David Aspinall.
Proof General maintainer <proofgen@dcs.ed.ac.uk>
LFCS,
Division Of Informatics,
University of Edinburgh.
Edinburgh.
http://www.dcs.ed.ac.uk/home/proofgen
----------------------------------------------------------------------
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")
Byte Compilation.
-----------------
Compilation of the Emacs lisp files improves efficiency but can
sometimes cause compatibility problems. It should be okay if you run
with the same version of Emacs that you compiled with. You can
compile Proof General by typing 'make' in the directory where you
installed it. 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 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:
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 notes below for more details.
Notice that the customization mechanism is only available in
Emacs 20.x and XEmacs.
----------------------------------------------------------------------
Notes for Coq
=============
If you want to use this mode for Coq, you need to make sure you have
an appropriate version, which is from later than 1 March 1998.
Check the values of coq-tags and coq-prog-name in coq.el to see that
they correspond to the paths for coqtop and the library on your system.
Install coqtags in a standard place or add <proof-home>/coq to your PATH.
NB: You may need to change the path to perl at the top of the file.
If you are running Coq, generate a TAGS file for the library by running
coqtags `find . -name \*.v -print`
in the root directory of the library, $COQTOP/theories. If you are
running LEGO, do the same using legotags in the appropriate directory.
----------------------------------------------------------------------
Notes for LEGO
==============
Install legotags in a standard place or add <proofgeneral-home>/lego
to your PATH.
NB: You may need to change the path to perl at the top of the file.
----------------------------------------------------------------------
Notes for Isabelle and Isabelle/Isar
====================================
Check the value of isabelle-prog-name.
If you use the interface wrapper scripts isa/interface or
isar/interface, you may need to change the path to bash
on the first line.
The distribution includes a version of Isamode's theory file mode.
Use C-h m to check on the features available.
|
