[isabelle-dev] Timeouts in Flyspeck_Tame
florian.haftmann at informatik.tu-muenchen.de
Thu Feb 14 10:43:18 CET 2019
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
>> 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
> 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 228 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev