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 <rpolla...@gmail.com> wrote: > > Gerwin, > > 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 > releases. > > Thanks for any info. > > --Randy > > 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 >> branch. >> >> Cheers, >> Gerwin >> >>> 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. >>> >>> Cheers, >>> Gerwin >>> >>> _______________________________________________ >>> isabelle-dev mailing list >>> isabelle-...@in.tum.de >>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> >> >> _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
