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

[Fabian Huch]

On 2/29/24 10:38, Makarius wrote:
> 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
>
I heard from Fabian that nowadays the session runs reasonably fast (6 
hrs -- Flyspec-Tame-computation is nearly 5 hrs). But this does not seem 
to fit with your results.

>
> 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

If it should be nightly we really need high-end hardware here (not 1/4 
slice of a Xeon 4316) -- we won't have free access to these machines for 
much longer anyway.

>
> 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.

Im am in favor of having an "untested" groups vs. commenting out proofs.


Fabian