While fixing theories in the AFP, I arrived in a strange situation where "isabelle build -D thys" would no longer find and check the remaining unbuilt theories.

Instead, I got a java OutOfMemory exception on the java heap. This is before anything starts building - I take it java has run out of heap just trying to parse all the theories, logs and heaps and figure out what work to do.

Unfortunately I can't exactly reproduce this, since I've since got a theory to build and changed the outcome. Instead isabelle seems to get stuck - after 10 minutes at ~6 cores java still hasn't picked and started any sessions.

In case anyone else gets stuck in this situation, here is my best workaround:

cat thys/*/ROOT | grep session | cut -d' ' -f2 | xargs -n 10 isabelle build -d thys

By focusing on (the dependencies of) 10 sessions at a time, isabelle seems to get the job done.

The grepping and cutting is a bit ugly. Would it make sense to have an equivalent of 'findlogics' which found sessions? That would allow

isabelle findsessions -d (DIR) | xargs -n 10 isabelle build -d (DIR)

If noone else has seen this kind of thing, just ignore me.


isabelle-dev mailing list

Reply via email to