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

Re: [PVS-Help] Problem installing in RED HAT 9

On Mon, May 10, 2004 at 02:00:19AM -0400, Nikhil Varma wrote:
> Hello,
> I tried to install PVS 3.1 in red hat 9 and after doing /bin/relocate and
> then trying to execute pvs I get the following messages in the emacs
> window that pops up.
> ************************************************************************
> Starting pvs-allegro6.2 -qq ...
> dlopen(/home/nikhil/pvs/bin/ix86-redhat5/runtime/libacl623.so, mode)
> error: /home/nikhil/pvs/bin/ix86-redhat5/runtime/libacl623.so: symbol
> errno, version GLIBC_2.0 not defined in file libc.so.6 with link time
> reference
> ************************************************************************
> Debugger entered--Lisp error: (error "Could not run PVS")
>   signal(error ("Could not run PVS"))
>   error("Could not run PVS")
>   pvs()
>   load("pvs-load" nil nil nil)
>   eval-buffer(#<buffer  *load*> nil "/home/nikhil/pvs/emacs/go-pvs.el" nil
> t)
>   load-with-code-conversion("/home/nikhil/pvs/emacs/go-pvs.el"
> "/home/nikhil/pvs/emacs/go-pvs.el" nil t)
>   load("/home/nikhil/pvs/emacs/go-pvs.el" nil t)
>   command-line-1(("-load" "/home/nikhil/pvs/emacs/go-pvs.el"))
>   command-line()
>   normal-top-level()
> *******************************************************************
> Please suggest a way out of this problem.

See http://pvs.csl.sri.com/faq.shtml, first question.

This particular problem stems from the new threading implementation RedHat
9 and later is using, which has become standard in 2.6 kernels.
A quick workaround is to start PVS with the script found on
the above web-page, or to execute the following in your shell (remove the
$ which designates the command line prompt):

$ LD_ASSUME_KERNEL=2.4.19	# Do not use the new posix thread
$ export LD_ASSUME_KERNEL	# implementation
$ pvs



P.S.:  I expect that this will become a problem with all newer distributions
which will use the 2.6 kernel and later versions of the standard C library.
Using this work-around also allows me to use ICS as a decision procedure on
RedHat Linux 9.
Marcel Kyas
Institute for Computer-Science and Applied Mathematics
Christian-Albrechts-Universitšt Kiel

Homepage: http://www.informatik.uni-kiel.de/~mky