Re: [isabelle] Isabelle 2014 and proof general



> Apart from proper names an concepts, we are back to the canonical
> question: Are there any remaining uses of Proof General?
> 
> Just being stuck out of habit over decades is no good reason. The word
> "reason" is related "ratio" or "rational", but sticking blindly to
> habits is rather irrational. This natural inertia has sucked up a lot of
> resources over the years. It is better to spend resources now to figure
> out how close we are to the final disposal of Isabelle Proof General --
> after more than 5 years of Isabelle/PIDE development.
> 
> That is a serious topic, but some hard facts need to be put on the
> table, not just "I don't want to change habits".

Let me put forward some arguments in defence of Proof General support in Isabelle.

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.
(Some people might find Jedit/Isabelle asynchronous proving superior to Proof General's sequential mode but I
like the control Proof General gives me. One of the reasons is that some of my lemmas take a long time to prove and I do not want to to try prove them until I am ready to do so. For example when I am reorganizing my proofs and moving code around
I would not want it to rush and try prove things until I am finished.)

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.

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.

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.


Sincerely,
Vadim Zaliva

--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva





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