build_task not working

[Fabian Huch]

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.
>
>