On 16/11/11 17:59, David Matthews wrote:
On 16/11/2011 17:15, Makarius wrote:
On Wed, 16 Nov 2011, Rob Arthan wrote:
On 16 Nov 2011, at 15:17, Phil Clayton wrote:
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.
Seconded: at least one user of ProofPower (me) and many users of Isabelle are already in that situation.
Yes, the big applications are already using x86_64 routinely, with 8-32 GB memory requirement. Pretty soon, x86 will be only for "small" portable devices.
OK. I've now added CInterface.null as a persistent vol (the only one) containing (void*)0. It should be possible to test for null by using fromClong x = 0.
All built and working! Many thanks. I'll be glad to ditch the vol option approach. Also, the Foreign exception is now working as expected for double arguments.
I've just started thinking about how to do callbacks for X86/64. They're more complicated than for X86/32 because some arguments are in registers but I think I can probably get round this.
The other issue for X86/64 is that CInterface doesn't currently support calling foreign functions with floating point arguments. Getting this to work would require some big changes to the code.
From my perspective, callbacks on x86_64 are more important but I accept that any design would need to consider both for the long run.
Phil