Email Gateway (Jun 25 2025 at 19:33): Email Gateway (Jun 25 2025 at 19:33):From: Florian Haftmann <florian.haftmann@cit.tum.de>
*** Unable to convert bytea parameter at position 7 to literal
Job ended at Wed Jun 25 21:29:15 GMT+2 2025, with status failed
https://build.proof.cit.tum.de/build?id=e42c0340-8807-4c4c-b9c4-64757f490958
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Jun 26 2025 at 08:16):From: Fabian Huch <huch@in.tum.de>
Those are due to repeated crashes because of memory problems since
yesterday afternoon:
* * java.lang.OutOfMemoryError: Java heap space
*** Ran out of memory retrieving query results.
I am not yet sure what causes the increased memory consumption.
Fabian
On 6/25/25 21:32, Florian Haftmann wrote:
*** Unable to convert bytea parameter at position 7 to literal
Job ended at Wed Jun 25 21:29:15 GMT+2 2025, with status failedhttps://build.proof.cit.tum.de/build?id=e42c0340-8807-4c4c-b9c4-64757f490958
Email Gateway (Jun 26 2025 at 08:55):From: Fabian Huch <huch@in.tum.de>
I think the problem comes from Isabelle/0e36478a1b6a. Initializing the
PIDE Session inside Session_Job creates a null store:
override val store:Store =store
so each call of Session.cache creates a new cache, allocating additional
memory. It looks like the intention of the above assignment is to assign
the store from the build context?
Fabian
On 6/26/25 10:15, Fabian Huch wrote:
Those are due to repeated crashes because of memory problems since
yesterday afternoon:* * java.lang.OutOfMemoryError: Java heap space
*** Ran out of memory retrieving query results.I am not yet sure what causes the increased memory consumption.
Fabian
On 6/25/25 21:32, Florian Haftmann wrote:
*** Unable to convert bytea parameter at position 7 to literal
Job ended at Wed Jun 25 21:29:15 GMT+2 2025, with status failedhttps://build.proof.cit.tum.de/build?id=e42c0340-8807-4c4c-b9c4-64757f490958
Email Gateway (Jun 26 2025 at 15:20):From: Makarius <makarius@sketis.net>
On 26/06/2025 10:55, Fabian Huch wrote:
I think the problem comes from Isabelle/0e36478a1b6a. Initializing the PIDE
Session inside Session_Job creates a null store:override val store:Store =store
so each call of Session.cache creates a new cache, allocating additional
memory. It looks like the intention of the above assignment is to assign the
store from the build context?
There is indeed something wrong. See now:
changeset: 82769:7cb5ef6da1f0
user: wenzelm
date: Thu Jun 26 17:14:01 2025 +0200
files: src/Pure/Build/build_job.scala src/Pure/PIDE/session.scala
description:
proper build_context.store, instead of circular null value (amending
0e36478a1b6a and e891ff63e6db);
Makarius
Last updated: Jul 12 2025 at 16:25 UTC