Re: build.proof.cit.tum.de – Key (name)=(Shadow_DOM) already exists

[Fabian Huch]

No, this is just an inconsistent database state left after a previous 
failure that did not terminate properly (presentation/510).

This can simply be resolved by ssh-ing into the build manager ssh host, 
and under the user 'build' (with ISABELLE_IDENTIFIER="build_cluster" 
exported) cleaning the build database:

   isabelle/bin/isabelle build_process -C -r -f

This is done automatically once a day.


Note that I have found the problem leading to the spurious '*** 
Interrupt' (a race condition in Progress.bash) but don't know why the 
interrupted build failed to terminate here.


Fabian


On 12/14/25 11:07, Achim D. Brucker wrote:
> Hi,
> This is just a hunch: there are two theories named Shadow_DOM in two 
> different AFP entries (and, hence, sessions). Could this be the 
> problem, i.e., have any new restrictions regarding the uniqueness of 
> theory names been introduced?
>
> Achim
>
> On 14/12/2025 09:56, Florian Haftmann wrote:
>> There is a problem with the build system:
>>
>> https://build.proof.cit.tum.de/build?id=8d101909-6923-47f7-97a5-4fde4c3ba060 
>>
>>
>> Any thoughts?
>>     Florian
>
>