[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