Am 10.02.19 um 17:01 schrieb 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; > > I have merely applied the recommendation from the NEWS: > > INCOMPATIBILITY; consider using > declare image_cong_simp [cong del] in extreme situations.
Thanks for going into this. But https://isabelle.sketis.net/devel/build_status/ still indicates failure for Flyspec-Tame from Wed 13th. Is there any chance that some other non-termination proof requiring image_cong_simp [cong del] is still left in Flyspeck-Tame? Btw. that the ancient cond_eval hack has been replaced by a proper tag has completely slipped out of my attention, hence I didn't notice that Flyspeck-Tame is completely untested without very_slow. At the moment I am thinking whether the old approach of checking everything except the computations can be restored without using fancy low-level stuff. Maybe by a locale. Cheers, Florian
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
