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
|
-*- mode:outline -*-
* Things to do for LEGO
See also ../todo for generic things to do, priority codes.
** C Improve X-Symbol support.
** D Fix Pbp implementation in LEGO itself (10h)
** D In LEGO, apart from Goal...Save pairs, we have
declaration...discharge pairs. See the section "Granularity of
Atomic Commands" for a proposal on how to generalise the current
implementation so that it can also deal with "Discharge".
[See also the Coq problem with Sections] (6h)
** D Inoking an "Expand" command produces a new proof state. But this is
incorrectly displayed in the response buffer and not the goals
buffer because special annotations are missing. Presumably, one
ought to replace "Toplevel.Pr()" by "Toplevel.PR()" in the
definition of "Expand" (see file newtop.sml [Version 1.4]). (30min)
** D Even with the more flexible region model, with
proof-nested-goals-behaviour=closequick, Proof General doesn't
do quite the right thing. Forget for a definition when inside
a proofstate kills off the whole proofstate. Effectively,
the definition is *global* rather than local to the proofstate,
and could perhaps be lifted to before the goal
(with the lift-global nonsense not so daft after all? Editing
behind the user's back is still objectionable though).
Another alternative fix would be to trigger some retraction action
on seeing the "Abort" regexp, rather than assuming it is the result of
some retraction action. More generally this could be used for error
handling.
** D Improve legotags. It cannot handle lists e.g., with
[x,y:nat];
it only tags x but not y. [The same problem exists for coqtags]
** X Mechanism to save object file. Specifically, after having processed
a script (interactively), it would be nice if one could now save the
buffer in object format. At the moment, it only gets converted
(automatically) when it is read in indirectly at a later stage.
However, there is currently no LEGO command to do this. [4h]
|
