[isabelle-dev] Timeouts in Flyspeck_Tame

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190214/8725877d/attachment.sig>