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

[Lawrence Paulson]

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):
> 
>