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
226
227
228
229
230
231
232
233
234
235
236
|
-*- outline -*-
--- This is a development release of Proof General, ---
--- some features may be incomplete or buggy. Please ---
--- report any problems to da+pg-support@inf.ed.ac.uk ---
--- thanks. Check files BUGS and <prover>/BUGS first. ---
* Summary of Changes for Proof General 3.5pre from 3.4
** Generic changes
*** Improved display management
The display handling functions have been overhauled to cope with
latest API changes and diversions between Emacs versions. Multiframe
mode should now work on both Emacs versions, with cut-down frames (no
toolbars, etc). There is a new user-level function
`proof-layout-windows' which displays windows in a default form for
the current display mode. This uses a vertical-horizontal split
scheme for three-pane mode (due to Pierre Courtieu), but three-pane
mode also works with three-way horizontal split as before.
*** Improved RPM packaging
Three packages are provided: ProofGeneral, ProofGeneral-emacs-elc and
ProofGeneral-xemacs-elc. The two elc RPMs contain compiled elisp for
GNU Emacs and XEmacs respectively. These RPMs are intended to be
compatible with the RPMs distributed with Red Hat/Fedora.
Please try out these packages and report any problems.
*** Desktop integration on freedesktop.org compliant desktops
Provided automatically (and only) with the RPM package.
WORK IN PROGRESS!! -- Please send me i18n strings, and report
any problems on particular desktops
(I'm only testing on Fedora Core 1/GNOME).
*** Keyboard hints and other messages displayed in minibuffer
Hints for keyboard usage and reporting on file processing are now
displayed in the minibuffer. If you do not like this behaviour,
customize the `pg-show-hints' variable.
*** pre-compiled .elc files: recompile needed for GNU Emacs
Proof General can now be reliably run as compiled code.
>>> Please help remove any final difficulties by reporting problems <<<<
However, compiled Emacs Lisp files sometimes have incompatibilities
between versions (and definitely between GNU Emacs and XEmacs). To
recompile the sources for a particular Emacs version, try:
make clean
make compile
Check the settings in the Makefile for your Emacs version.
*** Bundling of X-Symbol Mode (4.5.1-beta)
!!THIS IS WORK IN PROGRESS, IT MAY WELL BREAK X-SYMBOL FOR YOU!!
[ Currently should be working in Isabelle, perhaps not other provers ]
To disable use of the bundled version, either delete/move away the
x-symbol subdirectory, or load your own local version first [put
(require 'x-symbol-hooks) in .emacs, or unpack in your own .xemacs
directory].
From now on, PG is not backward compatible with previous X-Symbol
versions. Either upgrade your installed version, or be careful to
load PG first (so that the bundled version of X-Symbol is used).
Notice that the package version of X-Symbol may load itself first by
default during XEmacs startup (especially if you have it installed
site-wide), so it may be tricky to override. You can prevent this
with "xemacs -no-autoloads", but that may result in other needed
packages not being loaded! There seems to be no good way around this
provided in XEmacs. In case of problems, consult your sysadmin to try
to prevent global loading of x-symbol.
*** Bundling of MMM Mode (for multiple modes in one buffer)
MMM mode allows submodes to be used in the same file.
See http://mmm-mode.sourceforge.net/.
At present it is configured for Isar, to allow LaTeX and sml-mode to
be used inside Isar scripts. Contributions of configuration for other
provers welcomed.
*** X-Symbol (and MMM-mode) minor mode behaviour simplified
These minor modes like to be responsible for turning themselves on and
off. PG does not anymore try to synchronise the on/off settings in
all PG buffers (which could lead to half an hour of fontification!).
Instead the menu reflects the current minor mode status; toggling it
will also update the default "global for PG" behaviour for new script
buffers.
*** Movement of cursor on interrupt is disabled
By default, the cursor jumps to the end of the locked region on an
error. Previously it also jumped on an interrupt. This is configurable
via `proof-shell-handle-error-or-interrupt-hook', which see.
*** Automatic slow-down on fast tracing display
Proof General will try to configure itself to update the display of
tracing output infrequently when the prover is producing rapid,
perhaps voluminous, output. This counteracts the situation that
otherwise Emacs may consume more CPU than the proof assistant, trying
to fontify and refresh the display as fast as output appears.
See `proof-trace-output-slow-catchup' for setting.
*** Proof General -> Options menu changes
**** Improvement to options handling
Facility to reset to default values added, and saving
of (just) proof assistant settings.
**** Strict read only added
Strict read only behaviour for the locked (blue) region
can now be enabled/disabled without restarting scripting.
(Output hightlighting option has been removed from this menu,
but is still available under
Advanced -> Customize -> User Options -> ..
**** Deactivate Action added
This setting controls an automatic action when scripting is
deactivated in a partially processed buffer. Ordinarily, PG will
query whether to retract or completely process the file.
One of these can be chosen as a default action.
**** Follow mode: add "followdown" setting
In this mode, the point moves with the locked region when it moves
down in the buffer (processing). For undo, the point does not move.
**** Display management: added shrink-windows-tofit option
This option shrinks and expands the display of prover output,
within reasonable window sizes, when in 2-window mode. It avoids
wasting half the screen with empty space (with the drawback
of moving the boundary up and down).
Available under PG -> Options -> Display -> Shrink To Fit.
*** Add proof-indent-pad-eol setting to prettify locked regions in XEmacs.
This works by adding unnecessary spaces to the end of lines when TAB
is pressed.
*** Parsing internals changed: minor user visible differences
Please report any problems/annoyances which may be unexpected.
NB: Not yet enabled for Isabelle/Isar.
*** Tweaks to menus, colours
Electric terminator menu option more visible.
Reduce contrast for mouse highlighting of regions.
*** Added `proof-shell-identifier-under-mouse-cmd'
Allows PG to conveniently send a command to the prover which passes
the identifier under the mouse, or the active region, as an argument.
Bound globally to Control-Meta-Mouse-button1.
Presently only configured in Isabelle/Isar, to parse terms (inside
strings) and theorems (outside).
** GNU Emacs compatibility, simplified font-lock, handling nested comments
*** Numerous improvements, thanks due to Stefan Monnier.
*** Some GNU Emacs backwards compatibility removed: use 21.1 or later
** Changes for Isabelle
Beginnings of support PGIP protocol (work in progress with Isabelle
2004). Presently allows Isabelle to configure Proof General prover
settings menu.
Backward compatibility may not be maintained: it's simply too much
effort. This means that if you upgrade your Emacs version, which
forces you to upgrade Proof General because Emacs upgrades usually
break Proof General (Emacs authors pay little heed to maintaining
APIs), then you may have to upgrade your Isabelle version as well.
** Changes for Coq
*** Indentation
*** Menu entries for commands, tactics and terms
*** "Holes" system, for editing structured expressions
Holes are a powerful feature for complex expression editing. It is
inspired from other tools, like Pcoq
(http://www-sop.inria.fr/lemme/pcoq/index.html). The principle is
simple, holes are pieces of text that can be "filled" by different
means. The new menu system makes use of the hole system. Almost all
holes operation are available in the Coq/holes menu.
*** X-symbols are much improved (more symbols, cleaner grammar)
Symbols are encoded only if between spaces or _'s. Sub/superscripts
are now introduced by '__' and '^^' respectively, and the rest of the
word is sub/superscripted. To put spaces inside sub/superscripts, use
_{...} or ^{...}. Notice that this syntax is not understood by Coq
and you will need to defined it with the "Notation" command of Coq.
** Additional instances of Proof General
*** ccc: Proof General for the Casl Consistency Checker
Provided by Christoph Lüth <cxl@informatik.uni-bremen.de>.
See http://www.informatik.uni-bremen.de/cofi/ccc for more information.
*** pgshell: Proof General for shell scripts/simple command interpreters.
This instance of PG is handy just for using script management to
cut-and-paste into a buffer running an ordinary shell or tool
with a command-line interpreter of some kind.
Provides an instant and cheap interface to command-line interpreters,
to avoid tiresomely using cut-and-paste to run pre-recorded commands.
|