[isabelle-dev] Remaining uses of Proof General?

[Makarius]

On Fri, 27 Jun 2014, Peter Lammich wrote:

> My overall impression is that Isabelle/jEdit is usable but much less
> mature than PG:
> It does not scale well to large projects, and tends to be unstable.
> It has many cool advanced features, but lacks important basic ones.

Better reverse all that, just to simplify your life.  There might be 
technological fine points, but the big problems are phsychological ones. 
You need to leave PG behind and adopt a quite different system.


> However, in my opinion, Isabelle/jEdit is approaching a level of 
> maturity required for production use, once the user knows about its 
> deficits and how to avoid them.

That is also a tautology: PG has tons of deficits, but working around them 
has become second nature to long-term users. In Isabelle/jEdit you need to 
get used to different behaviour, and make yourself productive with it.

*Any* system is just crap, but in different ways.


 	Makarius