Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 723

Synopsis:        installing 3.0
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Mon Dec 23 18:20:00 2002
Originator:      John Doner
Organization:    math.ucsb.edu
Release:         PVS 3.0

  I downloaded and installed the 3.0 beta, following the
  instructions.  There seem to be some library files missing.
  Is this because our system is not up-to-date, perhaps?
  The details:
  I get this error in the main emacs window:
     Starting pvs-allegro6.2 -qq ...
     ld.so.1: /net/sparc/PVS/bin/sun4-SunOS5/runtime/pvs-allegro6.2: fatal: lib
 rt.so.1: open failed: No such file or directory
  with the *Backtrace* containing
     Signaling: (error "Could not run PVS")
       signal(error ("Could not run PVS"))
       error("Could not run PVS")
       load("pvs-load" nil nil nil)
       eval-buffer(#<buffer  *load*> nil "/net/sparc/PVS/emacs/go-pvs.el")
       load-with-code-conversion("/net/sparc/PVS/emacs/go-pvs.el" "/net/sparc/P
 VS/emacs/go-pvs.el" nil t)
       load("/net/sparc/PVS/emacs/go-pvs.el" nil t)
       command-line-1(("-load" "/net/sparc/PVS/emacs/go-pvs.el"))
  My emacs version is 20.4.1
  uname -a produces
     SunOS gauss 5.6 Generic_105181-23 sun4u sparc SUNW,Ultra-5_10
  I tried getting a copy of the missing file librt.so.1
  (actually, a link to something else, which I also copied) and
  putting it in the LD_LIBRARY_PATH, but only got a similar
  error for some other missing file.
  By the way, 3.0 installs and runs just fine on my home machine
  with RedHat Linux 7.2
  John E. Doner, UCSB Math. Dept., doner@math.ucsb.edu


Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools