Stream: Mirror: Isabelle Development Mailing List

Topic: Problem with isabelle build_task

Email Gateway (Dec 19 2024 at 12:51):

From: Florian Haftmann <florian.haftmann@cit.tum.de>
On

isabelle: 24c1edcbcc6b tip
afp: 209f3131a057 tip

command

isabelle build_task -A : -a

yields

*** Unable to convert bytea parameter at position 7 to literal

https://build.proof.cit.tum.de/build?id=c2a000a2-aa24-4481-806e-196c5a06fa4d

Whats going wrong here?

Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

Email Gateway (Dec 19 2024 at 22:07):

From: Makarius <makarius@sketis.net>
On 19/12/2024 13:50, Florian Haftmann wrote:

*** Unable to convert bytea parameter at position 7 to literal

https://build.proof.cit.tum.de/build?id=c2a000a2-aa24-4481-806e-196c5a06fa4d

Whats going wrong here?

I've seen this and a few other breakdowns as well, shortly after I've updated
some relevant Isabelle components, e.g. see Isabelle/f48597f265ff.

I am presently trying out some variations, directly on the build manager
server, to see if this is the reason, or something completely different.

Makarius

Email Gateway (Dec 19 2024 at 22:33):

From: Makarius <makarius@sketis.net>
On 19/12/2024 23:06, Makarius wrote:

I am presently trying out some variations, directly on the build manager
server, to see if this is the reason, or something completely different.

I failed to get back to a situation that works, even after reverting all my
recent updates of Isabelle components (the local Admin/components/main on the
server is changed wrt. the repository version, a copy is attached here).

Even "bin/isabelle build_manager_database -A:" did not help to return to
consistent db content, see this error
https://build.proof.cit.tum.de/build?name=user%2F927

We need Fabian to sort it out ...

Makarius

main

Email Gateway (Dec 20 2024 at 07:41):

From: Fabian Huch <huch@in.tum.de>
In our discussion yesterday I got slightly confused since we were
jumping between database updates and inconsistent build database states.
There are two databases:

• the build database (for the build cluster), that can end up in an
  inconsistent state if the build process was terminated abnormally. This
  can be solved on our installation switching to the build_cluster
  identifier (as the "build" user) and cleaning the db:

export ISABELLE_IDENTIFIER="build_cluster"

bin/isabelle build_process -C -r -f

• the build manager database that needs to be updated if the Isabelle
  version running on the server is out of sync with the repository version
  that submits the build_task, SQL-wise. This is done by stopping the
  manager, updating the repository, running

bin/isabelle build_manager_database -A:

The underlying problem was that 4 GB of JVM seem to be no longer
sufficient for the "all" job. I've increased the limit to 8GB.

Fabian

On 12/19/24 23:32, Makarius wrote:

On 19/12/2024 23:06, Makarius wrote:

I am presently trying out some variations, directly on the build
manager server, to see if this is the reason, or something completely
different.

I failed to get back to a situation that works, even after reverting
all my recent updates of Isabelle components (the local
Admin/components/main on the server is changed wrt. the repository
version, a copy is attached here).

Even "bin/isabelle build_manager_database -A:" did not help to return
to consistent db content, see this error
https://build.proof.cit.tum.de/build?name=user%2F927

We need Fabian to sort it out ...

Makarius

Last updated: Feb 01 2025 at 20:19 UTC