On 29/02/2024 17:30, Makarius wrote:
note that ARM is much slower: the analogous test on Mac
Studio M1 from some hours ago is still running, here are some results so far:
Finished HOL (0:02:08 elapsed time, 0:07:09 cpu time, factor 3.33)
Finished HOL-Analysis (0:04:34 elapsed
On 29/02/2024 16:23, Fabian Immler wrote:
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
On Thu, Feb 29, 2024 at 10:39 Makarius 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
On 29/02/2024 11:24, Makarius wrote:
On 29/02/2024 10:38, Makarius wrote:
It has now terminated as follows (on of1.proof.cit.tum.de):
Finished Lorenz_C1 (11:29:26 elapsed time, 67:46:46 cpu time, factor 5.90)
That is something to be investigated. Either there is something odd in the
machine
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
I have forwarded your email to a working email address.
Tobias
On 29/02/2024 11:01, Makarius wrote:
On 29/02/2024 10:38, Makarius wrote:
An odd (unexplained) change has occurred on AFP:
changeset: 14197:ddf90847bfa5
user: immler
I've sent this with CC to immler.emails.immler_email
On 29/02/2024 10:38, Makarius wrote:
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
On 29/02/2024 10:38, Makarius wrote:
An odd (unexplained) change has occurred on AFP:
changeset: 14197:ddf90847bfa5
user: immler
I've sent this with CC to immler.emails.immler_email according to
AFP/38e4f6bce76e metadata, but that address did not work.
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
