[isabelle-dev] Fwd: Build of AFP entry Ramsey-Infinite failed

[Makarius]

On 7/23/24 12:54, Fabian Huch wrote:
> The offending changeset seems to be Isabelle/0b8922e351a3:
> 
> - before: https://build.proof.cit.tum.de/build?name=user%2F74
> 
> - after: https://build.proof.cit.tum.de/build?name=user%2F75
> 
> So there seems to be some problem with ZTerm.standard_vars in that session.

Thank you for cleaning after me. I have addressed it now as follows:

changeset:   80613:42408be39d6c
tag:         tip
user:        wenzelm
date:        Tue Jul 23 22:50:59 2024 +0200
files:       src/Pure/Build/export_theory.ML
description:
disable thy_cache for now (amending 0b8922e351a3): avoid crash of 
AFP/Ramsey-Infinite due to exception THEORY "Duplicate theory name";


On Sat and Sun, when preparing for travel to Bonn / HIM, I was unsure if 
the build cluster was working correctly. I did not see any errors, in 
fact I did not see any activity at all. This has happened before, when 
the implicit state on the server was fine and the new test did not 
change any sources.


	Makarius