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

[Tobias Nipkow]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev