On Monday 05 December 2005 12:14, David Matthews wrote:
I'm trying to install Isabelle on an AMD Athlon 64, which is a 64 bit x86 architecture.
Polyml gives a known segmentation fault, but installing its fix produces:
Poly/ML is not available for this architecture - x86_64
Ever heard about this? Do I just need to change machine
Poly/ML does not currently have support for 64-bit mode on the AMD 64 but I believe that this machine will run 32-bit programs. You need to edit the driver/configure script so that it will compile this in the same way as for the other iX86 machines. Changing the line that reads i?86) echo "Building for Intel architecture" into i?86 | x86_64) echo "Building for Intel architecture" ought to allow it to compile. I don't know how the virtual address space is organised so it's possible that there may be problems once you've compiled it. Let me know if this works and I will make the change in CVS.
I found a way to use PolyML with Isabelle without recompiling PolyML, i.e. using the pre-build Isabelle PolyML.
I can't check exactly how I did it, since that machine is currently dead. But I recall it was quite simple to do.
Here's what I remember - there's a package called linux32 [1] which I installed. Then modify the Isabelle/lib/scripts/run-polyml file as follows:
Replace every invocation of $POLY with linux32 --4gb $POLY
So for example, the first one is echo "PolyML.make_database "$(fixpath "$OUTFILE")"; PolyML.quit();" | "$POLY" -r "$(fixpath "$INFILE")"
and becomes echo "PolyML.make_database "$(fixpath "$OUTFILE")"; PolyML.quit();" | linux32 --4gb "$POLY" -r "$(fixpath "$INFILE")" I count two more occurences after that. You'll need to run linux32 --help to check that the argument really is --4gb, and that I've recalled this correctly. You really need that 4GB option, though, whatever it is.
Cheers, Martin
[1] http://packages.ubuntu.com/breezy/utils/linux32 (link to the source is the .orig.tar.gz at the bottom of the page)