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
|
-*- outline -*-
* Known issues which will be resolved before 3.4
The items below are known and will be fixed (I hope!) before 3.4
is released. Please don't send email about them (unless you have
a patch...)
** X-Symbol probs with Isabelle
-- \<tokens> don't immediately get decoded
-- latin1 chars get saved in file
-- superscripts/subscripts broken
-----------------------------------------------------------------
* Known Bugs and Workarounds for Proof General.
Contact: mailto:bugs@proofgeneral.org
See also: http://www.proofgeneral.org/ProofGeneral/BUGS
Generic bugs are listed here, which may affect all of the supported
provers. See lego/BUGS coq/BUGS, etc, for specific bug lists for each
of the provers supported.
The bugs here are split into problems which apply for all Emacs
versions, and those which only apply to particular versions.
* Generic problems, for all Emacs versions
** Visibility control doesn't distinguish theorems with same name.
If you have more than one theorem with the same name in a buffer,
their proof visibilities are controlled together.
** If the proof assistant goes into a loop displaying lots of information
It may be difficult or impossible to interrupt it, because Emacs
doesn't get a chance to process the C-c C-c keypress or "Stop" button
push (or anything else). In this situation, you will need to send an
interrupt to the (e.g.) Isabelle process from another shell. If that
doesn't stop things, you can try 'kill -FPE <emacs-pid>'.
This problem can happen with looping rewrite rules in the Isabelle
simplifier, when tracing rewriting. It seems to be worse on
certain architectures, and slower machines.
** Toolbar enablers unreliable on some platforms.
Occasionally the buttons are disabled/enabled when they shouldn't be.
An extra click on the toolbar may solve this. If you have problems,
please customize `proof-toolbar-use-button-enablers' to nil to
disable the enablers.
** Using C-g can leave script management in a mess.
The code is not fully 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 processed proof script files
Because of read-only restrictions of the protected region.
This is an inherent problem with outline because it works by
modifying the buffer.
Workaround: none, nevermind. (If it's hugely needed we could support
modified outline commands).
** When proof-rsh-command is set to "ssh host", C-c C-c broken
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.
** In tty mode, the binding C-c C-RET has no effect.
Workaround: manually bind C-c RET to 'proof-goto-point instead.
** Multiple file scripting 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!
* Problems with particular Emacs versions
** Looping in Emacs 21.2
Several (odd) circumstances cause this version of Emacs to loop.
For example, (setq-default column-number-mode t) before starting
Emacs, or moving the cursor around in the *coq* buffer.
It seems likely that these are Emacs bugs, workaround unknown.
Please contact us if you can help.
** Buggy output fontification with Emacs 21.2 / X-Symbol
Output colouration may spill into adjacent symbols when
X-Symbol support is switched on.
** Emacs menus: options not updated dynamically, positions erratic, etc.
Also, proof assistant specific menus only appear in scripting buffer.
These are drawbacks with GNU Emacs menu support.
** Emacs faces sometimes faulty, esp in console mode
Emacs support is let down in console mode, because faces are not
implemented there. (XEmacs can use colours and underline in console
mode)
** XEmacs 21.1.9 on Win32
Some strange problems reading files with this version of Emacs. Gives
spurious "end of internal input stream", or silently ignores parts of
files. Example is coq/coq.el which reads in fine on Linux.
Solution: use a more recent version of XEmacs.
** If you have problems using Mule versions of GNU Emacs
Beware setting standard-display-european: Pascal Brisset suggests
adding this line to .emacs should help:
(setq process-coding-system-alist '(("" . no-conversion)))
** Strict read only disabled by default in GNU Emacs.
Unfortunately strict read only is incompatible with font lock in
GNU Emacs, so it is disabled by default. Instead, you get a warning message
if the locked region is edited.
** In GNU Emacs, spurious "Region read only" errors
Same problem as above, different symptom.
When proof-strict-read-only is set and font lock is on, these
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.
** XEmacs undo in the script buffer can edit the "uneditable region"
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.
** As of GNU Emacs 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. The code that is
turned off deals with term markup for proof by pointing, which only
affects LEGO at the moment. This problem could affect forthcoming
versions of XEmacs (but hasn't as far as XEmacs 21.4). [Can anybody
tell us if it affects Mule versions of Emacs?]
Workaround: for LEGO pbp, use GNU Emacs 20.2, or XEmacs 20.4/later.
** 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.
|
