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? 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. It may help to run the disc garbage collector (poly -d) on the database first.
Regards, David.