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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
