[isabelle-dev] Remaining uses of Proof General?

[Makarius]

On Mon, 28 Apr 2014, Matthew Fernandez wrote:

> 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?)

I don't know all details about the terminology, which is also slightly 
varying over time.  There are Isabelle tools called "emacs" and "jedit" 
after the underlying text editors, which I introduced myself some years 
ago, alongside with "isabelle tty" (which actually uses "rlwrap" as editor 
if that is available).

"isabelle emacs" invokes "Proof General" or "Isabelle Proof General" (in 
contrast to the Coq version), or "Proof General Emacs" (in contrast to the 
Eclipse version) -- David Aspinall could explain that more precisely.  I 
used myself wrongly "ProofGeneral" over many years, and David never told 
me that until it was rather late, but I changed that habit afterwards.

"isabelle jedit" starts Isabelle/jEdit.  This was once a tiny Isabelle 
plugin for the jEdit text editor (so the distinction did not exist yet), 
but is now a rather big IDE based on jEdit and a lot of extra 
functionality provided by the plugin + a few JVM bootstrap tricks. 
Regular users of official releases also get a native application wrapper 
that was newly introduced in Isabelle2013-2, and is different from the 
jEdit distribution.


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

Can you say more about typical situations?  When doing occasional 
debugging, either of tools or the system itself, I need more knowledge 
about what happens when exactly.  I never do this in Proof General these 
days, but within the Prover IDE in a buffer that contains only the main 
items of interest.  Then I edit carefully, based on educated guesses how 
the PIDE document model works, or I toggle the continuous checking that 
was newly introduced in Isabelle2013-2.


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

I reckon that this refers to the official Isabelle2013-2 release.  I have 
reworked many details of scheduling in the past few months, even just now 
when writing this email.  When the Isabelle2014-RC line starts (probably 
in July) you should look precisely at your typical applications to see how 
it works.  I don't want to see again a situation where problem reports 
trickle only slowly *after* the release is shipped.


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

It is a normal sign of stagnation of some application that it suddenly 
runs blazingly fast on old or tiny hardware.  At ITP 2013 last summer I've 
seen a few Coq users working comfortably with CoqIDE or Proof General on 
netbooks are small laptops.  That surely can't be done with a full-scale 
Prover IDE like Isabelle/jEdit. When Proof General was young and strong, 
it was also huge and bloated compared to the hardware of that time, 
escpecially XEmacs was really heavy and we had many insider jokes about 
that.

The relation of hardware vs. software performance is not an accident, but 
the result of the normal balancing of trade-offs: How much functionality 
can we afford on a certain range of hardware at the moment?  I routinely 
walk through consumer electronics stores like Fnac Paris, to see what you 
get for 500..1000 EUR, to estimate what can be expected from typical 
users.  Then I test on 3 systematically on 3 dissimilar systems, 2 of them
actually > 3 years old.


What I normally don't test is unplugged battery mode, because I am in the 
lucky situation of not commuting.  People who do that routinely, should 
make some systematic experiments with the nominal number of Isabelle/ML 
threads at 0.5 of the true number of cores, i.e. 0.25 of the virtual 
number of cores on Intel.  To simplify the calculation, just try the 
constant threads = 1 an see how it works.

Last summer at Rennes, someone was surprised to have a "2 core laptop 
running at 600% CPU", but it actually turned out a new i7 with 8 virtual 
CPUs.  The defaults were just burning down the batteries, without any 
extra benefit in those warm summer days.


 	Makarius