[isabelle] Spurious abort while building sessions (de Vilhena)

Paulo Emílio de Vilhena

2018-10-17 23:28:32 UTC

Hello,

I have a similar problem with some theories: Isabelle will abort whenever I
open a certain theory on jedit. I've tried to enhance the swap size but it
didn't work (I wasn't running out of RAM actually). Does someone have an
idea on how to solve this problem?

Thanks,

Paulo

Send Cl-isabelle-users mailing list submissions to
To subscribe or unsubscribe via the World Wide Web, visit
https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users
or, via email, send a message with subject or body 'help' to
You can reach the person managing the list at
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Cl-isabelle-users digest..."
1. Re: Spurious abort while building sessions (Lars Hupel)
2. Re: Spurious abort while building sessions (Manuel Eberl)
3. Re: Spurious abort while building sessions (Dominique Unruh)
4. Re: Spurious abort while building sessions (Lars Hupel)
5. 'hence' and 'thus' (Stepan Holub)
6. Re: 'hence' and 'thus' (Tobias Nipkow)
----------------------------------------------------------------------
Message: 1
Date: Wed, 10 Oct 2018 13:10:02 +0200
Subject: Re: [isabelle] Spurious abort while building sessions
Content-Type: text/plain; charset=utf-8
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
------------------------------
Message: 2
Date: Wed, 10 Oct 2018 13:33:41 +0200
Subject: Re: [isabelle] Spurious abort while building sessions
Content-Type: text/plain; charset=utf-8
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

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.

------------------------------
Message: 3
Date: Wed, 10 Oct 2018 15:10:25 +0300
Subject: Re: [isabelle] Spurious abort while building sessions
<
Content-Type: text/plain; charset="UTF-8"
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.

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

------------------------------
Message: 4
Date: Wed, 10 Oct 2018 14:13:14 +0200
Subject: Re: [isabelle] Spurious abort while building sessions
Content-Type: text/plain; charset=utf-8

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
------------------------------
Message: 5
Date: Wed, 10 Oct 2018 14:47:25 +0200
Subject: [isabelle] 'hence' and 'thus'
Content-Type: text/plain; charset=utf-8; format=flowed

Isar commands 'hence' and 'thus' are merely historic: they came from
Mizar into John Harrison's Mizar mode. In very early Isar versions
(approx. 1998) I merely copied them from there. Later I refined the Isar
language quite a lot (2001/2002, 2015/2016) without reconsidering this
legacy: proofs become shorter and more maintainable by*not* using
'hence' and 'thus' anymore. (That is the standard Isar style since 2006.)

Hello,
does this mean that the section 4.1.1. of the tutorial "Programming and
Proving in
Isabelle/HOL" is outdated?
That would be a bit unfortunate, since any new user is likely to trust
the chapter named "Isar by example" in a the first file found under
"Tutorials" in the brand new distribution.
Best
Stepan
------------------------------
Message: 6
Date: Thu, 11 Oct 2018 13:10:14 +0200
Subject: Re: [isabelle] 'hence' and 'thus'
Content-Type: text/plain; charset="utf-8"

2006.)

Hello,
does this mean that the section 4.1.1. of the tutorial "Programming and

Proving in

Isabelle/HOL" is outdated?

No, these commands work fine and many users are attached to them.
Tobias

That would be a bit unfortunate, since any new user is likely to trust

the

chapter named "Isar by example" in a the first file found under

"Tutorials" in

the brand new distribution.
Best
Stepan

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/attachments/20181011/d02f5461/attachment.p7s
End of Cl-isabelle-users Digest, Vol 160, Issue 8
*************************************************