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.