Re: [isabelle-dev] Has anyone ever run out of memory trying to *start* to build the AFP?
On Fri, 6 Jun 2014, Thomas Sewell wrote: 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) I take this as a reminder that isabelle findlogics is actually legacy for Proof General, which is to be discarded eventually. Isabelle system programming is now done in Isabelle/Scala, starting already 5 years ago, and working more and more smoothly as it is actually being used. So no more bash, perl, ruby, python, sed, awk scripting, just plain Scala programming with some Isabelle library operations. For example, the recently updated build_doc tool (bc61161a5bd0) is now a proper Isabelle/Scala tool, which merely happens to have a bash wrapper for historical reasons (it is still required for some administrative bash scripts). For regular use, the tool can be used directly in the Console/Scala shell of Isabelle/jEdit like this (e.g. in current f40ac83d076c): import isabelle._ Build_Doc.build_doc(Options.init, new Build.Console_Progress(true), docs = List(jedit)) This has the advantages of statically-typed programming in an interactive TTY loop, over an untyped scripting language like bash. It requires a bit of practice and giving up old customs to become fluent with it, but then it works surprisingly well. I've done that in the past few weeks routinely, when working on the Isabelle manuals. It also saves a lot of JVM process creation and warmup-time. That approach might be a bit shocking to hardcore Linux users, but for most Isabelle users it makes more and more sense. Isabelle/jEdit is an IDE, which means Integrated Development Environment, so it is not surprising that it has an integrated system programming shell. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Has anyone ever run out of memory trying to *start* to build the AFP?
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
[isabelle-dev] Has anyone ever run out of memory trying to *start* to build the AFP?
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
