[isabelle-dev] Problems with server room cooling at TUM

Makarius makarius at sketis.net
Mon Aug 19 11:35:14 CEST 2024


On 08/08/2024 15:38, Makarius wrote:
> On 03/08/2024 14:17, Makarius wrote:
>> TUM has problems with cooling of server rooms for a couple of days, although 
>> I am not close enough to know the details. Several servers have been 
>> shutdown down to reduce heat production.
> 
> I hear that there are plans to be back to normal on 14-Aug-2024, afternoon. 
> Further note that 15-Aug-2024 is a local holiday.

We seem to be mostly back to normal, but I now see 2 problems on our side 
(Isabelle/dff10bb4ebdb and AFP/a7ca8592cbc7).


(1) Failure of "isabelle build_task -a":

Transferring repositories ...
*** The column name user was not found in this ResultSet.


(2) Failure of AFP:

Balog_Szemeredi_Gowers FAILED (see also "isabelle build_log -H Error 
Balog_Szemeredi_Gowers")
*** Undefined fact: "of_nat_div_le_of_nat" (line 1248 of 
"~~/dirs/AFP/thys/Balog_Szemeredi_Gowers/Balog_Szemeredi_Gowers_Main_Proof.thy")
*** At command "by" (line 1248 of 
"~~/dirs/AFP/thys/Balog_Szemeredi_Gowers/Balog_Szemeredi_Gowers_Main_Proof.thy")
*** Undefined fact: "of_nat_div_le_of_nat" (line 1202 of 
"~~/dirs/AFP/thys/Balog_Szemeredi_Gowers/Balog_Szemeredi_Gowers_Main_Proof.thy")
*** At command "by" (line 1202 of 
"~~/dirs/AFP/thys/Balog_Szemeredi_Gowers/Balog_Szemeredi_Gowers_Main_Proof.thy")

Crypto_Standards FAILED (see also "isabelle build_log -H Error Crypto_Standards")
*** Undefined fact: "of_nat_div_le_of_nat" (line 1162 of 
"~~/dirs/AFP/thys/Crypto_Standards/SEC1v2_0.thy")
*** At command "using" (line 1162 of 
"~~/dirs/AFP/thys/Crypto_Standards/SEC1v2_0.thy")


See also:

changeset:   14738:a6e01f6ceed8
user:        paulson <lp15 at cam.ac.uk>
date:        Fri Aug 09 20:45:57 2024 +0100
files:       thys/Balog_Szemeredi_Gowers/Balog_Szemeredi_Gowers_Main_Proof.thy 
thys/Crypto_Standards/SEC1v2_0.thy
description:
lemma renaming


	Makarius



More information about the isabelle-dev mailing list