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



Dear all,

I can confirm this.
when proving False via


theory Scratch
imports Main
begin

lemma False 
proof (intro TrueE)

the system gets lost somehow (on MacOS X 10.9):
- changing the method of (intro TrueE) does not stop the system from evaluation
  (comsuming 100% of CPF and eating > 4 GB of RAM)
- also if one reloads the buffer, everything remains red and evaluation continues
- sometimes even when quitting Isabelle via Cmd-Q, afterwards a poly-process remains which eats up > 4 GB RAM.

Here are some more details:

2 x 2.8 Ghz Quad-Core Intel Xeon
6 GB RAM

ML_PLATFORM="x86_64-darwin"
ML_HOME="/Applications/Isabelle2013-2-RC1.app/Isabelle/contrib/polyml-5.5.1-1/x86_64-darwin"
ML_SYSTEM="polyml-5.5.1-1"
ML_OPTIONS="-H 500"

Best regards,
René

Am 25.11.2013 um 10:27 schrieb bnord <bnord01 at gmail.com>:

> By the way, I could reproduce this under Linux on the same machine (a little less frequent) and could reproduce it under OS X on a different machine only when letting the non-terminating command run for a while. This also left me with a runaway process under OS X which I had to terminate manually after exiting Isabelle/Jedit.
> 
> Best
>    Benedikt
> 
> Am 25.11.13 07:29, schrieb bnord:
>> Hi,
>> 
>> 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.
>> 
>> Best
>>    Benedikt
>> 
>> Am 24.11.2013 19:45, schrieb Makarius:
>>> Dear Isabelle users,
>>> 
>>> this is another attempt to make a stable release of Isabelle this autumn:
>>> 
>>>  http://isabelle.in.tum.de/website-Isabelle2013-2-RC1
>>> 
>>> This is presumably the only release candidate before final lift-off of Isabelle2013-2 in the first days of December.
>>> 
>>> 
>>> Notable changes versus Isabelle2013-1 (from NEWS):
>>> 
>>> *** Prover IDE -- Isabelle/Scala/jEdit ***
>>> 
>>> * More robust editing of running commands with internal forks,
>>> e.g. non-terminating 'by' steps.
>>> 
>>> * More relaxed Sledgehammer panel: avoid repeated application of query
>>> after edits surrounding the command location.
>>> 
>>> 
>>> There should not be any incompatibilites wrt. Isabelle2013-1, which means everybody who is already on the latest release can try out the new release candidate without any extra efforts.
>>> 
>>> 
>>> See also https://bitbucket.org/isabelle_project/isabelle-release for the main website where the Isabelle release process is formally organized. There is also a link to an issue tracker on this Bitbucket site.
>>> 
>>> Observations from testing release candidates may be discussed here on isabelle-users (not isabelle-dev), on the bitbucket tracker, or via private mail.
>>> 
>>> 
>>>    Makarius
>>> 
>> 
> 
> 

-- 
René Thiemann                    mailto:rene.thiemann at uibk.ac.at
Computational Logic Group        http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck





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