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 <l...@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

# 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

_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev