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

[Makarius]

On 28/06/2020 17:32, Florian Haftmann wrote:
> 
> 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.

I have experimented with it several times, but could not reproduce the problem.

In the past few months, I did see occasional failures of HOL-Nominal-Examples
due to resource problems, when many build jobs run in parallel (but not such
"hangs"). In such situations, I just ran it again and it usually worked.


> Maybe a side effect of recent renovation of the build process?

Does "isabelle build pide_session=false" make a difference.

Did you use option -N?

What is your value for option -j and -o threads?


> I would appreciate if you can have a look at it.

I still need to revisit a few pending aspects of this seemingly trivial
upgrade of isabelle build.


	Makarius

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20200701/ba99dac9/attachment.sig>