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
|
Known Bugs and Workarounds.
===========================
$Id$
* Toolbar: retract button can give "BUG" error message "called from
wrong buffer" when the process is inactive.
* 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.
* 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.
* You can't use more than one proof assistant at a time in the same
Emacs session. Attempting to load Proof General for a second prover
will fail. Workaround: stick to one prover per Emacs session,
make sure that the proof-assistants variables only enables
Proof General for the provers you need.
* 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).
* There is an obscure bug with processes on Solaris which results in
buffers full of ^G after certain combinations of input. Workaround:
get a patch from Sun, or use Linux.
* XEmacs sessions perhaps 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: Is this bug still present? Test examples?)
*`proof-find-next-terminator' (bound to C-c C-e) doesn't work
properly. Workaround: use other means to navigate in a proof scipt
buffer.
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
=======================
* 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 issues are 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.
|
