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
