[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] PVS proof-trees
Do you have a *tcl-pvs* buffer? If so, does it look normal (a few '%'
prompts is normal). If not, could you run
M-x eval-expression <RET>(pvs-wish)<RET>
and see if that generates an error or produces a *tcl-pvs* buffer?
Sebastian Verschoor <firstname.lastname@example.org> wrote:
> Hi Sam,
> Thanks for the fast reply. I have followed your instructions, but no solution
> typing wish in the shell gives me a small window
> (C-h v pvs-wish-cmd <RET>)
> pvs-wish-cmd is a variable defined in `pvs-tcl.el'.
> Its value is "wish"
> And also the links appear to be in order:
> pvs-5.0-ix86-Linux-allegro$ which wish
> pvs-5.0-ix86-Linux-allegro$ ll /usr/bin | grep wish
> lrwxrwxrwx 1 root root 22 2010-07-28 02:12 wish -> /etc/
> -rwxr-xr-x 1 root root 5500 2009-11-06 13:02 wish8.4*
> -rwxr-xr-x 1 root root 5500 2009-12-01 01:15 wish8.5*
> pvs-5.0-ix86-Linux-allegro$ ll /etc/alternatives | grep wish
> lrwxrwxrwx 1 root root 16 2010-07-28 02:11 wish -> /usr/bin/wish8.4*
> lrwxrwxrwx 1 root root 32 2010-07-28 02:11 wish.1 -> /usr/share/man/man1/
> Any other ideas on what could be the issue?
> Sebastian Verschoor
> StudentNr: s1910396
> LinkedIn: http://www.linkedin.com/in/sebastianverschoor
> PGP key fingerprint: 268B E86C 4E2C 2C5A 086E 408C 8FEE 241D 5BC9 740D
> On 1 March 2012 03:44, Sam Owre <email@example.com> wrote:
> 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 <firstname.lastname@example.org> wrote:
> > Dear PVS helpdesk,
> > I am learning to use the PVS system, for a University project by Wim
> > (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),
> > shows me the *pvs* buffer with the proof, but no display with the
> > I have installed the PVS 5.0 binary from the website (http://
> > cgi-bin/downloadlic.cgi?file=pvs-5.0-ix86-Linux-allegro.tgz), which I
> > 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
> > 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