Re: [isabelle-dev] Timeouts in Flyspeck_Tame
On 16/02/2019 14:07, Florian Haftmann wrote: > Am 14.02.19 um 13:34 schrieb Makarius: >> >> In contrast to my proposal concerning Flyspeck-Tame-Base it is better to >> keep the main AFP document unchanged, e.g. like this: >> >> session Flyspeck-Tame-Eval (very_slow) = Flyspeck-Tame + ... >> >> This will change the timing for Flyspeck-Tame in the recorded database, >> but such renamings occasionally happen over the years. > > See now > https://bitbucket.org/isa-afp/afp-devel/commits/00b771f6c60d99745fb933d4043c1ed123a427e5 Great. This looks fine to me. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Timeouts in Flyspeck_Tame
Am 14.02.19 um 13:34 schrieb Makarius: > On 14/02/2019 12:04, Florian Haftmann wrote: At the moment I am thinking whether the old approach of checking everything except the computations can be restored without using fancy low-level stuff. Maybe by a locale. >>> >>> This is indeed a bit fragile. I used to make manual tests of >>> Flyspeck-Tame over some time, but now ignore that problem. >>> >>> Maybe it is possible to make a non-slow session "Flyspeck-Tame-Base" >>> that does everything except the actual "eval" steps, and postpone the >>> checks to session Flyspeck-Tame (very_slow) = Flyspeck-Tame-Base ... >> >> Something like that indeed. A completeness proof relative to a locale >> which has the computational results as assumption apt for later >> interpretation. > > In contrast to my proposal concerning Flyspeck-Tame-Base it is better to > keep the main AFP document unchanged, e.g. like this: > > session Flyspeck-Tame-Eval (very_slow) = Flyspeck-Tame + ... > > This will change the timing for Flyspeck-Tame in the recorded database, > but such renamings occasionally happen over the years. See now https://bitbucket.org/isa-afp/afp-devel/commits/00b771f6c60d99745fb933d4043c1ed123a427e5 Florian signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Timeouts in Flyspeck_Tame
On 14/02/2019 12:04, Florian Haftmann wrote: >>> At the moment I am thinking whether the old approach of checking >>> everything except the computations can be restored without using fancy >>> low-level stuff. Maybe by a locale. >> >> This is indeed a bit fragile. I used to make manual tests of >> Flyspeck-Tame over some time, but now ignore that problem. >> >> Maybe it is possible to make a non-slow session "Flyspeck-Tame-Base" >> that does everything except the actual "eval" steps, and postpone the >> checks to session Flyspeck-Tame (very_slow) = Flyspeck-Tame-Base ... > > Something like that indeed. A completeness proof relative to a locale > which has the computational results as assumption apt for later > interpretation. In contrast to my proposal concerning Flyspeck-Tame-Base it is better to keep the main AFP document unchanged, e.g. like this: session Flyspeck-Tame-Eval (very_slow) = Flyspeck-Tame + ... This will change the timing for Flyspeck-Tame in the recorded database, but such renamings occasionally happen over the years. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Timeouts in Flyspeck_Tame
>> At the moment I am thinking whether the old approach of checking >> everything except the computations can be restored without using fancy >> low-level stuff. Maybe by a locale. > > This is indeed a bit fragile. I used to make manual tests of > Flyspeck-Tame over some time, but now ignore that problem. > > Maybe it is possible to make a non-slow session "Flyspeck-Tame-Base" > that does everything except the actual "eval" steps, and postpone the > checks to session Flyspeck-Tame (very_slow) = Flyspeck-Tame-Base ... Something like that indeed. A completeness proof relative to a locale which has the computational results as assumption apt for later interpretation. Florian signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Timeouts in Flyspeck_Tame
On 14/02/2019 10:43, Florian Haftmann wrote: > > But https://isabelle.sketis.net/devel/build_status/ still indicates > failure for Flyspec-Tame from Wed 13th. Is there any chance that some > other non-termination proof requiring image_cong_simp [cong del] is > still left in Flyspeck-Tame? Maybe it is just a coincidence, it did work for Isabelle/18cb541a975f vs. AFP/9181c1974aa0, but later failed again for AFP/e064b4022c1c -- see also the "CSV" link on https://isabelle.sketis.net/devel/build_status Later today we should get new measurements. > Btw. that the ancient cond_eval hack has been replaced by a proper tag > has completely slipped out of my attention, hence I didn't notice that > Flyspeck-Tame is completely untested without very_slow. > > At the moment I am thinking whether the old approach of checking > everything except the computations can be restored without using fancy > low-level stuff. Maybe by a locale. This is indeed a bit fragile. I used to make manual tests of Flyspeck-Tame over some time, but now ignore that problem. Several days of unclear situation is a natural consequence of this arrangement. Maybe it is possible to make a non-slow session "Flyspeck-Tame-Base" that does everything except the actual "eval" steps, and postpone the checks to session Flyspeck-Tame (very_slow) = Flyspeck-Tame-Base ... Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Timeouts in Flyspeck_Tame
Am 10.02.19 um 17:01 schrieb Makarius: > On 04/02/2019 14:17, Makarius wrote: >> On 04/02/2019 10:37, Lars Hupel wrote: >>> Is this related to the latest Poly/ML changes? The "slow" job still runs >>> on the x86_64 platform. Last time it worked was 76fbd806ebc5. Hardware >>> is 8-core LRZ VM. >> >> I can confirm this: see >> https://isabelle.sketis.net/devel/build_status/AFP_bulky_64bit_6_threads/index.html >> >> I have switched back to stable polyml-5.7.1-8 for now (see >> Isabelle/a5732629cc46) and will be unavailable for the next few days. > > This did not change the non-termination, but the following helps: > > changeset: 10116:9181c1974aa0 > tag: tip > user:wenzelm > date:Sun Feb 10 16:49:10 2019 +0100 > files: thys/Flyspeck-Tame/PlaneGraphIso.thy > description: > adapted to Isabelle/7e4966eaf781 -- avoid non-termination; > > I have merely applied the recommendation from the NEWS: > > INCOMPATIBILITY; consider using > declare image_cong_simp [cong del] in extreme situations. Thanks for going into this. But https://isabelle.sketis.net/devel/build_status/ still indicates failure for Flyspec-Tame from Wed 13th. Is there any chance that some other non-termination proof requiring image_cong_simp [cong del] is still left in Flyspeck-Tame? Btw. that the ancient cond_eval hack has been replaced by a proper tag has completely slipped out of my attention, hence I didn't notice that Flyspeck-Tame is completely untested without very_slow. At the moment I am thinking whether the old approach of checking everything except the computations can be restored without using fancy low-level stuff. Maybe by a locale. Cheers, Florian signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Timeouts in Flyspeck_Tame
On 04/02/2019 14:17, Makarius wrote: > On 04/02/2019 10:37, Lars Hupel wrote: >> Is this related to the latest Poly/ML changes? The "slow" job still runs >> on the x86_64 platform. Last time it worked was 76fbd806ebc5. Hardware >> is 8-core LRZ VM. > > I can confirm this: see > https://isabelle.sketis.net/devel/build_status/AFP_bulky_64bit_6_threads/index.html > > I have switched back to stable polyml-5.7.1-8 for now (see > Isabelle/a5732629cc46) and will be unavailable for the next few days. This did not change the non-termination, but the following helps: changeset: 10116:9181c1974aa0 tag: tip user:wenzelm date:Sun Feb 10 16:49:10 2019 +0100 files: thys/Flyspeck-Tame/PlaneGraphIso.thy description: adapted to Isabelle/7e4966eaf781 -- avoid non-termination; changeset: 69777:7e4966eaf781 parent: 69767:d10fafeb93c0 user:haftmann date:Thu Jan 31 13:08:59 2019 + files: NEWS src/HOL/Analysis/Caratheodory.thy src/HOL/Analysis/Convex.thy src/HOL/Analysis/Elementary_Topology.thy src/HOL/Analysis/Embed_Measure.thy src/HOL/Analysis/Homotopy.thy src/HOL/Analysis/Sigma_Algebra.thy src/HOL/Binomial.thy src/HOL/Complete_Lattices.thy src/HOL/Enum.thy src/HOL/Fun.thy src/HOL/GCD.thy src/HOL/Hilbert_Choice.thy src/HOL/Hoare_Parallel/RG_Examples.thy src/HOL/Probability/ex/Dining_Cryptographers.thy src/HOL/Set.thy src/HOL/Set_Interval.thy src/HOL/UNITY/Comp/Alloc.thy description: proper congruence rule for image operator I have merely applied the recommendation from the NEWS: INCOMPATIBILITY; consider using declare image_cong_simp [cong del] in extreme situations. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Timeouts in Flyspeck_Tame
On 04/02/2019 10:37, Lars Hupel wrote: > Is this related to the latest Poly/ML changes? The "slow" job still runs > on the x86_64 platform. Last time it worked was 76fbd806ebc5. Hardware > is 8-core LRZ VM. I can confirm this: see https://isabelle.sketis.net/devel/build_status/AFP_bulky_64bit_6_threads/index.html I have switched back to stable polyml-5.7.1-8 for now (see Isabelle/a5732629cc46) and will be unavailable for the next few days. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
