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
|
Instructions for installing Proof General
=========================================
This file describes what to do to be able to run Proof General.
Please let us know if you have any problems in trying to install it.
Unpack this distribution in some <directory>. Put this line in your
.emacs file:
(load-file "<directory>/elisp/generic/proof-site.el")
This 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.
You cannot run more than one instance of Proof General at a time: so
if you're using Coq, don't edit .ML files! If there are some assistants
supported that you never want to use, you can remove them from
the variable `proof-assistants` in proof-site.el to solve this problem.
In XEmacs, you can do this (and most other customization of Proof
General) via the Customize mechanism, see the menu:
Options -> Customize -> Emacs -> External -> Proof General
Further customization may be needed depending on the proof assistant
(for example, the name of the proof assistant binary). See the
entries below for more notes.
If you are installing Proof General site-wide, you can put the
components in separate directories, 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.
In case of difficulty, please contact us via the address below.
Proof General maintainer <proofgen@dcs.ed.ac.uk>
School of Computer Science,
Division Of Informatics,
University of Edinburgh.
Edinburgh.
http://www.dcs.ed.ac.uk/home/proofgen
----------------------------------------------------------------------
Customization 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.
----------------------------------------------------------------------
Customization for LEGO
======================
Install legotags in a standard place or add <proof-home>/lego
to your PATH.
NB: You may need to change the path to perl at the top of the file.
----------------------------------------------------------------------
Customization for Isabelle
==========================
|
