Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] build HOL - memory allocation

Email Gateway (Aug 18 2022 at 10:20):

From: paolot@informatik.uni-bremen.de
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.

Last updated: May 03 2024 at 08:18 UTC