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

[Fabian Huch]

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