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
|
-*- outline -*-
* Known Bugs and Workarounds for Proof General.
Contact: mailto:proofgen@dcs.ed.ac.uk
See also: http://www.dcs.ed.ac.uk/home/proofgen/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.
* Proof General 3.0 BUGS addendum (fixed in current pre-rel)
** FSF Emacs: problem with version 20.5
PG freezes when starting a proof assistant.
Fixed in the current pre-release.
** Problems with Japanese versions of FSF Emacs (at least)
These have older versions of CL macros (defined in file "egg")
with Japanese documentation.
Hopefully fixed in current pre-release, please send in details of
any problems!
** You may occasionally see duplications of short (<10 chars)
messages from the proof assistant. This is caused by a too high
setting of the configuration variable
proof-shell-eager-annotation-start-length.
Fixed in current pre-release.
* Generic problems
** 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)))
** 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. 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.
** 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.
** Ordinary undo in the 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, spurious "Region read only" errors
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.
** 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.
** 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 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.
** 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.
|
