On 16/11/2011 15:17, Phil Clayton wrote:
On 16/11/11 11:17, David Matthews wrote:
On 16/11/2011 04:15, Ian Zimmerman wrote:
Phil> David, My situation is slightly unusual so perhaps it's Phil> useful/interesting to explain some background. I'm working on Phil> support for GLib/GTK in SML which involves a significant number of Phil> calls to C functions.
Last I knew, this was impossible in Poly/ML due to no callbacks from C. Has something crucial changed?
The CInterface structure has had callbacks for a long time. They're only implemented on X86 but that covers the vast majority of users. There's an example in mlsource/extra/CInterface/Examples/ForeignTest.sml.
To clarify, callbacks are available on i386 but not x86_64.
I suspect those involved with large scale theorem proving will start moving to 64 bit OSes, if not already, so one application can address more than 4GB memory, as that amount of physical memory is becoming quite common these days.
Yes, you're correct. I'd forgotten that. I seem to recall that there was a problem with floating point on X86/64 but it may be possible to provide call-backs for functions that don't use them.
David