Email Gateway (Aug 18 2022 at 09:35): Email Gateway (Aug 18 2022 at 09:35):From: "Peter V. Homeier" <palantir@earthlink.net>
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
Email Gateway (Aug 18 2022 at 09:35):From: Nicole Rauch <rauch@informatik.uni-kl.de>
Dear Peter,
You might consider using SML/NJ (at least temporarily). It is already
available natively for Intel Macs, see
http://www.smlnj.org/dist/working/110.59/index.html
and for me, it works well (I'm using SML/NJ 110.58 with Isabelle 2005
as well as with Isabelle 2006 preview).
Best regards,
Nicole
Email Gateway (Aug 18 2022 at 09:35):From: Martin Klebermaß <martin@klebermass.de>
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@klebermass.de
============================
Fuchsbergstr. 11
D-82223 Eichenau
Mobil: +49 (0) 176 / 70073282
============================
smime.p7s
Email Gateway (Aug 18 2022 at 09:35):From: David Matthews <David.Matthews@prolingua.co.uk>
Lawrence Paulson wrote:
Do you want to reply to this?
Begin forwarded message:
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
Email Gateway (Aug 18 2022 at 09:35):From: "Peter V. Homeier" <palantir@earthlink.net>
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@klebermass.de>, who kindly shared that he has been able to "use SMLNJ (http://www.smlnj.org) 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!
Peter
-----Original Message-----
From: David Matthews <David.Matthews@prolingua.co.uk>
...
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
Email Gateway (Aug 18 2022 at 09:37):From: Lawrence Paulson <lp15@cam.ac.uk>
Poly/ML gives better performance than SML/NJ, probably because of its
better garbage collector. However, SML/NJ is quite usable.
I'm interested to hear that you are using Isabelle rather than HOL.
Are there any interesting details you can share?
Larry
Email Gateway (Aug 18 2022 at 09:43):From: "Peter V. Homeier" <palantir@earthlink.net>
I have a great respect and admiration for the Isabelle system, and wish to learn more about it, in addition to HOL4. One area of possible application is a port of my higher order quotients project from HOL4 to Isabelle/HOL. I believe this would be a good learning experience for me, and possibly useful to others. When speaking with Christian Urban during FLoC about his nominal datatypes package, he shared that having higher order quotients available might have made his project easier.
Peter
Last updated: May 03 2024 at 04:19 UTC