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 

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 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
>  ...
>  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 mailing list
> _______________________________________________
> Proofpower mailing list

Proofpower mailing list

Reply via email to