[isabelle-dev] Build Manager problem

[Fabian Huch]

This means that the build database was left in an undefined state after 
a previous failure -- in such a case, one can clean it up with:


ssh build.proof.cit.tum.de

sudo su - build

export ISABELLE_IDENTIFIER="build_cluster"

isabelle build_process -C -r -f


The database is cleaned automatically for every nightly build.



Fabian


On 10/21/24 19:16, Makarius wrote:
> We have a problem with the Build Manager database:
>
> *** Batch entry 0 INSERT INTO "isabelle_build_sessions" VALUES 
> (('Shadow_DOM'), ('Core_DOM'), ('Pure
> *** HOL
> *** HOL-Library
> *** Core_DOM'), (''), ('1ba926c267c761faab03e3fc034bdd537a6eba09 
> <meta_info>
> ...
> *** '), ('3600000'::int8), ('172459'::int8), ?, 
> ('41e2f25d-19af-41f0-8e90-f50d455f64f8')) was aborted: ERROR: 
> duplicate key value violates unique constraint 
> "isabelle_build_sessions_pkey"
> ***   Detail: Key (name)=(Shadow_DOM) already exists.  Call 
> getNextException to see other errors in the batch.
>
> https://build.proof.cit.tum.de/build?id=445859c1-0a95-4653-9f47-dc3ba4a75fce 
>
>
>
> Any ideas?
>
>
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev