<div><div><div><br></div><div><div class="gmail_quote"></div></div></div><div><div dir="ltr" class="gmail_attr">On Thu, Feb 29, 2024 at 10:39 Makarius <<a href="mailto:makarius@sketis.net" target="_blank">makarius@sketis.net</a>> wrote:</div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;border-left-color:rgb(204,204,204)" dir="auto">
So what is the reasoning behind the change ddf90847bfa5? The log does not say <br>
anything tangible.</blockquote></div></div><div><div><div dir="auto">You are right, unfortunately that ended up as a „parrot“ commit message.</div></div></div><div><div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;border-left-color:rgb(204,204,204)" dir="auto"></blockquote><div dir="auto"><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;border-left-color:rgb(204,204,204)" dir="auto"><br>
Of course it is better to check things formally, instead of having them <br>
commented-out.</blockquote></div></div><div><div><div dir="auto">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.</div></div></div><div><div><div dir="auto"><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;border-left-color:rgb(204,204,204)" dir="auto">So far, I thought that Lorenz_C0 was there to be tested <br>
properly, and Lorenz_C1 an untested add-on example that is unlikely to fail on <br>
its own account.</blockquote></div></div><div><div><div dir="auto">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“.</div><div dir="auto"><br></div><div dir="auto">„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.</div><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto"></div></div></div><div><div><div dir="ltr" style="font-family:-apple-system,helveticaneue;font-size:16px;font-style:normal;font-weight:400;letter-spacing:normal;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none;background-color:rgba(0,0,0,0);border-color:rgb(0,0,0);color:rgb(0,0,0)">On Thu, Feb 29, 2024 at 11:55 Makarius <<a href="mailto:makarius@sketis.net" target="_blank" style="font-family:-apple-system,helveticaneue">makarius@sketis.net</a>> wrote:<br></div><blockquote style="width:343px;min-width:150px;font-size:16px;font-style:normal;font-weight:400;letter-spacing:normal;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none;margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;font-family:-apple-system,helveticaneue;background-color:rgba(0,0,0,0);border-color:rgb(0,0,0) rgb(0,0,0) rgb(0,0,0) rgb(204,204,204);color:rgb(0,0,0)" dir="auto">On 29/02/2024 11:33, Fabian Huch wrote:<br>> I heard from Fabian that nowadays the session runs reasonably fast (6 hrs -- <br>> Flyspec-Tame-computation is nearly 5 hrs). But this does not seem to fit with <br>> your results.<br><br>On which hardware precisely?<br></blockquote></div></div><div>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.<div dir="auto"><br></div><div dir="auto">Fabian (Immler)</div><div dir="auto"><br></div>

</div>