Re: [isabelle] HOL for x86_64 Linux?



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






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