On Thursday 22 Jun 2006 3:49 pm, David Matthews wrote:
Rob Arthan wrote:
On Wednesday 21 Jun 2006 8:53 pm, Rob Arthan wrote:
The annotated and edited correspondence below gives highlights of a problem Artur Gomes is having building ProofPower.
What Artur was seeing in the log fiiles from the ProofPower build script ...
... on standard error:
catchSEGV; &context = 0x807c224, in_run_time_system=1,
Phil Clayton tells me that this is very likely the problem with newer Linux kernels reported originally by Martin Ellis (see correspondence on this list beginning 23rd November 2004). But I am not sure what Artur should do - the problem was fixed in a development version of Poly/ML 4.1.3, but the sources for that are no longer available. Will it work if he upgrades the driver program to 4.2 and uses the 4.1.3 database?
My first question was going to be why were you using 4.1.3?
Because we don't know yet whether the performance problem I encountered with 4.2.0 will be significant for the very large ProofPower applications that QinetiQ have. We will be looking into that, but we don't know enough yet.
Unfortunately, the slight changes to the basis library mean that a couple of the ProofPower source files have to be changed for 4.2.0.
Certainly this looks like the mmap address problem and I would definitely suggest upgrading if you can. You may find you can run the 4.1.3 database with the 4.2 run-time but I can't be sure. ...
I tried it and it doesn't fall over immediately. But it's a messy solution, particularly if we aren't sure it will work. I shall put together a patch for ProofPower to let you build the current version of ProofPower with Poly/ML 4.2.0 (Arturo: I will mail you when I have done this).
Regards,
Rob.