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

[Makarius]

On 29/02/2024 10:38, Makarius wrote:
> 
> Looking briefly into the history reveals this evidence:
> 
> changeset:   8561:13b3e24a71b0
> user:        wenzelm
> date:        Mon Nov 20 07:50:03 2017 +0100
> files:       thys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_C1.thy 
> thys/Ordinary_Differential_Equations/ROOT
> description:
> adapted to timing on lxcisa0 with threads=8: (8:08:58 elapsed time, 47:18:51 
> cpu time, factor 5.81);
> 
> Although lxcisa0 has grown old, it is still representative for the performance 
> baseline of testing.
> 
> Yesterday, I've started the session on more current hardware to see how it 
> works now, but that is still running. Maybe something else is wrong on that 
> machine.

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.


	Makarius