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

Re: [PVS-Help] PVS proof-trees

Hi Sebastian,

Is 'wish' in your path?  You should be able to type wish at a shell
prompt and have a small window pop up.  If that works, check the value of
pvs-wish-cmd (C-h v pvs-wish-cmd <RET>), which should be set to "wish".

For my Linux setup, wish is in /usr/bin, but it is a link to
/etc/alternatives/wish, which in turn links to /usr/bin/wish-default, and
finally to /usr/bin/wish8.4.  This is part of the update-alternatives
mechanism (see man page for more information).  If any of these links was
broken, then wish would fail to work.  If you have /usrr/bin/wish8.x, you
can simple set pvs-wish-cmd in ~/.pvsemacs:

(setq pvs-wish-cmd "/usr/bin/wish8.x")

Though it's probably better to fix the links.

Let me know if that's not the problem, and we'll dig deeper.

Sebastian Verschoor <s.r.verschoor@student.rug.nl> wrote:

> Dear PVS helpdesk,
> I am learning to use the PVS system, for a University project by Wim Hesselink
> (he said maybe you'd know him :) ). However, I'm having some trouble in
> displaying the proof-trees: when I run the C-c C-p x command (x-prove), emacs
> shows me the *pvs* buffer with the proof, but no display with the proof-tree.
> I have installed the PVS 5.0 binary from the website (http://pvs.csl.sri.com/
> cgi-bin/downloadlic.cgi?file=pvs-5.0-ix86-Linux-allegro.tgz), which I extracted
> to a folder, then I ran the bin/relocate command.
> Some information on the system I am running:
> Ubuntu 10.04 (lucid)
> GNOME 2.30.2 (Ubuntu 2010-06-25)
> Kernel 2.6.32-38-generic (#83-Ubuntu SMP Wed Jan 4 11:13:04 UTC 2012)
> GNU Emacs 23.1.1
> sebastian@sebastian-laptop:~/.school/afstudeerproject/ar/
> pvs-5.0-ix86-Linux-allegro$ wish
> % info tclversion
> 8.4
> % set tk_version
> 8.4
> The PVS system is in /home/sebastian/.school/afstudeerproject/ar/
> pvs-5.0-ix86-Linux-allegro
> PVS Version 5.0 - Allegro CL Enterprise Edition 8.2 [Linux (x86)] (Apr 14, 2011
> 1:43) - Allegro CL Enterprise Edition 8.2 [Linux (x86)] (Apr 14, 2011 1:43)
> Could you maybe help me getting the proof-tree display to work?
> Thanks in advance,
> Sebastian
> --
> Sebastian Verschoor
> StudentNr: s1910396
> LinkedIn: http://www.linkedin.com/in/sebastianverschoor
> PGP key fingerprint: 268B E86C 4E2C 2C5A 086E  408C 8FEE 241D 5BC9 740D