TWiki> PG Web>ProofGeneralKit>ProofGeneralEclipse>PGEmacsEclipseComparison (21 Aug 2006, DavidAspinall)EditAttach

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

Edit | Attach | Print version | History: r1 | Backlinks | Raw View | Raw edit | More topic actions
Topic revision: r1 - 21 Aug 2006 - 12:06:56 - DavidAspinall
 
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies