Email Gateway (Dec 14 2025 at 09:56): Email Gateway (Dec 14 2025 at 09:56):From: Florian Haftmann <florian.haftmann@cit.tum.de>
There is a problem with the build system:
https://build.proof.cit.tum.de/build?id=8d101909-6923-47f7-97a5-4fde4c3ba060
Any thoughts?
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Dec 14 2025 at 10:07):From: "Achim D. Brucker" <adbrucker@0x5f.org>
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
Email Gateway (Dec 15 2025 at 08:24):From: Fabian Huch <huch@in.tum.de>
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
Last updated: Dec 17 2025 at 08:33 UTC