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).