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
> On 6 Dec 2016, at 12:28 AM, Randy Pollack <rpolla...@gmail.com> wrote:
> I was looking at the Flyspeck_Tame entry in the AFP today. The
> current version of proofs built in Isabelle 2016 in a few minutes.
> But there is more to this development than checking the proofs. There
> are "Proofs by evaluation using generated code" that are only executed
> if ISABELLE_FULL_TEST=true. These proofs by evaluation take several
> hours to run.
> I wonder if these proofs by evaluation are checked when the AFP is
> brought up-to-date with a new release of Isabelle? Similarly, do
> other AFP entries have parts that may not be getting checked with new
> Thanks for any info.
> On Wed, Nov 30, 2016 at 11:46 AM, <gerwin.kl...@data61.csiro.au> wrote:
>> As of 61df7b06f131 there is now a new branch afp-2016-1, which will become
>> the new afp release branch when Isabelle2016-1 is released.
>> Any further changes to afp-devel will now by default not show up in this
>>> On 28 Nov 2016, at 6:08 PM, gerwin.kl...@data61.csiro.au wrote:
>>> Since the Isabelle2016-1 release is approaching, we will be preparing the
>>> new afp-2016-1 release branch as well.
>>> If there are any urgent changes or updates to afp-devel that still need to
>>> go into afp-2016-1, please let me know. I am planning to fork off the
>>> branch in two days. Changes after that will not make it into the release.
>>> isabelle-dev mailing list
isabelle-dev mailing list