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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
