[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Sun May 25 14:59:30 CEST 2014
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.
More information about the isabelle-dev