[isabelle-dev] Deadlock while building HOL-Proof

Makarius makarius at sketis.net
Thu Mar 8 13:08:11 CET 2018


On 07/03/18 21:01, Makarius wrote:
> 
> In the first round I made some fine-tuning, without getting to the
> bottom of the actual problem:
> 
> changeset:   67778:a25f9076a0b3
> changeset:   67779:fd2558014196

Today HOL-Proofs happened to work again for f95a163c58bb (before these
changes) and 7655e6369c9f (afterwards), see also
https://isabelle.sketis.net/devel/build_status/Linux_B_2_threads/index.html#session_HOL-Proofs
and
https://isabelle.sketis.net/devel/build_status/Linux_A_2_threads/index.html#session_HOL-Proofs
-- both had a timeout in the past few days.

So this fine-tuning alone does not really change anything.


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

I will continue with the investigations here.


	Makarius



More information about the isabelle-dev mailing list