[isabelle-dev] Future of ProofGeneral

Makarius makarius at sketis.net
Tue Apr 17 18:18:25 CEST 2012

On Tue, 17 Apr 2012, Lawrence Paulson wrote:

> I certainly care about it. Jedit is great for browsing existing theory 
> developments, but there is no support for actually doing proofs.

As I've said already 4 years ago, the double burden to keep ProofGeneral 
alive and make Isabelle/jEdit a full replacement (and more) slows things 
down considerably.

After long struggles, the Isabelle2011-1 version of Isabelle/jEdit is 
defined as first stable release, with many things still missing, but it 
can be used for many more things than just browsing.

The situation is improving further for the coming release, but I am still 
encumbered by ProofGeneral Emacs, since nobody has ever stepped forward to 
take over the responsibility for it.


More information about the isabelle-dev mailing list