Re: [isabelle] Isabelle 2014 and proof general
On Fri, 12 Sep 2014, Vadim Zaliva wrote:
Let me put forward some arguments in defence of Proof General support in
In principle this discussion is 5-3 years late. Already 5 years ago,
Isabelle/PIDE development has started to become serious, and 3 years ago
there was the turning point for practical use of Isabelle/jEdit as the
main application of the PIDE framework.
Hardcore users of Proof General Emacs have chosen to ignore this over a
long time. In Isabelle2014 the tiny change to make Proof General
"optional" -- with proper documentation in NEWS and hardly any effort to
reactivate it based on information from the "system" manual -- seems to
have the effect that people actually do wake up.
For the purpose of this discussion the functionality of PIDE such as
Proof General as well as Isabelle/Jedit could be broadly split into 3
1. Basic functionality - basic editing functionality used in Isabelle
mode as well as for other modes. Here you have managing multiple
buffers, windows, search, clipboard, completion, etc.
2. Isabelle specific interface.
3. Other functionality of the PIDE which is not strictly speaking is
necessary for working with Isabelle. For example integration with
other languages (ML, LISP, Haskell), spell checker integration, etc.
I have limited experience with #2 but for my purposes both Proof General
and Isabelle/JEdit were comparable.
This means you did not spend long enough with Isabelle/jEdit, to find out
what it really does (and what not yet). The "jedit" manual in
Isabelle2014 is once again updated and extended, and now rather long with
almost 50 pages. There is a lot to discover, but long-term Proof General
users need to unlearn quite a lot.
Some people might find Jedit/Isabelle asynchronous proving superior to
Proof General's sequential mode but I like the control Proof General
The document-oriented approach with implicit checking is inherent in PIDE.
If you don't believe in it, you are welcome to start a project to
implement a PG-emulation using the official Isabelle protocol function
interface (not the old TTY loop, which is already legacy). This is
possible in user-space, using the current Isabelle/Scala infrastructure to
connect Isabelle to the outside world.
Most importantly in #1 I found jEdit (mind you, not Isabelle/jEdit but
jEdit itself) lacking, compared to Emacs. A couple of trivial examples:
I-search and working with rectangular blocks in copy/paste.
Both search and blocks work much better in jEdit than in Emacs. After 15
years of Emacs, I left it behind in 2006, and today I can't live without
jEdit quick-search / hyper-search and various advanced selection modes.
The two weeks I had invested in 2006 to unlearn Emacs key bindings and
learn a few jEdit tricks have paid off.
The general qualities of jEdit also convinced me in 2006/2007 to make it
the basis for the main example application of PIDE.
This does not mean all PIDE applications need to work with jEdit.
Isabelle/Eclipse and Clide have already been mentioned, and will hopefully
be updated soon to Isabelle2014.
Finally, although it is not directly related to Isabelle, I think in #3
emacs have much more to offer due to the amount of code written for
Emacs over the decades.
This can be accounted both on the positive and negative side. Tons of
existing material in Emacs makes it slow to move anywhere. Most of the
material is actually obsolete.
In contrast, jEdit has many useful plugins, while many things are missing,
but it is easy to improve on that. I have done quite something for
Isabelle/jEdit -- the "Isabelle" plugin has become a large assembly of
modules to augment jEdit in many ways, both specifically and
non-specifically to Isabelle.
jEdit is somewhere in the middle in project size and complexity, e.g.
compared to Emacs or Eclipse, and it is relatively easy to move it
onwards, with a little bit of enthusiam and energy.
For example I am working with Haskell, LISP code and Isabelle proofs at
the same time and now I am forced to run jEdit and Emacs concurrently.
Emacs key binding in jEdit are not exactly the same as real Emacs on Mac
so I am constantly struggling when switching between the two. With Proof
General I was easily editing all Isabelle, LISP and Haskell from the
comfort of the same familiar environment.
With "familiar environment" we are back to "I don't want to change
I don't see why an Isabelle front-end should specifically support Emacs,
apart from accidental side-conditions from the past. Why not vi instead?
The old debate of Emacs vs. vi has long been settled in favour of vi
This archive was generated by a fusion of
Pipermail (Mailman edition) and