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
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
|
-*- outline -*-
--- This is a development release of Proof General, ---
--- some features may be incomplete or buggy. Please ---
--- report any problems to da@dcs.ed.ac.uk, thanks. ---
* Summary of Changes for Proof General 3.4pre from 3.3
** Generic Changes
*** Support added for Emacs 21
Toolbar and splash screen supported
[seems good; please tell me of any problems]
Fontification (as ever) is problematic due to changes
in font-lock, and its insiduous self-enabling actions.
Current status: broken in Emacs 20, working in 21.
*** Support for "tracing" buffers improved and enabled by default.
(Support is enabled in Isabelle only so far)
Compared with experimental tracing in PG 3.3, there is now only one
tracing buffer, treated somewhat like a response buffer.
When large volumes of output arrive in Emacs, as typically is the
case during tracing (especially tracing looping tactics!), Emacs
may hog the CPU and spend all its time in the process filter
(especially with X symbol and fontification active). We call this
"choking".
If Emacs is choking, it may not process user events as swiftly as
normal and it can become difficult to interrupt the prover process
ordinarily (with the toolbar Stop button or C-c C-c). As a
workaround, PG will watch for keyboard quits when it's displaying
trace output, and send the prover an interrupt if it sees a quit
has been sent. So you should be able to interrupt with C-g during
choking.
If the choking effect slows down your prover too much by giving
Emacs too much CPU, disabling output fontification by customizing
`proof-output-fontify-enable' may help.
** Isabelle Changes
Isabelle/Isar syntax changes.
-----------------------------------------------------------------
OLDER CHANGES
=============
* Summary of Changes for Proof General 3.3 from 3.2
** Generic Changes
*** Visibility control for completed proofs
You can make proofs invisible using a context sensitive menu
(right button on a completed proof), or as soon as they are
completed with the "Options -> Disappearing Proofs" option.
Two menu items "Show proofs" and "Hide proofs" apply to
all the completed proofs in the buffer.
NB: proofs of theorems with the same name are not
distinguished, their visibility is controlled together.
*** Command to insert last output as comment in proof script.
Sometimes it is useful to paste some of the output from
goals or response buffer into the proof script. A new
function `pg-insert-last-output-as-comment' (C-c C-;)
inserts the last output and converts it into a comment
using `comment-region'.
*** Changes to colours, mouse highlighting, echo help messages
Now `proof-locked-face' becomes a lighter cyan. This is
less obtrusive when editing proofs, but is not so visible
for demonstrating PG: if you prefer the old stronger colour,
customize the face to "lightsteelblue2" using
M-x customize-face RET proof-locked-face.
New face `proof-mouse-highlight-face' (default: darker blue
than locked region) is now used for mouse highlighting regions of
script. Less ugly than the previous default (green) highlight face.
Also, for XEmacs, there are now (trivial) help messages in echo
area describing the highlighted region under the mouse.
*** Experimental features and new user option
There's a new user option `proof-experimental-features' which
is nil by default. If you set it to t, you will (maybe after
restarting Proof General) enable certain experimental features.
In this release, the experimental features are:
Context menu options to move spans up/down
Context menu dependency commands (Isabelle only, see below)
To customize this from the menu:
Proof General -> Customize -> User Options -> Experimental features
*** Proof General startup script welcomes user
The "binary" (startup script) bin/proofgeneral now loads
PG and invokes a function to display a splash message,
which invites the user to load a file. A bit more
friendly than simply being confronted by a standard
XEmacs screen.
*** Changes to Proof General RPM packaging mechanism
Can now build RPM packages with "rpm -ta" from tarball source.
RPM includes menu file and icons so that Proof General may
appear on your window system menus (tested under Linux Mandrake).
We no longer distribute an SRPM.
*** Compatibility fixes.
Fixes for FSF Emacs and XEmacs 21.4
Better support for win32 versions of XEmacs (see README.windows).
Fixes for recent version 3.3g of X-Symbol (and note on
web page about using ~/.xemacs/xemacs-packages/ for install locn).
*** Bug fixes.
XEmacs 21.1 has faulty implementation of buffer-syntactic-context,
workaround added. (Symptom was parsing breaking, giving unexpected
"I can't see any complete commands to process!" error message, esp
with strings broken across lines containing parentheses).
Fixed Emacs-confusion minibuffer contents switching bug. (Bug
was triggered by using toolbar while minibuffer active).
** Coq Changes
Compatibility for V7 added.
Experimental enhancements to handling of compiled files and
file dependency. (Only tested with Coq 6.3.1: we need help
from Coq implementors to add primitive support in V7, please
appeal to them to help Proof General!).
1) At the end of scripting foo.v (i.e. when activing scripting is
switched off), "Reset Initial. Compile Module <foo>" is
automatically issued. This clears the context and writes a .vo file,
to keep your .vo files up to date. It means that when using PG Coq,
you should use the correct commands ("Require foo.") to load all
the modules you depend on, so that scripting can continue in the
next file.
2) PG tracks file dependencies by noticing "Reinterning" messages
from Coq. When a file "b.v" is processed which has a "Require a",
command, PG will try to find "a.v" and will automatically lock
it. (This part of the process is fragile, for two reasons: it
is hard to find the directory for a.v, since Coq doesn't report
it, and the reinterning message is only issued the first time the
file is reinterned).
3) When a file is retracted, PG attempts to automatically unlock
all the dependent files, by issuing a coqdep command to determine
the dependencies. (This is a rather nasty hack, it's hoped for
the future that Coq will support this functionality directly).
This functionality is enabled with the Coq settings option
"Auto Compile Vos".
Whole goals output is displayed. (Improvement suggested by
Robert Schneck).
** Isabelle Changes
Support for theorem dependency tracking: context-sensitive menu
(right button on a completed proof) provides a facility for browsing
the ancestors and child theorems of a theorem, and highlighting them.
The idea of this feature is that it can help you untangle and
rearrange big proof scripts, by seeing which parts are
interdependent.
This facility is not yet closely integrated with Isabelle and
relies on an auxiliary ML file which is only compatible with
Isabelle99-2. It is only supplied for Isabelle/classic.
To activate the feature, use the Isabelle setting option "Theorem
Dependencies." Notice that you need to switch this on *after*
starting an Isabelles session, and must switch on/off on every
restart. (This behaviour will improve once better integrated
with Isabelle).
NB this is classed as an experimental feature, so you must set
proof-experimental-features to enable it.
Not yet documented. Comments and suggestions welcome.
** Changes for developers to note
*** proof-shell-process-output now sets proof-shell-last-output and
proof-shell-last-output-kind which gives clearer interface internally
and with rest of code. See docs.
*** Support for "tracing" buffers added.
This was added for Isabelle's simplifier tracing, when a large
amount of output is produced during a proof for debugging.
The user would rather see the output as it arrives than wait
for a long time.
Experimental stage and not yet enabled for any prover.
See proof-shell-spill-output-regexp.
|
