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

Reply via email to