Hi, can you please help?
Thanks! -- Giamp
----- Forwarded message from Lawrence Paulson lp15@cam.ac.uk ----- Date: Fri, 2 Dec 2005 11:48:53 +0000 From: Lawrence Paulson lp15@cam.ac.uk Reply-To: Lawrence Paulson lp15@cam.ac.uk Subject: Re: installation To: giamp@dmi.unict.it
Try your question at polyml@informatics.ed.ac.uk. If they recomment Poly/ML-4.2, you need to download our Poly/ML-4.14, which is a version of that patched "backwards" to support the current Isabelle release.
There's always SML/NJ, though it's slower for big proofs.
Larry
On 2 Dec 2005, at 11:29, giamp@dmi.unict.it 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?
----- End forwarded message -----
---------------------------------------------------------------- This message was sent using IMP, the Internet Messaging Program.
giamp@dmi.unict.it wrote:
Hi, can you please help?
Thanks!
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.
David P.S. Please subscribe to the Poly/ML mailing list with the email address you use to mail to it. To avoid spam, messages from other mail addresses are held and I have to forward them to the list manually.
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)
On Monday 05 December 2005 12:59, Martin Ellis wrote:
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.
[1] http://packages.ubuntu.com/breezy/utils/linux32 (link to the source is the .orig.tar.gz at the bottom of the page)
I've just looked at the source for linux32, and it seems there's a --3gb AND a --4gb option!
I'm now less certain that it was the --4gb option, so if one doesn't work...
Martin
-
David.Matthews＠prolingua.co.uk -
giamp＠dmi.unict.it -
m.a.ellis＠ncl.ac.uk