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

[Makarius]

An odd (unexplained) change has occurred on AFP:

changeset:   14197:ddf90847bfa5
user:        immler
date:        Tue Feb 27 15:10:13 2024 +0100
files:       thys/Ordinary_Differential_Equations/Ex/Lorenz/C1/Lorenz_C1.thy 
thys/Ordinary_Differential_Equations/ROOT
description:
enable proof in session Lorenz_C1


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.


Further note that the standard nightly build (isabelle_cronjob) is affected: 
it will probably terminate within 1-3 more days. See also lrzcloud2 on 
https://isatest.sketis.net/devel/cronjob-main.log


So what is the reasoning behind the change ddf90847bfa5? The log does not say 
anything tangible.

Of course it is better to check things formally, instead of having them 
commented-out. So far, I thought that Lorenz_C0 was there to be tested 
properly, and Lorenz_C1 an untested add-on example that is unlikely to fail on 
its own account.

If huge and heavy things like Lorenz_C1 should get a more formal status in 
AFP, we probably need a session group "very_very_slow" or alternatively 
"untested" to say that it is not tested regularly.


	Makarius