[isabelle-dev] Remaining uses of Proof General?

[Matthew Fernandez]

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.
>
>
>      Makarius
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

________________________________

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.