This message on isabelle-users is related and suggests how to avoid the OutOfMemory:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-April/msg00116.html Tobias On 06/06/2014 06:40, Thomas Sewell wrote: > 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. > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
