[PVS-Help] PVS proof-trees

Subject: [PVS-Help] PVS proof-trees

From: Sebastian Verschoor <s.r.verschoor@xxxxxxxxxxxxxx>

Date: Wed, 29 Feb 2012 18:12:24 +0100

Authentication-Results: mr.google.com; spf=pass (google.com: domain ofsebastian.verschoor@gmail.com designates 10.52.71.146 aspermitted sender) smtp.mail=sebastian.verschoor@gmail.com;dkim=pass header.i=sebastian.verschoor@gmail.com

DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma;h=mime-version:sender:from:date:x-google-sender-auth:message-id:subject:to:content-type;bh=N8BZiNzbDBvFgMFIFhJZGgmiWQkxjspmAfc6Rd/LMG4=;b=Nl83AD3d81V6OujcFVNiyI3fU4uRpKVJbL9QN1Da/5N+AfZrCqW/VkDJHgYaszOpXINV1qBj0i8CIWeSHCL3TP1/1moqUcdOgFdtm6k9L5b0TZkImoqIfkhLha1XgGIvVlrpe9iZ0CrsryYqeflc6VlRroY//W55DEUzQj0Y2eI=

List-Help: <mailto:pvs-help-request@csl.sri.com?subject=help>

List-Id: PVS-Help <pvs-help.csl.sri.com>

List-Post: <mailto:pvs-help@csl.sri.com>

List-Subscribe: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>

List-Unsubscribe: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>

Sender: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

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