[isabelle-dev] HOL-Nominal-Examples starving on lxbroy10

[Lawrence Paulson]

This reminds me of a problem I used to have a couple of years ago: building Isabelle/HOL, CPU utilisation would suddenly drop to 0% about three minutes in. This didn’t always happen, but if it did, it happened at a precisely reproducible time. Surely something was waiting for some event. The problem eventually went away but I don’t recall that it was actually solved.

Larry

> On 29 Jun 2020, at 07:56, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
> There are possibly related issues with
> HOL-Analysis/HOL-Complex_Analysis. We have 5 consecutive failed builds,
> two where HOL-Analysis gets aborted with "Interrupt"
> 
> https://ci.isabelle.systems/jenkins/job/isabelle-all/2075/
> https://ci.isabelle.systems/jenkins/job/isabelle-all/2079/
> 
> and three where HOL-Complex_Analysis just timed out after 180 minutes:
> 
> https://ci.isabelle.systems/jenkins/job/isabelle-all/2076/
> https://ci.isabelle.systems/jenkins/job/isabelle-all/2077/
> https://ci.isabelle.systems/jenkins/job/isabelle-all/2078/
> 
> On my laptop, HOL-Complex_Analysis takes less than a minute. On the
> Jenkins machine, it normally takes about 1.5 seconds, so this is clearly
> not a genuine timeout.
> 
> The most recent build seems to work so far though:
> https://ci.isabelle.systems/jenkins/job/isabelle-all/2080/
> 
> I'm at a loss here.
> 
> Manuel
> 
> On 28/06/2020 17:32, Florian Haftmann wrote:
>> Dear Makarius,
>> 
>> I'm reproducibly running into a mysterious build issue on lxbroy10.
>> 
>> Using hg id
>> 
>> 	 6678e4d9508f
>> 
>> and settings
>> 
>> 	ML_SYSTEM=polyml-5.8.1
>> 	ML_PLATFORM=x86_64_32-linux
>> 	ML_OPTIONS=--minheap 500
>> 	ISABELLE_TOOL_JAVA_OPTIONS=-Djava.awt.headless=true -Xms512m -Xmx4g
>> -Xss16m -Xmx8g
>> 
>> a
>> 
>> 	isabelle build HOL-Nominal-Examples
>> 
>> does not terminate after a few hours, leaving a java and a polyml
>> process with no significant resource usage.
>> 
>> I'm at a loss to diagnose what's going on here.
>> 
>> Maybe a side effect of recent renovation of the build process?
>> 
>> I would appreciate if you can have a look at it.
>> 
>> Greetings,
>> 	Florian
>> 
>> 
>> 
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev