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
|
Summary of Changes for Proof General 3.0 from 2.1
=================================================
Generic Changes
---------------
* The excellent X-Symbol package is now well supported by
Proof General. This allows proof assistants to display logical
symbols, Greek letters, etc, with ease. The original patches
for Isabelle are courtesy of David von Oheimb. There are
early experimental configurations provided for LEGO and Coq
which use ordinary character sequences rather than escaped
tokens (so "/\" appears as a wedge, and "Gamma" appears
as the letter Gamma). You may need to install X-Symbol first;
visit http://www.fmi.uni-passau.de/~wedler/x-symbol
* Demonstration instance of Proof General for Isabelle shows
how you can get the interface going with a minimum of fuss.
It has less than 30 simple settings.
* Proof General is now more cany about the queue of commands.
You can now add more proof commands on the end of the queue,
without the "Proof Process Busy" message.
* New function C-c C-f (proof-find) to invoke some prover-specific
mechanism to search for theorems.
* Whenever scripting is triggered in a new file, a cd command
is sent to the proof assistant to switch to the right directory
(in case other files are included).
* [XEmacs only] Toolbar has six new buttons (State, Context, Info,
Command, Help, Stop) which invoke commands previously available on
keys/menus. Also a new "Find" button for proof-find.
* [XEmacs only] Toolbar enablers have been added.
Buttons are automatically enabled or disabled as appropriate.
This requires XEmacs 21 or better for reliable working,
so is disabled for earlier versions.
If you do not like enablers, you can turn them off with
the new configuration variable proof-toolbar-use-enablers.
With this variable nil, buttons do nothing when they
otherwise be disabled.
* Menus and keybindings have been reorganized.
Bindings C-c <letter> are being phased out; they are supposed
to be reserved for the user according to Emacs convention.
* Keybindings for assert/retract now invoke the same functions as the
toolbar. In particular, C-c C-n and C-c C-u are simplified so that
they always process or retract exactly one command, rather
than one command beyond point. Moreover, C-c C-u does not
take an optional argument to delete the retracted text
(it was too easy for the user to accidently type C-u C-c C-u !)
* New command C-c C-RET proof-goto-point which generalises
previous proof-assert-until-point to also do retracting if
point is in the locked region.
* User options have been re-organized and renamed to be
more suggestive. Boolean options can be
toggled from the menu and saved with "Save options"
on the ordinary Emacs "Options" menu. (Others can
be set via Customize).
* "Active terminator minor mode" is now called "electric
terminator". It has one setting for all buffers, and
you can customize it if you want it permanently on.
* Command C-c C-t (proof-try-command) removed in favour of
C-c C-v (proof-execute-minibuffer-cmd), which now uses the
filter proof-state-preserving-p to check that a command is safe.
* Terminal string now automatically added to command for C-c C-v
* [XEmacs only]
New function control-button1 (proof-mouse-track-insert) copies
individual commands (highlighted regions) from an open proof.
When a proof is closed, it behaves as mouse-track-insert
(the default XEmacs behaviour of control-button1).
* Switching scripting buffers is now more flexible.
When scripting is turned off in a partly-finished buffer,
the user is prompted whether to retract or process the buffer.
Automatic retraction or completion can be selected by
configuring the option proof-auto-action-when-deactivating-scripting.
(To be compatible with the file operations in a proof assistant,
Proof General only allows completely processed or completely
unprocessed scripts in non-active buffers).
* New function C-c C-s (proof-toggle-active-scripting) to switch
scripting on or off in current buffer. This is a handy way to
discard or finish off scripting in an unfinished buffer
triggering the deactivation mechanism mentioned above.
Switching on scripting in a buffer may cause the proof
assistant to load files it depends on, so it is also handy
to see what happens before scripting begins in the buffer.
* Proof by pointing has been re-enabled in the code.
LEGO's implementation of the proof-by-pointing rule choices
is dodgy, but works sometimes, and it is nice to demonstrate
Proof General's support for pbp until another prover implements
it. (It should be relatively straightforward to implement for Coq,
since the CtCoq pbp code is now embedded in the core system; we need
a Coq expert to do this).
* Cleaned up example files so all demonstrate same theorem "conj_comms".
Would be nice to add more theorems to compare scripts/proofs in
different systems. Please send in example scripts!
* Shorter buffer names for convenience.
* Removed transparent gif (text logo) from splash screen
because XEmacs can't display it nicely.
* Documentation updates.
Coq Changes
-----------
* Set proof-{qed,save}-commands so the toolbar functions work.
* Generic command C-c C-f (proof-find-theorems) replaces Coq
specific command C-c C-s (coq-Search).
LEGO Changes
------------
* Proofs which have no save command are now closed off automatically
when another command arrives, so undo-redo is more flexible.
Isabelle and Isar Changes
-------------------------
* Several tweaks for input syntax.
* Recognize goals of the old form val prems = goal ...
and saves of the old form val thm = result.
* Proofs which are "unfinished", i.e. have no qed or result,
are now closed off automatically, mirroring the behaviour
of Isabelle. This does not apply to Isar.
* Confusing display of only last error is fixed: multiple
error messages are now coalesced properly.
Only in the developers' release
-------------------------------
* Provisional instantiation of Proof General for
Plastic (http://www.dur.ac.uk/CARG/plastic.html)
by Paul Callaghan <P.C.Callaghan@durham.ac.uk>.
Internal changes for developers to note
---------------------------------------
* x-symbol support has been made generic. See documentation
and proof-config.el.
* Many robustness improvements so that Proof General fails
gracefully when certain configuration settings are unset.
The aim is to make it easier to adapt to new proof
assistants.
* A new setting proof-completed-proof-behaviour allows for
more flexible ways of managing goal...save regions, including
automatically closing them when the first command after
the proof is completed arrives. This means we can handle
proof assistants which do not have an explicit save command
now. See the documentation of proof-completed-proof-behaviour.
* Renamed several configuration variables for uniformity.
Check the ChangeLog for details.
* Speed optimizations for the proof-shell-filter, to attempt
to give more CPU to a hungry and noisy proof process.
To help with this there is a new configuration variable
proof-shell-eager-annotation-start-length.
* proof-site now does nothing if it has already been loaded.
Previously it would load again, possibly altering settings.
* Multiple file handling improvements:
Added proof-shell-inform-file-processed-cmd setting to
tell the prover about files which are processed completely
inside Proof General.
This is called when scripting is turned off inside a completely
processed buffer.
Added proof-shell-inform-file-retracted-cmd setting for
symmetric case: to tell the prover when files which are to be
considered *not* completely processed inside Proof General.
The is called when scripting is turned on inside a completely
processed buffer (as the conceptual state of the buffer changes
to partly-processed).
* proof-shell-leave-annotations-in-output variable has been added.
This allows quick and dirty mark up of output from the proof
assistant using special characters with codes above 128 and
font-lock. Such characters are removed from display in the
output buffers.
However, it is NOT recommended to use this mechanism heavily,
because the entire mechanism of using 8 bit character codes as
"special" characters is fragile and needs replacing in future
versions of Proof General!
* proof-font-lock-zap-commas has been added to control whether
or not the excrutiating font-lock hack to unhighlight commas
is enabled.
* Many code cleanups and improvements.
|
