TODO


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.  Also, for
low-level (possibly obsolete) detail, see the file TODO.developer.

Please send any suggestions, comments, or offers of help to
da+pg-feedback@inf.ed.ac.uk.  Thanks!


Plans 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.