[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] PVS 3.2 on Fedora Core 5



Hi Mark,

Thanks for your posting.  Someone complained earlier of this - I didn't
have immediate access to a FC5 machine.  I now have a patch - it's a bit
of a hack (of course, so is LD_ASSUME_KERNEL). and I updated the FAQ.
Could you try the script at http://pvs.csl.sri.com/pvs and let me know
if it works for you?

Thanks,
Sam Owre

Mark Brown <rpmdb@yahoo.com> wrote:

> Hello,
> 
> I had a little trouble installing PVS 3.2 on Fedora Core 5 today.  Here's where I started:
> 
> -Download and install 5 CD ISO images containing Fedora Core 5 (FC5)
> -Tweak with network card and display settings on FC5
> -Update all software using "yum -y update" at command line in FC5
> -Install emacs using "yum install emacs"
> -Install PVS 3.2 from the linux zip and the system zip
> -Relocate PVS using bin/relocate
> 
> My problem was that when I ran the pvs shell script to start up PVS, I received some errors stating that low-level glibc shared objects could not be used / found.  Errors included:
> 
> uname: errror while loading shared libraries: libc.so.6: cannot open shared object file: No such file or directory
> 
> and:
> 
> /bin/sh: error while loading shared libraries: libdl.so.2: cannot open shared object file: No such file or directory
> 
> After some script debugging, I found that these errors occurred after the pvs shell script had exported the shell variable LD_ASSUME_KERNEL.  Google helped me to understand what that meant, see 
> 
> http://people.redhat.com/drepper/assumekernel.html (technical overview) and
> http://dag.wieers.com/howto/compatibility/ (simpler How-to advice)
> 
> Next I experimented with modifications the pvs script.  I chose to run the emacs editor (using the installed PVS extensions) using the "one time" method described by Dag Wieers's compatibility webpage as follows:
> 
> PVSEMACS="LD_ASSUME_KERNEL=${LD_ASSUME_KERNEL} ${PVSEMACS}"
> 
> I inserted this line at a carefully chosen place within the pvs script.  Please note that the location of this line within the pvs script MUST be chosen carefully.  I chose to put it directly after these lines:
> 
> case $PVSEMCAS in
>   *[xl]emacs*) \
> 
> I think this solved my problem.  This fix enabled me to launch pvs within the emacs editor using the (modified) pvs script, and parse, typecheck and prove the example from chapter 2 of the PVS system guide -- hopefully that means it works Ok.
> 
> Best regards,
> 
> Mark Brown
> RedPhone Security