[isabelle-dev] Has anyone ever run out of memory trying to *start* to build the AFP?

[Thomas Sewell]

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.

Cheers,
     Thomas.