Hi Rob,

Thanks for your help.

I have tried your suggestion, but it still doesn't work.

a) After execute xpp - b, I also get a seg fault.

b) I tried gdb pp, but gdb report that pp is not a an executable file (File format not recognized). But I suppose you mean xpp here, I tried gdb xpp. Then gdb works. With "run -b", I got a report from gdb "
Program received signal EXC_BAD_ACCESS, Could not access memory.
Reason: KERN_INVALID_ADDRESS at address: 0x0000000000000000
0x00000001008369f5 in _XReply()"

it not the same as you mentioned.

c) I build OpenMotif 2.3.3 from source. I applied the referred patch, but it seems it doesn't work :(

Best Wishes!

On 17 Apr 2011, at 21:41, Rob Arthan wrote:

Shu (with an aside to Phil, below),

Your answer's to Phil's questions make me suspect that this is a problem specific to OpenMotif on Mac OS X. Here are a few more things to try:

a) To eliminate one small possibility can you check whether xpp still fails with a segmentation fault if you run it with this command:

xpp -b

(The -b option makes it run "in the foreground" which simplifies the way it starts up and makes it easier to debug.)

b) Try running it under the gnu debugger, gdb. To do this run the command:

gdb /usr/local/pp/bin/pp

... This should give you a prompt "(gdb)". Type:

run -b

... This will try to run xpp. I am expecting that you will get a report from gdb including something like "Program received signal SIGSEGV, Segmentation fault." followed by the "(gdb)" prompt again. If so, type


... and let us know what it says.

"quit" at the "(gdb)" prompt will get you out of gdb. Use Control+C to get to the prompt if necessary.

[Aside to Phil: when xpp runs in the background, gdb won't follow xpp through the fork unless you do clever things that have never worked for me: it will just say that the process exited normally. As it is fairly rare that running in the background makes any difference, I usually try debugging with "-b" first. You don't need to single step with gdb if the failure you are expecting is a signal like a segmentation fault, gdb will trap the signal and prompt for commands.]

c) This is assuming (b) is going to show a failure in a motif call: did you build OpenMotif from source? If so, there is a patch available at http://bugs.motifzone.net/show_bug.cgi?id=1497 that you will need to apply. If you used port or fink to install OpenMotif, which version did you download? If you installed LessTif, then I strongly recommend you install OpenMotif instead.



On 17 Apr 2011, at 20:53, Phil Clayton wrote:

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

(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!


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
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.
  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!


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 mailing list

Proofpower mailing list

Proofpower mailing list

Reply via email to