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
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 failedLarry
Last updated: Feb 04 2026 at 02:22 UTC