[isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory
Lars Hupel
hupel at in.tum.de
Wed Feb 17 22:22:15 CET 2016
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
More information about the isabelle-dev
mailing list