[isabelle-dev] Has anyone ever run out of memory trying to *start* to build the AFP?
thomas.sewell at nicta.com.au
Fri Jun 6 06:40:35 CEST 2014
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
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
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.
More information about the isabelle-dev