[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] not a valid pvs file
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
then type the name: sum
then type the theory below.
then type M-x pa.
sum % [ parameters ]
% assuming declarations
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
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.
Initializing PVS: please wait...
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!