[isabelle-dev] Library/List_Prefix

[Makarius]

On Thu, 30 Aug 2012, Christian Sternagel wrote:

> I could however not test JinjaThreads, since even with poly 5.5.0, 4 cores 
> and 8GB RAM my computer flat-lined a few minutes after 'isabelle build -d . 
> -b JinjaThreads' with ISABELLE_BUILD_OPTIONS="threads=4 parallel_proofs=2". 
> It would be much appreciated if somebody with access to a more powerful 
> computer could adapt JinjaThreads.

It should work comfortably like this:

    ISABELLE_BUILD_OPTIONS="threads=4 parallel_proofs=2"

    ML_PLATFORM="x86-linux"
    ML_HOME="/home/polyml/polyml-svn/x86-linux"
    ML_SYSTEM="polyml-5.5.0"
    ML_OPTIONS="-H 1000"

Resulting in a runtime of JinjaThreads in the range of 20..40min.  You 
don't need to build an image for it (-b).


 	Makarius