Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing



I have also been having to occasionally quit and restart Isabelle 2014
jedit when it stops working.

Here is the syslog from the latest problem:

Welcome to Isabelle/HOL (Isabelle2014: August 2014)
poly: gc_mark_phase.cpp:439: virtual void
MTGCProcessMarkPointers::ScanAddressesInObject(PolyObject*, POLYUNSIGNED):
Assertion `baseAddr > (PolyWord*)obj && baseAddr < ((PolyWord*)obj)+length'
failed.

message_output terminated
/usr/local/Isabelle2014/lib/scripts/run-polyml-5.5.2: line 84:  1645
Aborted                 (core dumped) "$POLY" -q -i $ML_OPTIONS --eval
"$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" --error-exit <
/dev/null

rmdir: failed to remove `/tmp/isabelle-harry1631': Directory not empty

standard_error terminated
standard_output terminated
process terminated
command_input terminated
process_manager terminated
Return code: 134

On 29 October 2014 16:21, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch
> wrote:

> Hi Makarius,
>
> Here is another datapoint in the greyout story with Isabelle2014. The
> attached syslog ends with a DUP exception. This time there were no
> exceptions on the command line. The greyout happened again while I was
> using the query panel to find theorems.
>
> My setings are:
>
> JEDIT_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"
> ML_OPTIONS="-H 500 --gcthreads 4"q
>
> Hope this helps,
> Andreas
>
>
> On 10/10/14 13:48, Makarius wrote:
>
>> On Thu, 9 Oct 2014, Andreas Lochbihler wrote:
>>
>>  On 08/10/14 22:51, Makarius wrote:
>>>
>>>> >  Today, I experienced a PIDE greyout again, this time in Isabelle2014
>>>> >  while running
>>>> >  quickcheck. I've attached the Syslog content and the output of error
>>>> >  messages in the
>>>> >  terminal from which I had started Isabelle/jEdit.
>>>>
>>>>  Do you remember anything specific about the situation?  E.g. a very big
>>>>  message being
>>>>  output, say a large subgoal?
>>>>
>>>>  No, everything was quite small, actually. At that time, I was
>>> preparing exercises for
>>> the Isabelle course at ETH, so I just had a single theory file based on
>>> HOL/Main, and
>>> quickcheck normally outputs only small counterexamples.
>>>
>>>   The Isabelle/jEdit settings have these defaults for heap and stack:
>>>>
>>>>     JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss2m"
>>>>     JEDIT_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"
>>>>
>>>>  I had the -Xmx4096m option set before, but I will now also adapt your
>>> settings for -Xss
>>> and -Xms. Let's see what happens.
>>>
>>
>> I will keep an eye on the JVM stack, and experiment with bigger values
>> for a future release.
>>
>> The memory problem is mainly due to the 32bit limitation of our JVM
>> bundle, especially for
>> Windows.  Of course there is a proper 64bit Java for that platform, but
>> we don't use it yet.
>>
>>
>>      Makarius
>>
>> ------------------------------------------------------------
>> ----------------
>>                                http://stop-ttip.org
>> ------------------------------------------------------------
>> ----------------
>>
>



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