Email Gateway (Dec 30 2025 at 19:49): Email Gateway (Dec 30 2025 at 19:49):From: Florian Haftmann <florian.haftmann@cit.tum.de>
There is a reproducible break down in the build system:
https://build.proof.cit.tum.de/build?id=038ecd8c-6a3e-4e55-bacd-a455cf7f6b40
A few weeks ago there was a similar break down.
What is going on here?
Thanks a lot,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Jan 01 2026 at 21:47):From: Makarius <makarius@sketis.net>
On 30/12/2025 20:49, Florian Haftmann wrote:
There is a reproducible break down in the build system:
https://build.proof.cit.tum.de/build?id=038ecd8c-6a3e-4e55-bacd-a455cf7f6b40
Thanks for the hint. I have now reset the database state of the build server.
A few weeks ago there was a similar break down.
What is going on here?
There is some fragility in the design and/or implementation of the cluster.
Rather soon, I need to sit down with Fabian Huch, to sort it out.
Makarius
Email Gateway (Jan 02 2026 at 08:16):From: Tobias Nipkow <nipkow@in.tum.de>
Unfortunately the build system has hit the same problem again.
Tobias
On 01/01/2026 22:46, Makarius wrote:
On 30/12/2025 20:49, Florian Haftmann wrote:
There is a reproducible break down in the build system:
https://build.proof.cit.tum.de/build?id=038ecd8c-6a3e-4e55-bacd-a455cf7f6b40
Thanks for the hint. I have now reset the database state of the build server.
A few weeks ago there was a similar break down.
What is going on here?
There is some fragility in the design and/or implementation of the cluster.
Rather soon, I need to sit down with Fabian Huch, to sort it out.Makarius
Email Gateway (Jan 02 2026 at 21:08):From: Makarius <makarius@sketis.net>
On 02/01/2026 09:15, Tobias Nipkow wrote:
Unfortunately the build system has hit the same problem again.
I have reset everything once more, and tried "isabelle build_task -a"
successfully.
Hopefully this is sufficient for the rest of the Christmas vacation. I will be
mostly unavailable at least until 07-Jan-2026.
Makarius
Email Gateway (Jan 06 2026 at 11:47):From: Fabian Huch <huch@in.tum.de>
There are two problems here:
the underlying problem is that the Isabelle/Scala process uses up a
lot more memory than it used to, causing OOM errors.
the build infrastructure cannot handle build processes that have
abnormally terminated.
To address this, we can:
(1) tune memory settings and investigate into why we're using up so much
more JVM memory than before -- I'll look into that first.
(2) Make the system more robust in the face of such problems. I need to
sit down with Makarius to discuss this.
(3) Make the scheduling aware of memory limitations. The system was
designed such that this is possible, but it requires more work. I'll
work on that once the immediate problems are solved.
Fabian
On 1/2/26 22:08, Makarius wrote:
On 02/01/2026 09:15, Tobias Nipkow wrote:
Unfortunately the build system has hit the same problem again.
I have reset everything once more, and tried "isabelle build_task -a"
successfully.Hopefully this is sufficient for the rest of the Christmas vacation. I
will be mostly unavailable at least until 07-Jan-2026.Makarius
Last updated: Jan 07 2026 at 16:34 UTC