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