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
>> 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
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
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.
>>
