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
