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

[PVS-Help] PVS proof-trees

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
% set tk_version
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 Verschoor
StudentNr: s1910396
LinkedIn: http://www.linkedin.com/in/sebastianverschoor
PGP key fingerprint: 268B E86C 4E2C 2C5A 086E  408C 8FEE 241D 5BC9 740D