build_task not working

Lawrence Paulson lp15 at cam.ac.uk
Thu Mar 27 15:33:37 CET 2025


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.




More information about the isabelle-dev mailing list