[isabelle-dev] Deadlock while building HOL-Proof

[Makarius]

On 07/03/18 14:09, Makarius wrote:
> On 03/03/18 12:09, Clemens Ballarin wrote:
>> 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
> 
>> The deadlock happens on a MacBook Pro:
>>
>>   macOS 10.13.3 (17D102)
>>   2,7 GHz Intel Core i5
>>   8 GB 1867 MHz DDR3
> 
> Thanks for keeping an eye on such details and for exploring the history
> already.
> 
> Since HOL-Proofs fails occasionally, especially on underpowered
> hardware, I did not take recent failures of it seriously. Looking more
> closely at the build_log test database, I see that from 5a1b299fe4af to
> 0cd2fd0c2dcf (pull_date 19/20-Feb-2018) there is a change from normal
> failure to timeout. It could be due to lazy locale facts and the new
> (parallel) Thm.consolidate_theory operation.
> 
> I will investigate this further and try to isolate the actual problem.

In the first round I made some fine-tuning, without getting to the
bottom of the actual problem:

changeset:   67778:a25f9076a0b3
user:        wenzelm
date:        Wed Mar 07 17:27:57 2018 +0100
files:       src/Pure/more_thm.ML
description:
eliminated somewhat pointless parallelism (from 857da80611ab): usually
hundreds of tasks with < 1ms each, also note that the enclosing
join_theory happens within theory graph parallelism;

changeset:   67779:fd2558014196
user:        wenzelm
date:        Wed Mar 07 17:39:18 2018 +0100
files:       src/Pure/Isar/proof_context.ML src/Pure/global_theory.ML
description:
tuned -- more uniform;


I have also made various experiments to avoid lazy facts (and recorded
proofs) for HOL-Proofs, e.g. in the included changeset. This did not
help much -- maybe the chance to get the problem is slightly decreased.

Since David Matthews has make a lot of changes concerning fine-points of
heap management in the past few months, I would like to test it with
some Poly/ML repository version. But this does not build on macOS at the
moment.


	Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1520444545 -3600
#      Wed Mar 07 18:42:25 2018 +0100
# Node ID d0c8689cc6ac21adcd6a345e6b0b40db4ed3e292
# Parent  fd25580141966e4ec879f6f84046a2ada2be3913
test

diff -r fd2558014196 -r d0c8689cc6ac etc/options
--- a/etc/options	Wed Mar 07 17:39:18 2018 +0100
+++ b/etc/options	Wed Mar 07 18:42:25 2018 +0100
@@ -84,6 +84,8 @@
 
 section "Detail of Proof Checking"
 
+option force_proofs : bool = false
+  -- "force lazy facts when recording proofs (less heap requirements)"
 option record_proofs : int = -1
   -- "set level of proofterm recording: 0, 1, 2, negative means unchanged"
 option quick_and_dirty : bool = false
diff -r fd2558014196 -r d0c8689cc6ac src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Mar 07 17:39:18 2018 +0100
+++ b/src/HOL/ROOT	Wed Mar 07 18:42:25 2018 +0100
@@ -15,7 +15,7 @@
   description {*
     HOL-Main with explicit proof terms.
   *}
-  options [quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
+  options [quick_and_dirty = false, force_proofs, record_proofs = 2, parallel_proofs = 0]
   sessions
     "HOL-Library"
   theories
diff -r fd2558014196 -r d0c8689cc6ac src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Wed Mar 07 17:39:18 2018 +0100
+++ b/src/Pure/global_theory.ML	Wed Mar 07 18:42:25 2018 +0100
@@ -126,19 +126,22 @@
 
 (* enter_thms *)
 
+fun force_register_proofs thms =
+  Thm.register_proofs (if Options.default_bool "force_proofs" then Lazy.force_value thms else thms);
+
 fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy);
 
 fun add_facts arg thy =
   thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2);
 
 fun add_thms_lazy kind (b, thms) thy =
-  if Binding.is_empty b then Thm.register_proofs thms thy
+  if Binding.is_empty b then force_register_proofs thms thy
   else
     let
       val name = Sign.full_name thy b;
       val thms' = thms
         |> Lazy.map_finished (name_thms true true name #> map (Thm.kind_rule kind));
-    in thy |> Thm.register_proofs thms' |> add_facts (b, thms') end;
+    in thy |> force_register_proofs thms' |> add_facts (b, thms') end;
 
 fun enter_thms pre_name post_name app_att (b, thms) thy =
   if Binding.is_empty b then app_att thms thy |-> register_proofs