Hi,
i have bought a new MacBook and i would look forward for PolyML on Intel based Macs.
As i heard from Prof. Nipkow there are some problems with signaling or so on the intel based macs, so that it doesnt compile. So i have started to look a little bit on the source to about the problems and as much as i can see there are the following problems:
1. no global functions for changing the Floating Point Rounding mode needed for reals.c (im not sure if this is realy needed at the moment. 2. adding support for darwin i386 in mm.h (MM_CPU_TYPE) 3. sighandler.c SV_SAVE_REGS seems to be a ppc specific handler.
At the moment im looking about solving number 1, but before i start with this, i look forward if anyone has already done more research.
Thanks Martin Klebermass
working about these problems all the night i think i have solved some of them
- no global functions for changing the Floating Point Rounding mode
I have looked arround about implelementations of changing Floating Point Rounding Mode. You need to embed some asm code (fnstcw and other instructions to set the Rounding mode for the FPU). I have testet it yet whith some code from another open source software, but i have to check if there a license problems between both of these two etc.
- adding support for darwin i386 in mm.h (MM_CPU_TYPE)
I have changed this the way so the handler will use the interpretet database.
- sighandler.c SV_SAVE_REGS seems to be a ppc specific handler.
As it isnt used for the other platforms using x86 cpus i have dropped this at the moment, there have to be done more research if this is correkt.
To sum up everything. I got poly running on my Intelmac with the interpreted database. i compiled the interpreted database as described. Afterwords i started to integrate my poly installation into the isabelle installation.
FOL and HOL did build completly with this poly installation. But the test didnt work because of using to much memory (could this be because of the interpreted version?).
Starting xemacs with ProofGeneral did work, but when i start the proof emacs seems to hang (there is a poly programm running but nothing is going on).
Isar in the Interactive mode does not start too (error with no Isar object found).
So before continuing with integrating poly into the isabelle installation and searching for the problems there i would like to test poly in a standalone test to check if it is working. Is there any testsuite to test poly or other posibilities without getting to much side effects by other tools (like isabelle).
Martin Kleberma? wrote:
i have bought a new MacBook and i would look forward for PolyML on Intel based Macs.
As i heard from Prof. Nipkow there are some problems with signaling or so on the intel based macs, so that it doesnt compile.
Back in March Tobias had an Intel Mac on loan for a short while and I tried to get Poly/ML running on it. There were a few minor problems and one major one. The minor problems were to do with a few operating system dependencies and also that OS X on the i386 seemed to require the stack pointer to be aligned on a 16-byte boundary, requiring a tweaks to the IO_CALL macros in the assembly code segment.
The major problem had to do with the way Poly/ML checks for heap overflow on the i386 (and also stack overflow, but that's less of an issue). Whenever an object (e.g. a tuple or list cell) is created on the heap the heap pointer is adjusted and a check needs to be made that the heap isn't full. The i386 code generator uses the i386 BOUND instruction for this. This instruction was presumably introduced to check a value against array bounds before indexing into an array. It checks a register contents against two limits and generates a trap if it is outside the range. On all the other Unix systems, Linux, FreeBSD etc this results in a signal, either SIGSEGV or SIGFPE, and on Windows it results in an exception. These can be caught and handled and so Poly/ML uses this as a way of indicating that there is a need to garbage collect. When I tested this on Mac OS X it didn't seem to work. The Mach kernel appeared to get the trap but didn't pass this on as a signal and the application would just hang. This is really a bug in Mac OS X but I think the only option is to change the code-generator to replace the BOUND instruction with a test, branch and explicit call into the run-time system.
I expect to be working on the run-time system and the code-generator over the summer as part of a project to get Poly/ML on the AMD 64-bit machine. The Intel Mac isn't explicitly part of this but I may have a chance to look into it. In the meantime you can either make the changes yourself or use the portable interpreted version. That version will also need a few operating system dependent changes but those are quite minor.
David.
Hello David,
i have created a patch file for my modifications to get polyml on intel macs running.
To be sure it works: How can do a testrun with poly to test at least some basic functions for working correctly (As written in the other mail i have compiled the Isabelle Libs but i dont know if this is done with poly and so enough information to know poly is working).
For the reals.c Implementation i have used some code from MLtons Implementation of the IEEEEreals.
http://mlton.org/cgi-bin/viewsvn.cgi/mlton/trunk/runtime/basis/ IEEEReal.c?rev=1959&view=markup Im not sure if copying is allowed and if so what comments have to be inserted there.
Thanks for helping me.
Martin
Martin,
i have created a patch file for my modifications to get polyml on intel macs running.
Thanks. It sounds like you've managed to achieve quite a lot. I'll take a look at what you've done.
For the reals.c Implementation i have used some code from MLtons Implementation of the IEEEEreals.
I think Mac OS X now supports the fpsetround/fpgetround calls in /usr/include/fenv.h . That's probably the right way to do this.
Regards, David.
For the reals.c Implementation i have used some code from MLtons Implementation of the IEEEEreals.
I think Mac OS X now supports the fpsetround/fpgetround calls in /usr/include/fenv.h .
It does. MLton only uses the code Martin referenced on platforms that do not yet support fp{g,s}etround, namely, Cygwin, NetBSD, and OpenBSD.
BTW, MLton is released under a BSD-style license, so you can include code in other projects, provided you keep the copyright notice and don't use NEC's name for publicity without permission. See
-
David.Matthews＠prolingua.co.uk -
martin＠klebermass.de -
sweeks＠sweeks.com