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

[Makarius]

On 29/02/2024 11:33, Fabian Huch wrote:
> 
> 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.

On which hardware precisely?

This question also touches Intel vs. ARM: the native ARM Poly/ML is incredibly 
fast in most applications, but can be slower in some of these computations. I 
did not investigate this systematically so far.

Presently we are testing Intel only.


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

Concerning the unequal, but related brothers Lorenz_C0 and Lorenz_C1, I have 
now collected all available timing information since 2017. The command-line 
for that is "isabelle build_status -S Lorenz_C0 -l 10000", but it requires 
access to a non-public PostgreSQL server. The result is in the attached .csv: 
nothing special to be seen here, looks fine.


	Makarius
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Lorenz_C0.csv
Type: text/csv
Size: 137119 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240229/8e584aa7/attachment-0001.csv>