blob: 964057894e22c4e12e691c7b893eb763e5898d16 (
plain)
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
|
This is our brief list of planned things to do to Proof General.
$Id$
See also the Proof General development page on the web, and
the issue tracker at http://proofgeneral.inf.ed.ac.uk/trac.
Please send any suggestions, comments, or offers of help to
da+pg-feedback@inf.ed.ac.uk.
Ideas for upcoming versions
---------------------------
* Implement support for PG Kit. Support PGIP provers fully, with/without
broker. (See http://proofgeneral.inf.ed.ac.uk/kit).
* Use CEDET Emacs framework for development tools, to allow more
powerful parsing of proof scripts and features arising from that.
(See http://cedet.sourceforge.net/).
* Add a browser mode for browsing script files and/or live theory
data-structures, in the prover.
* More flexible goals buffer mode to allow menus of common proof
commands, especially via PBP-style highlighting
* Queue manipulation improvement: allow to extend or reduce
during processing, with fewer "Proof Process Busy" messages.
* Support more proof assistants. Add more example proofs.
|
