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
|
Known Bugs and Workarounds for Proof General.
=============================================
$Id$
Contact: proofgen@dcs.ed.ac.uk
See also: http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral/BUGS
-----------------
Generic problems
================
* Highlighting of locked (blue) and queue (red) regions in FSF Emacs
may be unreliable (disappear) in some cases. Cause unknown. If you
observe this, please submit a bug report with details of your system
and any other information you think may be relevant. Workaround:
switch to using XEmacs.
* Toolbar enablers for XEmacs 21: since these have been switched on,
it is apparent that the recognition of completed proofs is unreliable.
Please report cases where the buttons are enabled/disabled at the
wrong time.
* Ordinary undo in script buffer can edit the "uneditable region"
in XEmacs. This doesn't happen in FSFmacs. Test case:
Insert some nonsense text after the locked region.
Kill the line. Process to the next command.
Press C-x u, nonsense text appears in locked region.
Workaround: take care with undo in XEmacs.
* In FSFmacs, when proof-strict-read-only is set and font lock
is switched on, spurious "Region read only" errors are given
which break font lock.
Workaround: turn off proof-strict-read-only, font-lock, or for
the best of all possible worlds, switch to XEmacs.
* As of FSFmacs 20.3, multi-byte character codes are used. This
breaks some of the code in Proof General, which is turned off in
case the suspicious looking function
toggle-enable-multibyte-characters is present. This could effect
forthcoming versions of XEmacs.
Workaround: use FSFmacs 20.2, or XEmacs 20.4/later.
* Using C-g can leave script management in a mess. The code
needs to have some regions protected from Emacs interrupts.
Workaround: Don't type C-g while script management is processing. If
you do, use proof-restart-scripting.
* Outline-mode does not work in proof script files due to read-only
restrictions of protected region. Workaround: none, nevermind.
(If it's hugely needed we could support modified outline commands).
* `proof-find-next-terminator' (bound to C-c C-e) doesn't work
properly. Neither does 'proof-goto-command-start' (C-c C-a).
Workaround: use other means to navigate in a proof scipt buffer.
* Multiple file handling for Lego and Isabelle is slightly vulnerable.
Files are not locked when they are being read by the prover, so a long
file could be edited and saved as the prover is processing it,
resulting in a loss of synchronization between Emacs and the proof
assistant. Files ought to be coloured red while they are being
processed, just as single lines are. Workaround: be careful not
to edit a file as it is being read by the proof assistant!
* XEmacs sometimes has strange start-up delays of several seconds,
possibly due to face allocation, when running remotely and
displaying on an 8-bit display. One workaround (and in fact the
recommended way of working) is to run XEmacs locally and only
the proof assistant on your fast compute server, by setting
proof-rsh-command.
* There is an problem with process communication on Solaris, where
there is an input line length limitation for terminals in cooked mode,
perhaps to 256 characters. Further input elicits a bell character
(^G). This ruins Proof General's parsing of the shell buffer.
Future fix: try setting process-connection-type to nil, which
instructs XEmacs to use pipes instead of pseudo-terminals for
subprocess I/O. (You lose job control of processes you start in shell
mode, and some commands (notably ls) behave differently when writing
output to a pipe instead of a tty. But using a pipe will allow you to
paste arbitrarily long blocks of text into shell mode.)
Current workaround: use another OS, e.g. Linux.
[1999/08/20: believed to be fixed]
* XEmacs sessions maybe grow excessively in terms of memory
allocation. Maybe some of the spans aren't removed properly.
Setting a limit on the size of the process buffer doesn't seem to
help.
[1998/10/06: believed to be fixed]
* When proof-rsh-command is set to "ssh host" and you issue Ctrl-c to
interrupt, the whole process may be killed instead of interrupted.
This isn't a bug in Proof General, but the behaviour of ssh. Try
using rsh instead, it is said to forward signals to the remote command.
FSF Emacs specific bugs
=======================
*`proof-zap-commas-region' does not work for Emacs 20.2 on
lego/example.l . On *initially* fontifying the buffer,
commas are not zapped. However, when entering text, commata are
zapped correctly. Workaround: don't stare too much at commata
LEGO Proof General Bugs
=======================
* If LEGO attempts to write a (object) file in a non-writable
directory, it forgets the protocol mechanism on how to interact with
Proof General and gets stuck. Workaround: Directly enter "Configure
AnnotateOn" in the Proof Shell to recover.
* After a `Discharge', retraction ought to only be possible back to the
first declaration/definition which is discharged. However, LEGO Proof
General does not know that Discharge has such a non-local effect.
Workaround: retract back to the first declaration/definition which is
discharged.
* A thorny issue is local definitions in a proof state. LEGO cannot
undo them explicitly. Workaround: retract back to a command before a
definition.
* Normalisation commands such as `Dnf', `Hnf' `Normal' cannot be undone
in a proof state by the Proof General. Workaround: retract back to the
start of the proof.
* After LEGO has issued a `*** QED ***' you may undo steps in the proof
as long as you don't issue a `Save' command or start a new proof. The
LEGO Proof General assumes that all proofs are terminated with a
proper `Save' command. Workaround: Always issue a `Save' command after
completing a proof. If you forget one, you should retract to a point
before the offending proof development.
*legotags doesn't find all declarations. It cannot handle lists e.g.,
with [x,y:nat]; it only tags x but not y. [The same problem exists for
coqtags] Workaround: don't rely too much on the etags mechanism.
Coq Proof General Bugs
======================
* coqtags doesn't find all declarations. It cannot handle lists e.g.,
with "Parameter x,y:nat" it only tags x but not y. [The same problem
exists for legotags] Workaround: don't rely too much on the etags
mechanism.
* User defined tactics cannot be retracted. Workaround: you may need
to retract to the beginning of the proof.
Isabelle Proof General Bugs
===========================
* General difficulty with complex proof scripts. Since Isabelle uses
ML as a top-level language for writing proof-scripts, Proof General
may have difficulty understanding scripts which stray too far away
from the standard functions, tactics, and tacticals. You will
usually notice when a function, or whatever, doesn't get highlighted
as you might expect. This probably has no detrimental impact on the
interface unless you use your own "goal" or "qed" forms.
* Blocking when processing multiple files, beginning from a .ML file.
Proof General will block the Emacs process when it is waiting for
a theory file (and it's ancestors) to be read. To avoid this,
assert the theory file rather than the ML file.
|
