Re: [isabelle] HOL for x86_64 Linux?
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:
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,
Robert Rothenberg wrote:
> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and