[isabelle-dev] Remaining uses of Proof General?
matthew.fernandez at nicta.com.au
Mon Apr 28 01:41:40 CEST 2014
On 28/04/14 04:14, Makarius wrote:
> Are there any remaining uses of Proof General, e.g. in the situation of current
> Isabelle/5b6f4655e2f2 ?
I'm mostly on Isabelle/jEdit now, but I do delve back into Isabelle/Emacs (is that the current
terminology for this creature?) every now and then. My reasons are mostly predictable execution, as
I can control what the prover is up to with explicit stepping forwards and backwards. I can probably
achieve the same result toggling continuous checking on/off in Isabelle/jEdit, but haven't invested
the time in modifying my workflow. I've also encountered the problems discussed in other threads of
the Isabelle/jEdit GUI locking up when some tactic is looping and the JVM heap being exhausted with
no indication from the UI. However, if PG support disappeared entirely I wouldn't shed a tear.
Something which used to be a driving factor for me, but no longer is: Isabelle/Emacs is capable of
running on underpowered machines which do not have enough resources to run Isabelle/jEdit. This is
not a good reason for maintaining legacy support, but there may be users in this situation.
On 28/04/14 06:10, Makarius wrote:
> On Sun, 27 Apr 2014, Manuel Eberl wrote:
>> I am not, as it were, a user of Proof General anymore; however, I would
>> like, if I may, to point out one thing that annoys me in jEdit and that
>> was, in my opinion, better in Proof General: the handling of
>> abbreviations for Unicode characters.
> Please not again this talk about "jEdit". What you mean is Isabelle/jEdit, which is the default
> Prover IDE of Isabelle these days.
> The difference really matters, because jEdit (the text editor) has many different ways for
> abbreviations, completion etc. (You could also add various input methods of the Java platform, or
> the operating system.)
> In Isabelle/jEdit (the Prover IDE), I had varying default mechanisms for that over the years. The
> present one (in Isabelle/5b6f4655e2f2) is quite advanced, but also quite complex, not to say
> complicated. In the coming weeks and months it needs to be polished for the release, but there will
> be no further changes of the basic approach, as far as I can forsee.
> It is in principle also possible to provide completely different completion plugins, e.g. if someone
> wants to imitate the old X-Symbol behaviour precisely. jEdit is a very flexible text editor, and
> Isabelle/jEdit a powerful Prover IDE, which happens to provide certain defaults out of the box.
>> The current behaviour with “immediate completion” in jEdit is already a
>> great improvement over having to press “return” or “tab” every time one
>> wants to use an abbreviation, but one problem that remains is the fact
>> that jEdit performs the insertion of the character as soon as there is
>> only one character of that name left, which often leads to somewhat
>> unpredictable results – for instance, typing “\sigma” results in “σma”.
> That in isolation is predictable: the completion happens when the result is unique, and that notion
> of uniqueness does not change dynamically. That is the behaviour of Isabelle2013-2, though, since
> the new semantic completion introduces a "language context" that sometimes introduces
> non-determinism of a different kind, but not the above.
>> I would prefer a solution that is more suited to my style of typing
>> “\sigma” and immediately getting “σ”, like in Proof General.
> Here you merely need to train your fingers for the exact amount of prefix required for some symbol.
> If that does not work, you can leave the immediate completion off (which is the default). "Like in
> Proof General" means just the 4.x line, because that mechanism was quite different until 3.x, when I
> was still using Proof General myself.
>> Another problem is that some abbreviations, like “==”, are not automatically replaced since there
>> are several possibilities.
> That is on purpose, to avoid other odd effects. Very ambitious users can specify their own
> abbreviations in $ISABELLE_HOME_USER/etc/symbols, and see themselves how to balance the various
> possibilities of:
> (1) single-character abbreviations, e.g. "%"
> (2) unique abbreviations, e.g. "-->"
> (3) ambiguous abbrevations, e.g. "=="
> Note that "==" is rare in practice anyway, mostly for 'abbreviation' within the logical environment,
> which does not happen so often. Unless you are using old-style definitions with that Pure
> connective instead of the normal HOL one.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
More information about the isabelle-dev