Re: [isabelle] Fwd: Using Isabelle on Intel Macintosh?



Lawrence Paulson wrote:
> Do you want to reply to this?

> Begin forwarded message:
I am planning on buying a new Macintosh soon with an 64-bit  architecture Intel Core
2 Duo microprocessor (Merom).  I believe that Isabelle/HOL will run  on this machine,
with the PowerPC instruction set interpreted by Apple's "Rosetta"
software.  However, since this is slower than running native code,  I would greatly
prefer to use a port of Isabelle to the native instruction set.   This of course
depends on a port of PolyML.  There is already an Intel version of  PolyML for Linux,
FreeBSD, etc. listed at http://www.polyml.org/download.html, but  this does not appear
to exactly fit what we need.

There is a project under way to port Poly/ML to the AMD64 architecture which as far as I can tell is the same as the Intel 64. I'm hoping to have this working in a few months' time. The present i386 version of Poly/ML won't run on Mac OS X due to the way the Mach kernel handles certain kinds of traps. The changes for the AMD64 should include a work around for that as well. For the moment, therefore, your only option is to use the Power PC version.

Once the new version is working I'll think about the best way to distribute Poly/ML for the Mac and it may be worth thinking of producing a universal binary.

Regards,
David





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