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

[Tobias Nipkow]

Yes, I noticed when it happend.

Tobias

On 23/07/2024 11: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.
> 
> 
> Fabian
> 
> 
> On 7/23/24 12:13, Lawrence Paulson wrote:
>> Does anybody know what is going on here? Do we suddenly have two theories 
>> called Ramsey?
>>
>> Larry
>>
>>> Begin forwarded message:
>>>
>>> From: AFP Build <ci at isabelle.systems>
>>> Subject: Build of AFP entry Ramsey-Infinite failed
>>> Date: 23 July 2024 at 02:05:35 BST
>>> To: lp15 at cam.ac.uk
>>>
>>>
>>> The build for the session Ramsey-Infinite belonging to the AFP entry 
>>> Ramsey-Infinite failed.
>>>
>>> You are receiving this mail because you are the maintainer of that AFP entry.
>>>
>>> The following information might help you with resolving the problem.
>>>
>>> Build log: https://build.proof.cit.tum.de/build?name=presentation%2F22
>>>
>>> Isabelle ID:  fbc859ccdaf3
>>> AFP ID:       395f033f6f92
>>> Timeout?      false
>>> Exit code:    1
>>>
>>> Last 50 lines from stdout (if available):
>>>
>>> *** exception THEORY raised (line 378 of "context.ML"):
>>> ***   Duplicate theory name
>>> ***   {..., HOL-Library.FuncSet, HOL-Library.Countable_Set, 
>>> HOL-Library.Equipollence, HOL-Library.Ramsey, Ramsey}
>>> ***   {..., HOL-Library.Infinite_Set, HOL-Library.FuncSet, 
>>> HOL-Library.Countable_Set, HOL-Library.Equipollence, Ramsey}"
>>>
>>> Last 50 lines from stderr (if available):
>>>
>>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4950 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240723/18d07051/attachment.bin>