Hi all, it seems indeed that JinjaThreads since recently runs out of memory even on macbroy2 with parallelism, c.f. last afp isatest log:
> Running HOL-Word-JinjaThreads ... > poly(19058,0xa00a0540) malloc: *** mmap(size=16777216) failed (error code=12) > *** error: can't allocate region > *** set a breakpoint in malloc_error_break to debug > poly(19058,0xa00a0540) malloc: *** mmap(size=2097152) failed (error code=12) > *** error: can't allocate region > *** set a breakpoint in malloc_error_break to debug > terminate called after throwing an instance of 'St9bad_alloc' > what(): std::bad_alloc > /mnt/nfsbroy/home/isabelle/Isabelle2009-2/lib/scripts/run-polyml: line 74: > 19058 Abort trap "$POLY" -q $ML_OPTIONS > HOL-Word-JinjaThreads FAILED > (see also > /home/isatest/.isabelle/heaps/Isabelle2009-2/polyml-5.3.0_x86-darwin/log/HOL-Word-JinjaThreads) > > ### TC0.ty P ?E ?e == THE T. P,?E \<turnstile>1 ?e :: T > ### Ignoring duplicate introduction (intro) > ### [| ?P ?a; !!x. ?P x ==> x = ?a |] ==> (THE x. ?P x) = ?a > ### Rule already declared as introduction (intro) > ### ?P ?x ==> EX x. ?P x > ### Trying linear arithmetic... > ### Trying linear arithmetic... > ### Trying linear arithmetic... > ### Trying linear arithmetic... > ### Ignoring duplicate rewrite rule: > ### pcs (shift ?n1 ?xt1) == op + ?n1 ` pcs ?xt1 > ### Trying linear arithmetic... > ### Trying linear arithmetic... > ### Trying linear arithmetic... > ### Trying linear arithmetic... > ### Trying linear arithmetic... > ### Trying linear arithmetic... > ### Trying linear arithmetic... > ### Trying linear arithmetic... > ### Trying linear arithmetic... > > make: *** > [/home/isatest/.isabelle/heaps/Isabelle2009-2/polyml-5.3.0_x86-darwin/log/HOL-Word-JinjaThreads.gz] > Error 134 Also another test on a considerably smaller machine without parallelism does not run through any longer: http://www4.in.tum.de/~haftmann/cgi-bin/testboard.cgi/AFP/report/9eaa8a4c3b0745dd95acafb8477968f6 I would say we have broken through our current the sonic barrier and guess that this is due to the recent extension of JinjaThreads: http://www4.in.tum.de/~haftmann/cgi-bin/testboard.cgi/AFP/rev/1f41c1842f5a So, I would suggest to set JINJATHREADS_OPTIONS='-M 1 -q 0' on macbroy2 and give it again a try. Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
