Hi Lars, yes, I also saw this on testboard and was confused.
On my (low-end 2 core) machine (isabelle/e4e09a6e3922, afp/123d7cbae549): ~/repos/nonprim-corec/paper$ isabelle build -vd '$AFP' Formula_Derivatives ISABELLE_BUILD_OPTIONS="threads=4 parallel_proofs=2" ISABELLE_BUILD_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx2560m -Xss4m" ML_PLATFORM="x86-darwin" ML_HOME="/Users/traytel/.isabelle/contrib/polyml-5.6-1/x86-darwin" ML_SYSTEM="polyml-5.6" ML_OPTIONS="-H 500” [...] Running Formula_Derivatives … [...] Timing Formula_Derivatives (4 threads, 269.115s elapsed time, 708.123s cpu time, 222.858s GC time, factor 2.63) Finished Formula_Derivatives (0:04:34 elapsed time, 0:11:53 cpu time, factor 2.60) Dmitriy > On 17 Feb 2016, at 22:22, Lars Hupel <hu...@in.tum.de> wrote: > > Despite increasing the ML heap size with "-H 2000", the session > "Formula_Derivatives" is failing. The build VMs have 32 GB of RAM, so > that shouldn't be a problem. Here are the relevant environment variables: > > ML_PLATFORM="x86-linux" > ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86-linux" > ML_SYSTEM="polyml-5.6" > ML_OPTIONS="-H 2000" > > What strikes me as odd is that it's always the same session. > > > > Formula_Derivatives FAILED > (see also > /media/data/jenkins/.isabelle/heaps/polyml-5.6_x86-linux/log/Formula_Derivatives) > > sig > val check_eqv: > WS1S.idx -> > WS1S.nat -> > ((WS1S.nat, WS1S.nat) WS1S.atomic, WS1S.orderb) WS1S.aformula -> > (Presb.presb, unit) WS1S.aformula -> bool > type 'a set > end > ### theory "WS1S_Presburger_Equivalence" > ### 11.322s elapsed time, 30.652s cpu time, 4.624s GC time > ### Ignoring duplicate rewrite rule: > ### find0 SO ?vr (Eq_Const ?v ?va ?vb) \<equiv> False > ### Ignoring duplicate rewrite rule: > ### find0 SO ?vr (Less ?v ?va ?vb) \<equiv> False > ### Ignoring duplicate rewrite rule: > ### find0 SO ?vr (Plus_FO ?v ?va ?vb ?vc) \<equiv> False > ### Ignoring duplicate rewrite rule: > ### find0 SO ?vr (Eq_FO ?v ?va ?vb) \<equiv> False > val it = (): unit > ML> Exception- SysErr ("Cannot allocate memory", SOME ENOMEM) raised > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev