Well, it almost worked now ;).
even without -b all my memory was wasted and just as swapping started in
earnest I got an error message, i.e., I have to adapt JinjaThreads to
some previous changes.
Still, I am nowhere close to the 3-4 GB RAM usage that seem to be
possible. Maybe the reason is that I'm on x86_64?
My settings are:
ISABELLE_BUILD_OPTIONS="threads=4 parallel_proofs=2"
ML_PLATFORM="x86_64-linux"
ML_HOME="/home/griff/Repos/polyml/"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="--minheap 1000"
Side remark: since I now have to adapt at least TypeComp in JinjaThreads
I started that theory up in jEdit and noticed that the ProverSession
panel does not adapt to huge inputs (i.e., no scroll-bars are added. And
for TypeComp the list of dependencies is already quite long ;)
cheers
chris
On 08/30/2012 11:12 PM, Makarius wrote:
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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
