I've removed the two rules from continuous_intros as of 1254f3e57fed. Manuel
On 07/09/2018 14:56, Makarius wrote: > On 02/09/18 16:00, Manuel Eberl wrote: >> Okay I did some more experiments and I was now, interestingly enough, >> completely unable to reproduce the situation where Green /didn't/ >> timeout. So I have no idea what was going on there; perhaps I made a >> mistake in testing it. I don't know. >> >> It might be wise to remove "continuous_on_discrete" etc. from >> intro/continuous_intros and declare it as a simp rule instead. I'm still >> not quite sure what causes these problems. > The official isabelle-dev test results show that Ergodic_Theory and Lp > have suffered a lot: > > https://isabelle.sketis.net/devel/build_status/AFP/index.html#session_Ergodic_Theory > https://isabelle.sketis.net/devel/build_status/AFP/index.html#session_Lp > > > Here are some manual measurements: > > Isabelle/9207ada0ca31 + AFP/6d7e0f6b8096 > Finished HOL (0:03:18 elapsed time, 0:11:01 cpu time, factor 3.33) > Finished HOL-Analysis (0:05:44 elapsed time, 0:26:07 cpu time, factor 4.55) > Finished HOL-Probability (0:01:15 elapsed time, 0:05:25 cpu time, factor > 4.30) > Finished Lp (0:00:15 elapsed time, 0:01:03 cpu time, factor 4.21) > > Isabelle/f443ec10447d + AFP/6d7e0f6b8096 > Finished HOL (0:03:19 elapsed time, 0:11:03 cpu time, factor 3.33) > Finished HOL-Analysis (0:05:58 elapsed time, 0:27:06 cpu time, factor 4.54) > Finished HOL-Probability (0:01:16 elapsed time, 0:05:24 cpu time, factor > 4.22) > Finished Lp (0:02:41 elapsed time, 0:03:42 cpu time, factor 1.38) > > > So it is probably better to revise the rule declarations in main HOL. > > > Makarius
pEpkey.asc
Description: application/pgp-keys
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev