Hi Shu,
Unfortunately, I don't have any Mac OSes available to me, so I can't try
anything out myself. All I can suggest at this stage is to
1. Have a look at build.log to see whether the compiling/linking of xpp
produced any warnings etc. (You'll have to search for the place that
builds xpp.)
2. Run the program through gdb (the GNU debugger) to see if that can
shed any more light on the seg fault, e.g.
gdb xpp
(gdb) start
(gdb) continue
Even better would be to find the line in the C source code on which it
seg faults, e.g.
gdb xpp
(gdb) start
(gdb) step
...
etc.
(I am assuming gdb is available on the Mac. Also, you may have a better
debugger to hand, e.g. a graphical one.)
This isn't ideal. Hopefully one of the Mac users can shed more light on
this issue!
Phil
Shu Cheng wrote:
Hi Phil,
Thanks very much for your reply.
1 Yes, pp -d <database> is work well.
2 I downloaded the latest version of ProofPower, which is ProofPower
2.9.1w2 [HOL/Z Database]
3 I am using Mac OS X version 10.6. "uname -a" reports
"Darwin Shu-Chengs-MacBook-Pro.local 10.0.0 Darwin Kernel Version
10.0.0: Fri Jul 31 22:47:34 PDT 2009; root:xnu-1456.1.25~1/RELEASE_I386
i386"
4 Yes, I built it on this machine yesterday.
5 "PPENVDEBUG=1 xpp" reports
xpp: invoked as /usr/local/pp/bin/xpp
xpp: using PPHOME=/usr/local/pp
xpp: using
PATH=/usr/local/pp/bin:/opt/local/bin:/opt/local/sbin:/usr/bin:/bin:/usr/sbin:/sbin:/usr/local/bin:/usr/texbin:/usr/X11/bin
xpp: using
XUSERFILESEARCHPATH=/Users/shucheng/app-defaults/%N:/Users/shucheng/%N:/usr/local/pp/app-defaults/%N
Segmentation fault
Thanks very much for helping
Shu
On 17 Apr 2011, at 19:15, Phil Clayton wrote:
Hi Shu,
We will need some more information about this...
1. Does "pp -d <database>" work? (Note "pp" not "xpp".)
This should give you the ProofPower session
directly in the terminal.
2. What version of ProofPower are you using?
If "pp -d <database>" worked above:
The version printed by ProofPower.
Otherwise:
The ProofPower version is contained in the
file $PPHOME/VERSION where PPHOME is such that
"which xpp"
returns $PPHOME/bin/xpp.
Also, in this case, the Poly/ML version will be useful.
What does "ldd `which pp-ml`" say for libpolyml
and what version is Poly/ML in that directory.
3. What OS (incl. version) are you using?
What does "uname -a" report?
4. Are you running xpp (or pp) on the machine that
it was built on?
If not:
What does "file `which xpp`" report?
If you can, what does "uname -a" give for the
machine that built it?
5. Does "PPENVDEBUG=1 xpp" produce any more output?
That's probably enough to start with!
Phil
Shu Cheng wrote:
Hello everyone,
I am a fresher here.
When I try to use "xpp -d database" to open an xpp session in X11, I
get an error message -- Segmentation fault. Is anyone have any idea
for this?
Thanks a lot!
Shu Cheng
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
