[isabelle-dev] AFP: "enable proof in session Lorenz_C1"^

[Makarius]

On 29/02/2024 17:30, Makarius wrote:
> 
> note that ARM is much slower: the analogous test on Mac 
> Studio M1 from some hours ago is still running, here are some results so far:
> 
>        Finished HOL (0:02:08 elapsed time, 0:07:09 cpu time, factor 3.33)
>        Finished HOL-Analysis (0:04:34 elapsed time, 0:21:46 cpu time, factor 
> 4.77)
>        Finished Ordinary_Differential_Equations (0:01:06 elapsed time, 0:04:11 
> cpu time, factor 3.81)
>        Finished Lorenz_C0 (0:17:58 elapsed time, 1:45:23 cpu time, factor 5.86)

I've now killed that test after it had accumulated > 60h CPU time without 
terminating.

See further AFP/fd41e17fc7bd, where we are back to sanity for now.


	Makarius