[isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP
eberlm at in.tum.de
Sun Sep 9 20:30:32 CEST 2018
I've removed the two rules from continuous_intros as of 1254f3e57fed.
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:
> 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
> 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
> 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 1757 bytes
Desc: not available
More information about the isabelle-dev