[isabelle-dev] Deadlock while building HOL-Proof
Clemens Ballarin
ballarin at in.tum.de
Sat Mar 3 12:09:03 CET 2018
While building HOL-Proof I observe a deadlock, usually after 13 min CPU
time. It can be worked around with ISABELLE_BUILD_OPTIONS="threads=1".
The deadlock occurs most of the time. The earliest changeset I was able
to reproduce this with is
changeset: 67675:738f170f43ee
user: paulson <lp15 at cam.ac.uk>
date: Tue Feb 20 09:34:03 2018 +0000
summary: Merge
This includes changes to HOL/Tools and Pure/Concurrent.
'isabelle build' reports these settings:
ML_PLATFORM="x86-darwin"
ML_HOME="/Users/ballarin/.isabelle/contrib/polyml-5.7.1-5/x86-darwin"
ML_SYSTEM="polyml-5.7.1"
ML_OPTIONS="--minheap 500"
The deadlock happens on a MacBook Pro:
macOS 10.13.3 (17D102)
2,7 GHz Intel Core i5
8 GB 1867 MHz DDR3
Please let me know if I can provide any other useful information.
Clemens
More information about the isabelle-dev
mailing list