Email Gateway (Aug 18 2022 at 11:54): Email Gateway (Aug 18 2022 at 11:54):From: Robert Rothenberg <robrwo@gmail.com>
Hello,
Is there a version of HOL compiled for 64-bit Linux available? If not,
where can I get the sources to compile myself? Otherwise, will the 32-bit
version of HOL work with the 64-bit version of polyml?
Rob
Email Gateway (Aug 18 2022 at 11:54):From: Makarius <makarius@sketis.net>
At the moment 64bit Isabelle/HOL is rarely needed, so we do not distribute
it precompiled. There is nothing special about compiling Isabelle logics,
the sources are just the Isabelle sources. See also
http://isabelle.in.tum.de/installation.html, especially heeding this:
... For other platforms (Solaris, BSD, Cygwin etc.), Isabelle needs to
be compiled manually, see also
http://isabelle.in.tum.de/dist/Isabelle/INSTALL
Makarius
Email Gateway (Aug 18 2022 at 11:54):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Robert,
If you have the 64-bit version of polyml already, try doing this:
% cd path-to-isabelle/Pure
% isatool make clean
% cd ../HOL
% isatool make
Provided your polyml is installed properly this should rebuild HOL. I
highly doubt a 32-bit image will work on a 64-bit machine.
Here's some additional performance advice for 64-bit multi-core machines
with some spare memory:
I recommend polyml 5.1
If you have a bit of memory (I'm assuming, as you're running on
64-bits), increasing the initial heap size of polyml will yield a bit of
improvement. From my ~/isabelle/etc/settings:
ML_PLATFORM=x86_64-linux
ML_SYSTEM=polyml-5.1
ML_OPTIONS="-H 1000"
I have found that going to 1000 is the best trade off for me. Going up
to 1500 helps a little more, but not much. Beyond that it doesn't really
seem to do much. Isabelle 32-bit default is 500.
The ML_PLATFORM and ML_SYSTEM settings tell isabelle where to store the
heaps (look in ~/isabelle/heaps).
If you have multiple cores, there's some theory loading stuff isabelle
can parallelise. In Proof General: set Isabelle->Settings->Max Threads
to however many cores you have.
Use the -M option of isabelle usedir. Here's the line from my
~/isabelle/etc/settings for four cores:
ISABELLE_USEDIR_OPTIONS="-M 4 -p 1 -v true -V outline=/proof,/ML"
This will give you funky numbers like:
Building HOL ...
Finished HOL (0:02:35 elapsed time, 0:02:58 cpu time)
(2.4GHz intel Q6600)
Welcome to the 64-bit world, and I hope there's more parallelism coming
from the Isabelle creators :)
Hope this helps some people,
Rafal Kolanski.
Robert Rothenberg wrote:
Hello,
Is there a version of HOL compiled for 64-bit Linux available? If
not, where can I get the sources to compile myself? Otherwise, will the
32-bit version of HOL work with the 64-bit version of polyml?Rob
Email Gateway (Aug 18 2022 at 11:54):From: Makarius <makarius@sketis.net>
More parallelism is definitely coming, but this is orthogonal to the 64bit
platform. In fact, Poly/ML on x86_64 is almost 2 times slower than the
x86 version, because the internal word size is uniformly 64bit.
See http://isabelle.in.tum.de/devel/stats/at-mac-poly-5.1-para.html for
some performance charts for a quad-core 32bit Mac using
ML_OPTIONS="-H 2000"
ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4"
HOL_USEDIR_OPTIONS="-p 2"
Right now, 64bit only helps if significantly more heap space than 2GB is
being used, or if you happen to need more stack space than 64MB. Otherwise
plain x86 mode is adequate even on x86_64 machines.
Makarius
Email Gateway (Aug 18 2022 at 11:54):From: Timothy Bourke <tbourke@cse.unsw.edu.au>
For the record, the multitudes (surely) of FreeBSD users might also
take advantage of that project's pre-compiled packages:
http://portsmon.firepipe.net/portoverview.py?category=math&portname=isabelle
with: pkg_add -r isabelle-2007
Or download and compile via the FreeBSD ports system:
cd /usr/ports/math/isabelle
make install clean
Tim.
Last updated: May 03 2024 at 01:09 UTC