Re: [isabelle] [ExternalEmail] [isabelle-dev] afp-2016-1 branch

I don't know whether or not this was done in the past, but Lars Hupel
removed this conditional evaluation from Flyspeck_Tame in April 2016 [1]
when he introduced the new CI infrastructure.

All of Flyspeck_Tame now gets tested once a day (it is part of the
isabelle-nightly-slow job in Isabelle/Jenkins [2]).

As for other AFP entries, like Flyspeck_Tame, we have a few ones that
are too big to test on every push like the rest of the AFP and those get
tested in isabelle-nightly-slow. I don't know the AFP in enough detail
to say with certainty that none of them contains any parts that are
skipped during these tests like Flyspeck_Tame used to, but I don't think
so, given that that testing such things is the express purpose of





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.