Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Build Manager problem

Email Gateway (Oct 21 2024 at 17:17):

From: Makarius <makarius@sketis.net>
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@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Email Gateway (Oct 21 2024 at 17:37):

From: Fabian Huch <huch@in.tum.de>
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@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Email Gateway (Oct 21 2024 at 17:50):

From: Makarius <makarius@sketis.net>
On 21/10/2024 19:36, Fabian Huch wrote:

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

OK, this works.

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Dec 21 2024 at 16:20 UTC