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

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

Hi Sam,

Sorry I didn't look into your reply sooner. 

I can't tell for sure if the revised script is causing this error, but when I load pvs using it I get the emacs editor, several PVS items seems to load Ok, including Allegro and NASA's Field library, but after these PVS load-successes I get the following:

"error in process filter: Cannot open load file: Manip/emacs/pvs-prover-manip.el"

After this, none of the emacs toolbars work, and I have to kill the process to exit emacs.  However, when I use my script it works Ok even after this harsh treatment of emacs.

I hope this helps you.


Sam Owre <owre@csl.sri.com> wrote:
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?

Sam Owre

Mark Brown 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:
> 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