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

[Makarius]

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