[isabelle] Spurious abort while building sessions

[Dominique Unruh]

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.

[Lars Hupel]

Hi Dominique,

Post by Dominique Unruh
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

[Dominique Unruh]

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.

Post by Lars Hupel
Hi Dominique,

Post by Dominique Unruh
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

[Lars Hupel]

Post by Dominique Unruh
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.

You could also try to run Poly in 32-bit mode. On Ubuntu, you'll have to
install lib32stdc++6 for that.

Cheers
Lars

[Manuel Eberl]

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

Post by Dominique Unruh
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).
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.