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:
{ cat /home/artur/proofpower/polyml/x86-linux/ML_dbase >
slrpdb."polydb" ||
exit 1; }; echo "val product_version : string = " 2.7.6"; val
copyright :
string = "Copyright (c) Lemma 1 Ltd. 2002"; use"dtd108.sml";
use"
imp108.sml"; PolyML.commit();" | poly slrpdb."polydb"??| tee
dtd108.ldd >
imp108.ldd catchSEGV; &context = 0x807c224, in_run_time_system=1,
context.trapno=14
... on standard output:
root@firebird:/home/artur/proofpower/OpenProofPower-2.7.6# cat src/imp108.ldd Poly/ML RTS version I386-4.1.3 (19:13:05 Jun 19 2006) Copyright (c) 2002 CUTS and contributors.
Running with heap parameters
(h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%)
Mapping ./slrpdb.polydb Poly/ML 4.1.3 Release
My suggestion:
What happens if you try to run poly interactively, e.g., using the following command line:
poly /home/artur/proofpower/polyml/x86-linux/ML_dbase
The results:
When I try to run poly, I got things like that: root@firebird:/home/artur# poly /home/artur/proofpower/polyml/x86-linux/ML_dbase Poly/ML RTS version I386-4.1.3 (19:13:05 Jun 19 2006) Copyright (c) 2002 CUTS and contributors. Running with heap parameters (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%) segmentation fault I think we've nailed down that it's a Poly/ML problem - poly is reporting a segmentation fault whenever he runs it, with a bit more detail in the error report when he runs it via the ProofPower build scripts.
What should we try next?
Regards,
Rob.
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?
Regards,
Rob.
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.
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.
-
David.Matthews＠prolingua.co.uk -
rda＠lemma-one.com