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
|
This is our brief list of planned things to do to Proof General.
$Id$
See also the Proof General projects page on the web, under the
development section of the home page. Also, see the appendix "Plans
and Ideas" in the manual, and for low-level detail, the file "todo" in
the developer release.
Please send any suggestions, comments, or offers of help to
proofgen@dcs.ed.ac.uk. Thanks!
Plans for upcoming 3.x versions
-------------------------------
* Support turning on/off prover output automatically, e.g.
Coq's "Begin Silent" and "End Silent" commands.
[Now implemented in 3.2pre]
* Fix Isabelle's "Stack overflow in regexp". See isa/BUGS.
[Now implemented in 3.2pre]
* New key bindings for prover specific commands.
This will unfortunately result in changing some bindings, but make
room for more and avoid the user-reserved sequences C-c <letter>.
[Now implemented in 3.2pre]
* Add a favourites mechanism for proof commands issued using
point-and-click in goals buffer. Useful when pbp isn't supported.
[Now partially implemented in 3.2pre]
* Support more proof assistants
* A more flexible way of choosing which instance of PG we want,
allowing matches on the buffer before choosing the mode function.
* Isabelle PG: Non-blocking for .thy loading from .ML files.
Plans for later versions
------------------------
* Make an XEmacs package
* Queue manipulation improvment: allow to extend or reduce
during processing, with fewer "Proof Process Busy" messages.
* Improve process handling: disable interrupts and/or catch errors at
crucial points in code so that C-g can safely be used during script
processing. Handle deleted buffers smoothly.
* Implement "Atomic Command Sequence" idea, or something like
it. To allow more flexible understanding of undo behaviour
of proof assistants. Alternative is to base markup of
undoable regions on proof assistant output or messages.
* Add completion of theorem names, choice of proof commands, etc.
* Add a browser mode for browsing script files
and/or theory data-structures in the prover.
* More flexible goals buffer mode to allow menus of
common proof commands.
* Implement ideas in the Proof General White Paper.
(See the Development section of the web page for a link).
|
