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
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
|
Developers' Notes about Documentation
-------------------------------------
* Plan for outline of improved documentation. (Completed)
Terminology: I suggest "proof mode" should become "proof script
mode", aka "the proof script mode of Proof General". We should
be careful here, e.g. present docs speak of buffers in proof
mode, etc, but no buffer is directly in that mode, which is
confusing to the users, at least!
1. Introduction [da]
1.1 Quick start guide
1.2 Feature list, xref'd to later chaps.
1.2 Supported Proof Assistants, xref'd too.
Support for new instances, xref'd to later chaps.
2. Basics of script management [da]
2.1 What a proof script is
2.2 Locked region and queue region
2.3 Script processing commands
2.4 Toolbar commands
2.5 Other commands
2.4 Walkthrough example [maybe in appendix?]
3. Advanced script management [done]
3.1 Proof General's view of processed files
3.2 Switching between proof scripts
3.3 Retracting across files
3.4 Handy hints and tips (e.g. C-c C-b stuff?)
3.5 Using the proof shell
[ 3.6 Re-synchronizing with the proof assistant - if added ]
4. Customizing Proof General [da]
4.1 Setting user options, what they are:
proof-splash-inhibit
etc.
4.2 Using proof assistant on another machine
4.3 Examining configuration settings (xref'd later)
5. LEGO Proof General [done]
5.1 LEGO commands
5.2 LEGO customizations
6. Coq Proof General [anon]
6.1 Coq commands
6.2 Coq customizations
7. Isabelle Proof General [da]
7.1 Isabelle commands
7.2 Isabelle customizations
7.3 Notes about multiple files
8. Adapting Proof General to New Provers [da]
8.1 Files and directories. Skeleton code.
8.2 Settings for proof scripts
8.3 Settings for proof shell
-- Special annotations
9. Internals of Proof General. [tms]
9.1 Proof script mode:
- fontification hacks
- spans in locked region
9.2 Proof shell mode
- proof-action-list
- proof-shell-exec-loop
- proof-shell-output-filter
- eager annotations
10. Credits and history [done]
APPENDIX
A. Obtaining and installing the software [da]
B. Known bugs [done]
C. Future ideas and plans [da]
*********
Support for Function Menus
fume-func is a handy package which makes a menu from the function
declarations in a buffer. Proof General configures fume-func so
that you can quickly jump to particular proofs in a script buffer.
If you want to use fume-func, you may need to enable it for
yourself. It is distributed with XEmacs (and FSF GNU Emacs)
but by not enabled by default. To enable it you should find
the file func-menu.el and follow the instructions there.
At the time of writing, the current version of XEmacs is 20.4 and
it has these instructions:
(require 'func-menu)
(define-key global-map 'f8 'function-menu)
(add-hook 'find-file-hooks 'fume-add-menubar-entry)
(define-key global-map "\C-cl" 'fume-list-functions)
(define-key global-map "\C-cg" 'fume-prompt-function-goto)
(define-key global-map '(shift button3) 'mouse-function-menu)
(define-key global-map '(meta button1) 'fume-mouse-function-goto)
If you have any other version of Emacs, you should check the
fume-func.el file
*********
Isabelle with multiple files.
Proper multiple file support only works for .ML files which are read
via the theory loader, with use_thy. If you want to load .ML files
which aren't associated with theories, it's best to use a dummy
theory, see [Reference to Isabelle manual]
*****************************************************************
Notes for writing a paper describing Proof General
-------------------------------------------------
Thesis/introduction
===================
As programming languages have evolved, environments for developing and
debugging programs have also improved. However, discounting various
"visual" programming languages, a program is usually still a piece of
text which can be directly edited by a programmer, a situation which
hasn't changed since the early days when VDUs replaced punched cards.
Similarly, whilst the history of languages for proof assistants is
much shorter, we believe that a proof script, describing the
operations needed to construct a proof, will remain the fundamental
form of input for proof systems.
...
- interactive proof assistants geared to developing proof scripts
interactively, but may not come with integrated editing support.
Problem of shell-like interaction is that input has to be
tediously reassembled after or during proof to get a successful
proof script.
- script management [refs] aims to make this process easier.
Aspects of design
=================
- Generic. Fits inside Emacs architecture. (Compare with comint).
- Extensive use of Emacs Customization mechanism to make it easy
to set/inspect configuration as well as user-options.
- Script management with multiple files
Seen one proof assistant, use them all
======================================
- Same interface for different underlying systems
- Compare: web technology, where "browsing" works for
different protocols: http, ftp, etc
- Anyone can use Proof General to browse and replay proofs from
other systems, without needing to know how to invoke
the system, etc.
- However, proof script language and output remains particular to
each prover. It would be another (interesting) project to attempt to
map input and output into an interchange format for proof systems.
A Specification for a proof assistant interface
===============================================
The settings to instantiate Proof General can be seen as a set of
requirements for a proof assistant interface.
Example of API design guidlines
===============================
1. Use a different prompt for continued lines during input
communication. Helps parsing output.
|
