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

Re: [PVS-Help] PVS proof-trees



OK, in the *tcl-pvs* buffer, what happens if you type

show-proof-commands {"foo" "bar"}

Sam

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

> Hi Sam,
> 
> After I ran the x-prove command I do have a *tcl-pvs* buffer: just one line of
> % characters.
> 
> The M-x eval-expression <RET>(pvs-wish)<RET> works as well...
> 
> Greetings,
> 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
> 
> 
> On 1 March 2012 21:59, Sam Owre <owre@csl.sri.com> wrote:
> 
>     Hi Sebastian,
> 
>     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?
> 
>     Thanks,
>     Sam
> 
>     Sebastian Verschoor <s.r.verschoor@student.rug.nl> wrote:
> 
>     > Hi Sam,
>     >
>     > Thanks for the fast reply. I have followed your instructions, but no
>     solution
>     > yet:
>     >
>     > 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:
>     > sebastian@sebastian-laptop:~/.school/afstudeerproject/ar/
>     > pvs-5.0-ix86-Linux-allegro$ which wish
>     > /usr/bin/wish
>     > sebastian@sebastian-laptop:~/.school/afstudeerproject/ar/
>     > pvs-5.0-ix86-Linux-allegro$ ll /usr/bin | grep wish
>     > lrwxrwxrwx  1 root   root          22 2010-07-28 02:12 wish -> /etc/
>     > alternatives/wish*
>     > -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*
>     > sebastian@sebastian-laptop:~/.school/afstudeerproject/ar/
>     > 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/
>     > wish8.4.1.gz
>     >
>     > Any other ideas on what could be the issue?
>     >
>     > Thanks,
>     > 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
>     >
>     >
>     > On 1 March 2012 03:44, Sam Owre <owre@csl.sri.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.
>     >     Thanks,
>     >     Sam
>     >
>     >     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
>     >
>     >
> 
>