[isabelle] build HOL - memory allocation



Isabelle HOL used to work fine on my laptop till I tried to rebuild it -
in order to add proof terms.
Now, apparently, I can't rebuild it any more - even without.
From the error message it appears there's a brand new memory problem - I'm puzzled.

/usr/local/Isabelle2005 # ./build -t HOL

                *****************************
                * Welcome to Isabelle build *
                *****************************

Please check /usr/local/Isabelle2005/etc/settings
to make sure that Isabelle's ML system settings and compilation options
are appropriate.

The current values are:

  ML_SYSTEM=polyml-4.1.4
  ML_HOME=/usr/local/Isabelle2005/../polyml/x86-linux
  ML_OPTIONS=-H 80
  ML_PLATFORM=x86-linux

  ISABELLE_USEDIR_OPTIONS=-v true -V outline=/proof,/ML
  HOL_USEDIR_OPTIONS=


Press RETURN to compilation of

  HOL
  (targets: test)


Started at Sat Mar 17 15:21:26 CET 2007 (polyml-4.1.4_x86-linux on mut38-5-82-246-191-55)
make[1]: Entering directory `/usr/local/Isabelle2005/src/Pure'
make[1]: Nothing to be done for `Pure'.
make[1]: Leaving directory `/usr/local/Isabelle2005/src/Pure'
Building HOL ...
** MMAP: Unable to map file: 0 to address 0x2807e000
** errno=12: Cannot allocate memory
** This may be due to insufficient swap space, will retry in 2 seconds ...

** MMAP: Unable to map file: 0 to address 0x2807e000
** errno=12: Cannot allocate memory
** This may be due to insufficient swap space, will retry in 4 seconds ...

** MMAP: too many unsuccessful retries - giving up
Error number 12: Cannot allocate memory
HOL FAILED
(see also /usr/local/Isabelle2005/heaps/polyml-4.1.4_x86-linux/log/HOL)

 1. True
val it = [] : Thm.thm list
val HOL_proofs = 0 : int
**** Finished file "ROOT.ML" ****

+++ User 149.481  All 150.181 secs
val it = () : unit


Cannot map to address 0x2807e000

make: *** [/usr/local/Isabelle2005/heaps/polyml-4.1.4_x86-linux/HOL] Error 1
Finished at Sat Mar 17 15:24:08 CET 2007
0:02:42 total elapsed time


I'm working on a SUSE 10 Linux machine with more than 1,000 MB of total swap memory.
I re-dowloaded and reinstalled Isabelle 2005 with precompiled HOL. I'd think
the PolyML version is right:

/usr/local/Isabelle2005 # poly
Poly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
Copyright (c) 2002-5 CUTS and contributors.
Running with heap parameters (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%)
Mapping /usr/local/polyml/x86-linux/ML_dbase
Poly/ML 4.2.0 Release

I was wondering whether anyone has an insight.

Cheers, P.







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.