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