[isabelle] Using Isabelle on Intel Macintosh?



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.

I see from the above web page that a general user cannot easily port PolyML to a
new architecture, since the database needs to be specially constructed.  This is
beyond my skill at present.  Is anyone else working on this?

Apple has completed their transition away from PowerPC to Intel, already has substantial
support for creating 64-bit software at the command line, and plans to ship their
next version of OS X (Leopard) next spring with full support for 64-bit.  To simplify
matters, one can compile a program on the Macintosh to produce a "Universal"
binary, which contains versions for both PowerPC and for Intel.  I'd like to
ask that someone create a Universal binary version of PolyML.

It would be very helpful, and would be used by many people.

Thanks!

Peter





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