Re: [isabelle-dev] Timeouts in Flyspeck_Tame

2019-02-16 Thread Makarius
On 16/02/2019 14:07, Florian Haftmann wrote: > Am 14.02.19 um 13:34 schrieb Makarius: >> >> In contrast to my proposal concerning Flyspeck-Tame-Base it is better to >> keep the main AFP document unchanged, e.g. like this: >> >> session Flyspeck-Tame-Eval (very_slow) = Flyspeck-Tame + ... >> >>

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

2019-02-16 Thread Florian Haftmann
Am 14.02.19 um 13:34 schrieb Makarius: > On 14/02/2019 12:04, Florian Haftmann wrote: 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. >>> >>> This is indeed a

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

2019-02-14 Thread Makarius
On 14/02/2019 12:04, Florian Haftmann wrote: >>> 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. >> >> This is indeed a bit fragile. I used to make manual tests of

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

2019-02-14 Thread Florian Haftmann
>> 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. > > This is indeed a bit fragile. I used to make manual tests of > Flyspeck-Tame over some time, but now ignore

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

2019-02-14 Thread Makarius
On 14/02/2019 10:43, Florian Haftmann wrote: > > 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? Maybe

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

2019-02-14 Thread 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. >>

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

2019-02-10 Thread 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 >

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

2019-02-04 Thread Makarius
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