32-bit libraries seem required for linux?

[Jake Holland]

Hi,

I'm running 64-bit ubuntu server, and the installation instructions currently say the 32-bit libraries are "optional, for improved performance of Poly/ML", but the libraries appear actually to be required.

A web search for the error message didn't find the solution, so I thought I'd post my experience for the next person, and maybe word will get back to the maintainer of the page with the error (http://mirror.cse.unsw.edu.au/pub/isabelle/installation.html).

Here's the problem and my solution:

jholland@ubuntu:~$ tar xzf Isabelle2013_linux.tar.gz
jholland@ubuntu:~$ Isabelle2013/bin/isabelle build -s -b HOL
### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++)
### Using bulky 64bit version of Poly/ML instead
Building Pure ...
poly: heapsizing.cpp:606: bool HeapSizeParameters::getCostAndSize(POLYUNSIGNED&, double&, bool): Assertion `sizeMin >= minHeapSize && sizeMin <= maxHeapSize' failed.
/home/jholland/Isabelle2013/lib/scripts/run-polyml: line 77: 17925 Aborted (core dumped) "$POLY" -q $ML_OPTIONS
Pure FAILED
(see also /home/jholland/Isabelle2013/heaps/polyml-5.5.0_x86_64-linux/log/Pure)

val free : string -> term
val force_syntax : syntax -> unit
val eq_syntax : syntax * syntax -> bool
val empty_syntax : syntax
val const : string -> term
val check_typs : Proof.context -> typ list -> typ list
val check_typ : Proof.context -> typ -> typ
val check_terms : Proof.context -> term list -> term list
val check_term : Proof.context -> term -> term
val check_sort : Proof.context -> sort -> sort
val check_props : Proof.context -> term list -> term list
val check_prop : Proof.context -> term -> term
val basic_nonterms : string list
val ambiguity_warning_raw : Config.raw
val ambiguity_warning : bool Config.T
val ambiguity_limit_raw : Config.raw
val ambiguity_limit : int Config.T
end
structure Syntax : SYNTAX
val it = (): unit
HOL CANCELLED
Unfinished session(s): HOL, Pure
0:00:41 elapsed time, 0:00:12 cpu time, factor 0.29

jholland@ubuntu:~$
jholland@ubuntu:~$ sudo apt-get install lib32stdc++6 lib32gcc1-dbg
...

jholland@ubuntu:~$ Isabelle2013/bin/isabelle build -s -b HOL
Building Pure ...
Finished Pure (0:00:12 elapsed time, 0:00:09 cpu time, factor 0.75)
Building HOL ...
Finished HOL (0:05:07 elapsed time, 0:05:00 cpu time, factor 0.97)
0:05:31 elapsed time, 0:05:23 cpu time, factor 0.97


Thanks and cheers.

Jake