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

[Manuel Eberl]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: pEpkey.asc
Type: application/pgp-keys
Size: 1757 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180909/b735d77d/attachment-0002.key>