c-sterna at jaist.ac.jp
Fri Aug 31 05:25:32 CEST 2012
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:
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 ;)
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_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).
More information about the isabelle-dev