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 Isabelle.

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 categories:

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 gives me.

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 habits".

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 anyway.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.