[isabelle-dev] Remaining uses of Proof General?

[Makarius]

On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:

> In the course of a day, I typically find myself pulling from the 
> Isabelle repository several times. I am encouraged in this by my use of 
> Mercurial queues. So it's not untypical that my HOL image is slightly 
> out of date, usually in a harmless way. Sometimes I fire up Proof 
> General just because I know it will take the image as is instead of 
> forcing me to rebuild it (and waste 4 minutes of my time).

There is already "isabelle jedit -n" to bypass the automatic build. I 
never use that myself, because I no longer do the bootstrap dependency 
management in my head.

When I do have to step out of the self-build chain of the tool 
infrastructure, e.g. when working on the sources of Isabelle/Pure or 
Isabelle/jEdit sources, I use a separate jEdit editor process that is not 
Isabelle/jEdit. Another option is to use the last official release of 
Isabelle/jEdit to edit a few files elsewhere.


> Sometimes I would just wish Isabelle/jEdit could allow me to do the 
> quick-and-dirty things the more primitive Proof General allowed -- a "I 
> know what I'm doing" flag so to speak.

I guess it is more "I knew how it used to be done in the old times with 
Proof General end Emacs". Isabelle/jEdit does allow much more things than 
was possible before, it only needs to be discovered.

Sometimes my impression is that it would be better to discard Proof 
General on the spot, so that people have free mental energies to work in a 
more productive way with slightly more up-to-date tools.


 	Makarius