Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] build HOL and SUSE 10.2

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

From: paolot@informatik.uni-bremen.de
Just for record - in case anyone find the same. Compilation of
Isabelle2005 HOL may fail with openSUSE 10.2.
Apparently, the problem lays with the new kernel. In contrast, SUSE
10.0 with the original kernel gives no problem.
My machine is a Thinkpad R52.

linux-m02e:/usr/local/Isabelle # ./build 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=-p 2 -v true -V outline=/proof,/ML
HOL_USEDIR_OPTIONS=

Press RETURN to compilation of

HOL

Started at Tue Apr 3 00:42:57 CEST 2007 (polyml-4.1.4_x86-linux on
linux-m02e)
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 0xa55c0000
** 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 0xa55c0000
** 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
Run out of store - interrupting console processes
HOL FAILED
(see also /usr/local/Isabelle2005/heaps/polyml-4.1.4_x86-linux/log/HOL)

Search depth = 1

Search depth = 2

Search depth = 3

Search depth = 4

Search depth = 5

Search depth = 6

*** Interrupt.
*** At command "by" (line 102 of
"/usr/local/Isabelle2005/src/HOL/Wellfounded_Relations.thy").
Exception- ERROR raised
ERROR.

make: *** [/usr/local/Isabelle2005/heaps/polyml-4.1.4_x86-linux/HOL] Error 1
Finished at Tue Apr 3 00:45:36 CEST 2007
0:02:39 total elapsed time
linux-m02e:/usr/local/Isabelle #

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

From: Stefan Berghofer <berghofe@in.tum.de>
paolot@informatik.uni-bremen.de wrote:
The latest PolyML 5.0 version, which you can download from

http://sourceforge.net/project/showfiles.php?group_id=148318

should also work with SUSE 10.2. In order to get it to work with Isabelle2005,
you have to install a patch available at

http://www4.in.tum.de/~wenzelm/test/Isabelle2005-polyml-5.0.tar.gz

See also Markus Wenzel's message on this mailing list from January 9th, 2007.

Greetings,
Stefan

Last updated: Nov 21 2024 at 12:39 UTC