Stream: Mirror: Isabelle Development Mailing List

Topic: build_task not working

view this post on Zulip Email Gateway (Mar 27 2025 at 14:34):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
Here’s the output.

Host "of4-proof_classic": init ...
Host "of3-proof_classic": init ...
Host "of2-proof_classic": init ...
Host "of1-proof_classic": init ...
*** Batch entry 0 INSERT INTO "isabelle_build_sessions" VALUES (('HOL-Matrix_LP'), ('HOL'), ('Pure
*** HOL'), (''), ('3388d67c284096209f11b169986ae204ef7cf331 <meta_info>
*** e512a13d839ea34e1dc95b4853b580c309500b04 ~~/src/HOL/ATP.thy
*** fb5c04ec4758211546d540118f08450c5d57ab05 ~~/src/Tools/subtyping.ML
*** 97f6449e53d782a57a5af30e8df922ac66e4f9da ~~/src/Tools/try.ML
*** '), ('0'::int8), ('0'::int8), '\x'::bytea, ('af33ee54-8201-4e9e-bc5b-03a6b9474d55')) 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.

view this post on Zulip Email Gateway (Mar 27 2025 at 14:48):

From: Fabian Huch <huch@in.tum.de>
That is due to a previous build leaving the build database in an
inconsistent state (it is resetted daily but I've now done it manually).

Perhaps we could detect if there is a pending but inactive build in the
database (and remove the remnants), before attempting to start a new build?

Fabian

On 3/27/25 15:33, Lawrence Paulson via isabelle-dev wrote:

Here’s the output.

Host "of4-proof_classic": init ...
Host "of3-proof_classic": init ...
Host "of2-proof_classic": init ...
Host "of1-proof_classic": init ...
*** Batch entry 0 INSERT INTO "isabelle_build_sessions" VALUES (('HOL-Matrix_LP'), ('HOL'), ('Pure
*** HOL'), (''), ('3388d67c284096209f11b169986ae204ef7cf331 <meta_info>
*** e512a13d839ea34e1dc95b4853b580c309500b04 ~~/src/HOL/ATP.thy
*** fb5c04ec4758211546d540118f08450c5d57ab05 ~~/src/Tools/subtyping.ML
*** 97f6449e53d782a57a5af30e8df922ac66e4f9da ~~/src/Tools/try.ML
*** '), ('0'::int8), ('0'::int8), '\x'::bytea, ('af33ee54-8201-4e9e-bc5b-03a6b9474d55')) 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.

Last updated: Apr 18 2025 at 20:21 UTC