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

[Fabian Immler]

On Thu, Feb 29, 2024 at 10:39 Makarius <makarius at sketis.net> wrote:

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

You are right, unfortunately that ended up as a „parrot“ commit message.

>

> Of course it is better to check things formally, instead of having them
> commented-out.

That is the motovation for the change: it is better to check things
formally. Talking to Fabian Huch, I got the impression that now there are
more compute resources than five or six years ago.

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.

Mathematically, Lorenz_C0 is of not much value. Lorenz_C1 is a formal proof
for the computational part of Tucker‘s proof of Smale‘s 14th problem. So
Lorenz_C1 is of actual value and worth testing „regularly“.

„Regularly“ could also be weekly, monthly, or even just once for every
Isabelle release. It probably makes sense to reflect that in a new session
group „very_very_slow“ or the like.


On Thu, Feb 29, 2024 at 11:55 Makarius <makarius at sketis.net> wrote:

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

That must have been an Apple M1 Pro, and I believe the run time was about
6-7 hrs, but I did not measure it exactly. But as I said, Lorenz_C1 does
not need to run on a daily basis, so it also does not need to run on the
latest hardware.

Fabian (Immler)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240229/157e052a/attachment.htm>