Hi Randy,
there are a few sessions with the tag “slow” in the AFP, of which Flyspeck_Tame
is one. These are tested once a day. All other sessions are tested with each
push.
Cheers,
Gerwin
> On 6 Dec 2016, at 12:28 AM, Randy Pollack wrote:
>
> Gerwin,
>
> I was looking at the Flyspeck_Tame
On 05/12/16 17:13, Ondřej Kunčar wrote:
>
> If you remove the call of the function Thm.name_derivation, the cycle gets
> caught. The function
> is internally used in Goal.prove_future. It seems that the promises of the
> theorem in question
> are dropped in the function but we don’t understand
