Email Gateway (Aug 22 2022 at 14:30): Email Gateway (Aug 22 2022 at 14:30):From: Gerwin.Klein@data61.csiro.au
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
Email Gateway (Aug 22 2022 at 14:47):From: Randy Pollack <rpollack@inf.ed.ac.uk>
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
Email Gateway (Aug 22 2022 at 14:47):From: Manuel Eberl <eberlm@in.tum.de>
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
nightly-slow.
Cheers,
Manuel
[2] https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/
Email Gateway (Aug 22 2022 at 14:47):From: Lars Hupel <hupel@in.tum.de>
I did check for build conditions and occurrences of ISABELLE_FULL_TEST.
All of these should have been eliminated. In case anyone notices
leftover conditional builds (except for code generator checks), that
would be a bug.
Cheers
Lars
Email Gateway (Aug 22 2022 at 14:47):From: Gerwin.Klein@data61.csiro.au
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
Email Gateway (Aug 22 2022 at 14:48):From: Makarius <makarius@sketis.net>
The word "bug" always triggers critical questions. Can you explain the
point of removing the conditional build?
We are talking about these two changesets:
changeset: 2646:3dcc6b9eae2b
user: wenzelm
date: Wed Jan 11 21:30:05 2012 +0100
files: thys/Flyspeck-Tame/ArchComp.thy
description:
method "cond_eval" reduces total runtime to a few minutes if
FLYSPECK_SKIP_PROOFS=true;
changeset: 6524:cac201d3f3f9
user: Lars Hupel <lars.hupel@mytum.de>
date: Fri Apr 15 17:28:43 2016 +0200
files: thys/Flyspeck-Tame/ArchComp.thy thys/Flyspeck-Tame/ROOT
description:
full test for Flyspeck-Tame; get rid of ISABELLE_FULL_TEST
The optional version of Flyspeck-Tame had the advantage that the
relevant part for the test always happens quickly (without "slow" or
"very_slow" categorization). The full test -- which never failed in its
whole history -- was done once and a while (I think weekly).
This saved both CPU time and interactive testing time: I now find myself
doing manual Flyspeck-Tests, imitating the missing condition in the
Prover IDE by hand.
Makarius
Last updated: Apr 26 2024 at 16:20 UTC