Re: [isabelle] Isabelle2013-2-RC1 available for testing



I just worked with Isabelle/jEdit for a few hours, during which it
became unresponsive about 20 times. The reason for becoming
unresponsive were mostly non-terminating proof methods (mostly force,
blast and auto), although in these cases the non-termination did not
lead to consumption of large amounts of memory like with 'intro
TrueE'. By unresponsive, I mean that it will no longer update the
output panel and the text gets a gray background, which is different
from the regular case of non-terminating proof method which will allow
me to continue working in other places of the document. My system
shows that a poly process takes up one entire CPU core, while not
consuming much memory (just a few hundred MB).

Observations:
removing the non-terminating method invocation by editing the text
does not lead to recovery (at least not within a minute)
closing jEdit terminates all associated processes (including the
non-terminating poly process) almost immediately
it seems like try0 never gets stuck with non-terminating proof
methods, always killing them off after the timeout (for instance,
'apply force' may render the IDE irreversibly unresponsive when
applied to a certain goal, while this is not the case when applying
try0 to the same goal)

I'm running Ubuntu 12.10, x64.

On Mon, Nov 25, 2013 at 10:33 PM, Makarius <makarius at sketis.net> wrote:
> On Mon, 25 Nov 2013, bnord wrote:
>
>> when trying the "lemma False by (intro TrueE)" example on Windows many
>> times the whole Isabelle interaction seems to freeze, everything from the
>> previous command becomes a light-gray-pinkish background and there is no
>> Isabelle output/response whatsoever. Sometimes after running for several
>> minutes in the background the process seems to recover somehow.
>
>
> I have made two more rounds over all this.  In the next release candidate
> (in 48 hours) it should work better, although there are always situations
> where Poly/ML cannot be interrupted quickly.  Nonetheless, interruptibility
> of Poly/ML is generally better than other platforms I have seen recently,
> notably OCaml and JVM.
>
>
>         Makarius
>




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.