[isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

[Dmitriy Traytel]

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 <hupel at 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev