Re: [isabelle] Using Isabelle on Intel Macintosh?

Thank you for looking into this.  I think that many people are finding the Macintosh a congenial workspace for theorem proving, and would welcome your version of Poly/ML.  Please do announce when you have something working.

I have also heard from Martin KlebermaÃ? <martin at>, who kindly shared that he has been able to "use SMLNJ ( which is already ported to the Intel Mac."

How would you compare Poly/ML and SMLNJ with respect to supporting Isabelle?

Many thanks to both you and Martin!


-----Original Message-----
>From: David Matthews <David.Matthews at>
>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.


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