[isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

[Lars Hupel]

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