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

Re: [PVS-Help] not a valid pvs file



Hi Xiaoyu,

I'm not certain what is going on, but it looks like the lisp part of PVS
is not running (that's what the comint messages are about).  Did you run
bin/relocate after installing PVS?

Sam

xiaoyu xu <zhuhaiyu567@gmail.com> wrote:

> Hi everyone,
> I am a newer in pvs. And I want to proof an example. But when I type command
> M-x pa,
> it shows "*Message* is not a valid pvs file". I don't know how to solve this
> problem.
> 
> I followed the instruction in pvs-system-guide.pdf
> M-x new-pvs-file
> then type the name: sum
> then type the theory below.
> then type M-x pa. 
> 
> sum  % [ parameters ]
> : THEORY
> 
>   BEGIN
> 
>   % ASSUMING
>    % assuming declarations
>   % ENDASSUMING
> 
>   n: VAR nat
>   sum(n): RECURSIVE nat = 
>    (IF n = 0 THEN 0 ELSE n + sum(n - 1) ENDIF)
>    MEASURE (LAMBDA n: n)
>    closed_form: THEOREM sum(n) = n * (n - 1)/2
> 
>   END sum
> 
> I have also tried M-x tc, M-x pr. It didn't work.
> 
> When I try it this morning, the message is "wrong type argument: processp nil".
> Here is the message.
> 
> Loading pvs-prover-helps...done
> Loading pvs-eval...done
> Loading pvs-pvsio...done
> Initializing PVS: please wait...
> Entering debugger...
> new-pvs-file-name: ~/Downloads/pvs4.2/sum.pvs already exists.
> Making completion list...
> call-interactively: Text is read-only [8 times]
> comint-log: Wrong type argument: processp, nil [5 times]
> comint-log: Wrong type argument: processp, nil
> 
> I didn't edit .pvsemacs or .emcs. Is it something wrong with this?
> How can I edit these files?
> Thank you very much!
> 
> xiaoyu