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

[Makarius]

On 29/02/2024 11:24, Makarius wrote:
> On 29/02/2024 10:38, Makarius wrote:
> 
> It has now terminated as follows (on of1.proof.cit.tum.de):
> 
> Finished Lorenz_C1 (11:29:26 elapsed time, 67:46:46 cpu time, factor 5.90)
> 
> That is something to be investigated. Either there is something odd in the 
> machine configuration, or this bulky test now takes much longer than in 2017.

I now recall, that "slow" and "very_slow" tests are traditionally understood 
in the context of ML_system_64 = true, and that the Lorenz computations were 
slow in the default 64_32 model.

So everything looks like it has always been since 2017.


	Makarius