[isabelle-dev] Future of ProofGeneral

Lawrence Paulson lp15 at cam.ac.uk
Tue Apr 17 20:38:28 CEST 2012


Sorry, I didn't intend to be tactless or demanding, but at least something analogous to the “Isabelle" menu (offering access to show me/commands/prover settings) is needed. Unless it's there somewhere and I overlooked it.
Larry

On 17 Apr 2012, at 17:18, Makarius wrote:

> 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.
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




More information about the isabelle-dev mailing list