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

Re: [PVS] PVS on NOT (Linux OR Solaris)



I've been looking into this, and finally discovered that the
difference is that in freebsd, exporting an environment
variable also sets its value to "", whereas in linux the
variable is left unset.  The calls to getenv then return
different values ("" and nil, respectively), and various
tests fail.  I'm modifying the emacs code to call pvs-getenv,
which returns nil in either case.

Could you please send whatever changes you made to get this
to work?  I'd like to make sure that I haven't missed
anything.

Thanks,
Sam

> From:    a.degroot@science.ru.nl
> Subject: [PVS] PVS on NOT (Linux OR Solaris)
> Date:    Fri, 12 Nov 2004 10:45:31 +0100 (MET)
> To:      pvs@csl.sri.com
> 
> As a longtime non-user of Linux or Solaris, running PVS on some other OS
> is useful for me -- it means I don't need to keep an extra machine around
> for PVS purposes. More concretely, I can do everything in FreeBSD.
> 
> PVS 2.4 runs fine on FreeBSD with Linux compatibility turned on, as long
> as you hack the pvs script to believe that FreeBSD is Redhat 5.
> 
> PVS 3.2 does not run, at least not easily. I have
> 	* hacked the pvs script
> 	* added Linux /proc support for the allegro runtime
> after that, both emacs and xemacs sit there forever, with 100% CPU usage.
> Killing them yields a LISP backtrace like the following:
> 
>   # (unwind-protect ...)
>   accept-process-output()
>   # bind (result save process dispatch handler and-go status message
> string)
>   ilisp-send("(pvs::lisp (pvs::pvs-errors (progn (setq *pvs-path*
> \"/usr/local/pvs-3.2\")\n                     (setq *pvs-emacs-interface*
> t)\n     (pvs-init nil nil)\n                     (setq *noninteractive*
> nil)\n                (setq *noninteractive-timeout* )\n
> (setq *pvs-verbose* 0)\n                     (setq *force-dp* nil)\n(when
> '\n                       (set-decision-procedure ')))))" nil nil nil)
>   # bind (cursor-in-echo-area *pvs-output-pos* and-go status message
> string)
>   pvs-send*("(progn (setq *pvs-path* \"/usr/local/pvs-3.2\")\n   (setq
> *pvs-emacs-interface* t)\n                     (pvs-init nil nil)\n
> (setq *noninteractive* nil)\n                     (setq
> *noninteractive-timeout* )\n                     (setq *pvs-verbose* 0)\n
> (setq *force-dp* nil)\n                     (when '\n
> (set-decision-procedure ')))" nil nil)
> 
> 
> 
> Note that I can run bin/ix86-redhat5/runtime/pvs-allegro6.2 fine, and
> enter LISP expressions at the prompt there, so the problem appears to be
> in the interface between emacs and PVS. Unfortunately (?) I'm not so well
> acquainted with the catacombs and horrors of emacs. Does anyone have an
> idea of how to proceed with debugging this?
> 
> 
> [ade]