Stream: Mirror: Isabelle Development Mailing List

Topic: build_task


view this post on Zulip Email Gateway (Jan 30 2026 at 11:59):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>

It is somehow broken. I've made two attempts and it seems to always die like this.

*** '), ('0'::int8), ('0'::int8), ?, ('62474c52-55f8-4ca8-9577-ee151a524bc5')) was aborted: ERROR: duplicate key value violates unique constraint "isabelle_build_sessions_pkey"
*** Detail: Key (name)=(HOL-Matrix_LP) already exists. Call getNextException to see other errors in the batch.
Job ended at Fri Jan 30 12:50:19 GMT+1 2026, with status failed

Larry

view this post on Zulip Email Gateway (Jan 30 2026 at 12:10):

From: Fabian Huch <huch@in.tum.de>

As discussed before, these are leftover entries of a previous abnormal
failure.

I've removed them now in this instance.

Fabian

On 1/30/26 12:58, Lawrence Paulson via isabelle-dev wrote:

It is somehow broken. I've made two attempts and it seems to always die like this.

*** '), ('0'::int8), ('0'::int8), ?, ('62474c52-55f8-4ca8-9577-ee151a524bc5')) was aborted: ERROR: duplicate key value violates unique constraint "isabelle_build_sessions_pkey"
*** Detail: Key (name)=(HOL-Matrix_LP) already exists. Call getNextException to see other errors in the batch.
Job ended at Fri Jan 30 12:50:19 GMT+1 2026, with status failed

Larry


Last updated: Feb 04 2026 at 02:22 UTC