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
|
-*- outline -*-
* Known Bugs and Workarounds for Proof General.
Contact: mailto:proofgen@dcs.ed.ac.uk
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
** 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.
** Do not use C-x C-v or C-x C-w on a script file in active scripting mode
Proof General will lose track of the file.
Workaround: always turn off active scripting first with C-c C-s.
Also there is a possibility (untested) of losing synchronization with
multiple files if you use these functions. To be safe, kill
the buffer first and use C-x C-f instead of C-x C-v, or kill
and then re-find after C-x C-w.
[ FIXED, testing with 3.2 pre-releases. ]
** Toolbar enablers for XEmacs 21, some artefacts.
There is a timing issue, so that occasionally the buttons are
disabled/enabled when they shouldn't be. An extra click on the
toolbar solves this.
** 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).
** 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!
(Only applies to Lego and Isabelle)
** 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.
* Problems with particular Emacs versions
** Emacs menus: options not updated dynamically, positions erratic, etc.
Also, proof assistant specific menus only appear in scripting buffer.
These are drawbacks with FSF Emacs menu support.
** 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.
[ Is my suspicioun of XEmacs correct? Any suggestions? ]
** If you have problems using Mule versions of FSF 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 FSF Emacs.
Unfortunately strict read only is incompatible with font lock in
FSF Emacs, so it is disabled by default. Instead, you get a warning message
if the locked region is edited.
** In FSFmacs, 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 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. 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.1). Can anybody
tell me if it affects Mule versions of Emacs? Workaround: for LEGO
pbp, use FSFmacs 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.
|
