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

[Manuel Eberl]

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
>