Re: [PVS-Help] Simple PVS setup question

["Paul S. Miner" <paul.s.miner@nasa.gov>]

Ari,

Did you start PVS from within directory 
/home/<user>/pvs-3.2/Examples/ ?  If not, you need to explicitly tell 
PVS what is the current working directory (context).  The way to do 
this is via the M-x cc (change-context) command.

At 11:59 PM 6/6/2006, Ari Wilson wrote:
>Hi,
>
>I followed all of the instructions to install PVS on
>my machine and am running into the following problem
>(I haven't modified the pvs script or anything):
>
>I have a file, ex1.pvs that consists of the following:
>ex1: THEORY
>
>BEGIN
>
>f(x:nat):nat=x+1
>
>END ex1
>
>I do M-x tc and get the following message:
>/home/<user>/pvs-3.2/Examples/ex1.pvs is not in the
>current context
>
>Any suggestions? Thanks a lot.
>
>__________________________________________________
>Do You Yahoo!?
>Tired of spam?  Yahoo! Mail has the best spam protection around
>http://mail.yahoo.com

| Paul S. Miner, Ph.D.                      | phone: (757) 864-6201
| Senior Research Engineer                  | fax:   (757) 864-4234
| Safety-Critical Avionics Systems Branch  | mailto:paul.s.miner@nasa.gov
| NASA Langley Research Center      | http://shemesh.larc.nasa.gov/people/psm/
| Hampton, Virginia 23681-2199
-----------------------------------------------------
The contents herein do not necessarily reflect the positions of the 
United States Government.
-----------------------------------------------------