[isabelle-dev] Timeouts in Flyspeck_Tame

[Makarius]

On 04/02/2019 14:17, Makarius wrote:
> On 04/02/2019 10:37, Lars Hupel wrote:
>> Is this related to the latest Poly/ML changes? The "slow" job still runs
>> on the x86_64 platform. Last time it worked was 76fbd806ebc5. Hardware
>> is 8-core LRZ VM.
> 
> I can confirm this: see
> https://isabelle.sketis.net/devel/build_status/AFP_bulky_64bit_6_threads/index.html
> 
> I have switched back to stable polyml-5.7.1-8 for now (see
> Isabelle/a5732629cc46) and will be unavailable for the next few days.

This did not change the non-termination, but the following helps:

changeset:   10116:9181c1974aa0
tag:         tip
user:        wenzelm
date:        Sun Feb 10 16:49:10 2019 +0100
files:       thys/Flyspeck-Tame/PlaneGraphIso.thy
description:
adapted to Isabelle/7e4966eaf781 -- avoid non-termination;

changeset:   69777:7e4966eaf781
parent:      69767:d10fafeb93c0
user:        haftmann
date:        Thu Jan 31 13:08:59 2019 +0000
files:       NEWS src/HOL/Analysis/Caratheodory.thy
src/HOL/Analysis/Convex.thy src/HOL/Analysis/Elementary_Topology.thy
src/HOL/Analysis/Embed_Measure.thy src/HOL/Analysis/Homotopy.thy
src/HOL/Analysis/Sigma_Algebra.thy src/HOL/Binomial.thy
src/HOL/Complete_Lattices.thy src/HOL/Enum.thy src/HOL/Fun.thy
src/HOL/GCD.thy src/HOL/Hilbert_Choice.thy
src/HOL/Hoare_Parallel/RG_Examples.thy
src/HOL/Probability/ex/Dining_Cryptographers.thy src/HOL/Set.thy
src/HOL/Set_Interval.thy src/HOL/UNITY/Comp/Alloc.thy
description:
proper congruence rule for image operator


I have merely applied the recommendation from the NEWS:

  INCOMPATIBILITY; consider using
  declare image_cong_simp [cong del] in extreme situations.


	Makarius