*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Isabelle 2014 and proof general*From*: Vadim Zaliva <vzaliva at cmu.edu>*Date*: Fri, 12 Sep 2014 16:57:38 +0300*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <alpine.LNX.2.00.1409102031580.41896@lxbroy10.informatik.tu-muenchen.de>*References*: <A216A54B-BD72-4913-ADE9-B545E83D0813@cmu.edu> <alpine.LNX.2.00.1409102031580.41896@lxbroy10.informatik.tu-muenchen.de>*Sender*: Vadim Zaliva <vadim.zaliva at west.cmu.edu>

> 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

**Follow-Ups**:**Re: [isabelle] Isabelle 2014 and proof general***From:*Makarius

**Re: [isabelle] Isabelle 2014 and proof general***From:*Lars Noschinski

**References**:**[isabelle] Isabelle 2014 and proof general***From:*Vadim Zaliva

**Re: [isabelle] Isabelle 2014 and proof general***From:*Makarius

- Previous by Date: [isabelle] CfP: International Workshop on MILS: Architecture and Assurance for Secure Systems, Amsterdam 20.01.2015, co-located with HIPEAC
- Next by Date: Re: [isabelle] How to use latex commands inside proof?
- Previous by Thread: Re: [isabelle] Isabelle 2014 and proof general
- Next by Thread: Re: [isabelle] Isabelle 2014 and proof general
- Cl-isabelle-users September 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list