Proof General in Emacs and Eclipse
- Currently less functionality thatn ProofGeneralEmacs
- But... prettier windows, advanced IDE environment...
- Will become the future main platform for Proof General, with NewProofGeneralEmacs taking a back seat.
An incomplete comparison:
|
Feature |
ProofGeneralEmacs |
ProofGeneralEclipse |
|
Setup utility for new systems |
Yes |
No |
|
Supports Isabelle |
Yes |
Yes |
|
Supports Coq |
Yes |
No |
|
Supports Lego |
Yes |
No |
|
CVS support |
sort of |
Yes |
|
Support for running over a network |
sort of |
Yes |
|
Hints feature |
No |
Yes |
|
User Interface features |
|
Syntax highlighting |
Yes |
Yes |
|
Key bindings |
Yes |
Yes |
|
X-Symbols |
Yes |
Yes |
|
Symbol editor |
No |
Yes |
|
Integrated help |
No |
Yes |
|
Theory browsing tools |
No |
Yes |
|
Scripting |
No |
Yes |
Here,
sort of means that you may need to do some low-level Emacs configuration rather than having a nice
menu option readily available. Hard-core Emacs users are usually not worried, others may be.
Priorities
Please tell us what our priorities should be by adding comments below.
--
DavidAspinall - 21 Aug 2006