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

[PVS-Help] not a valid pvs file



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