[isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

[Makarius]

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