Email Gateway (Aug 22 2022 at 18:36): Email Gateway (Aug 22 2022 at 18:36):From: Dominique Unruh <unruh@ut.ee>
Hello,
when I run
/opt/Isabelle2018/bin/isabelle build -s -v -b HOL-Library >/tmp/build.log
on my new laptop the build aborts at a random point (or, rarely, completes).
The output says:
HOL-Library CANCELLED
Unfinished session(s): HOL, HOL-Library
Finished at Wed Oct 10 13:26:33 GMT+3 2018
0:01:35 elapsed time, 0:03:56 cpu time, factor 2.46
(full output attached in build.log). There is no error message in the
output besides "CANCELLED". The log (attached file HOL.gz) does not even
contain that.
I am not sure where to even start looking for the reason.
I am running Ubuntu 18.10 beta.
Best wishes,
Dominique.
build.log
HOL.gz
Email Gateway (Aug 22 2022 at 18:36):From: Lars Hupel <hupel@in.tum.de>
Hi Dominique,
on my new laptop the build aborts at a random point (or, rarely, completes).
could you please check journalctl or dmesg for instances of the OOM
killer? I've had that in the past in rare cases.
It may also be wise to set a maximum heap for Poly.
Cheers
Lars
Email Gateway (Aug 22 2022 at 18:36):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I had a similar problem once when we had some thread synchronisation
issues with Poly/ML. It can't be the exact same problem since those
issues only happened at the very end of the ML process, whereas in your
case the problem happens much earlier.
In any case, my guess would be that the ML process dies suddenly before
it can emit any kind of error messages. The OOM killer that Lars hinted
mentioned is a likely suspect.
It might also be interesting to check if this also happens with Pure
(and if yes how often); what I did in the past was to write a small
shell script of "isabelle build -b -c Pure" in a while look that stops
at the first failure. Pure is good for that because it only takes about
10 seconds to build.
Manuel
Email Gateway (Aug 22 2022 at 18:36):From: Dominique Unruh <unruh@ut.ee>
Hi Lars,
good catch! I did not notice that Ubuntu had chosen 1GB for the size of the
swap partition. Clearly too little for an 8GB laptop.
I repartitioned with 8GB swap, and now it works fine.
Thanks a lot!
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 18:36):From: Lars Hupel <hupel@in.tum.de>
You could also try to run Poly in 32-bit mode. On Ubuntu, you'll have to
install lib32stdc++6 for that.
Cheers
Lars
Last updated: Apr 20 2024 at 08:16 UTC