Re: [isabelle] Using Isabelle on Intel Macintosh?



Hi Peter,


im using Isabelle on a Macbook. You can not use Polyml because it doesnt work on the Intel Macs at the moment. But you can use SMLNJ (http://www.smlnj.org) which is already ported to the Intel Mac.

If you have any problems with installing Isabelle on your intel mac just send me an email.



Es grüßt Sie freundlich/best regards,
	Martin Klebermaß

============================
martin at klebermass.de
============================

Fuchsbergstr. 11
D-82223 Eichenau
Mobil: +49 (0) 176 / 70073282
============================





Am 30.08.2006 um 17:19 schrieb Peter V. Homeier:

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


Attachment: smime.p7s
Description: S/MIME cryptographic signature



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