Problem with isabelle build_task

[Fabian Huch]

In our discussion yesterday I got slightly confused since we were 
jumping between database updates and inconsistent build database states. 
There are two databases:

- the build database (for the build cluster), that can end up in an 
inconsistent state if the build process was terminated abnormally. This 
can be solved on our installation switching to the build_cluster 
identifier (as the "build" user) and cleaning the db:

   export ISABELLE_IDENTIFIER="build_cluster"

   bin/isabelle build_process -C -r -f

- the build manager database that needs to be updated if the Isabelle 
version running on the server is out of sync with the repository version 
that submits the build_task, SQL-wise. This is done by stopping the 
manager, updating the repository, running

   bin/isabelle build_manager_database -A:

The underlying problem was that 4 GB of JVM seem to be no longer 
sufficient for the "all" job. I've increased the limit to 8GB.


Fabian

On 12/19/24 23:32, Makarius wrote:
> On 19/12/2024 23:06, Makarius wrote:
>>
>> I am presently trying out some variations, directly on the build 
>> manager server, to see if this is the reason, or something completely 
>> different.
>
> I failed to get back to a situation that works, even after reverting 
> all my recent updates of Isabelle components (the local 
> Admin/components/main on the server is changed wrt. the repository 
> version, a copy is attached here).
>
> Even "bin/isabelle build_manager_database -A:" did not help to return 
> to consistent db content, see this error 
> https://build.proof.cit.tum.de/build?name=user%2F927
>
> We need Fabian to sort it out ...
>
>
>     Makarius