[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-HELP]-Install problem
Dear folks:
When I run the "PVS".In one buffer show these information:
"Debugger entered--Lisp error: (wrong-number-of-arguments #<subr set-match-data> 2)
set-match-data((2 7) evaporate)
byte-code("ÁÂ\"‡" [save-match-data-internal set-match-data evaporate] 3)
pvs-extract-expected-from-output("\"4.2\"" nil)
pvs-send-and-wait("*pvs-version*" nil nil)
pvs-major-version-number()
pvs()
load("pvs-load" nil nil nil)
eval-buffer(#<buffer *load*> nil "/home/Root/Pvs_files/pvs-4.2-ix86-Linux-cmulisp.tgz_FILES/emacs/go-pvs.el" nil t)
;;; Reading at buffer position 2780
load-with-code-conversion("/home/Root/Pvs_files/pvs-4.2-ix86-Linux-cmulisp.tgz_FILES/emacs/go-pvs.el" "/home/Root/Pvs_files/pvs-4.2-ix86-Linux-cmulisp.tgz_FILES/emacs/go-pvs.el" nil t)
load("/home/Root/Pvs_files/pvs-4.2-ix86-Linux-cmulisp.tgz_FILES/emacs/go-pvs.el" nil t)
command-line-1(("-load" "/home/Root/Pvs_files/pvs-4.2-ix86-Linux-cmulisp.tgz_FILES/emacs/go-pvs.el"))
command-line()
normal-top-level()
".
If I ignore these, run a demo from "Example/sum.pvs", I can success in "parse and typechecker". But failed in "prover command". The message buffer show the information is :
byte-code:(wrong-number-of-arguments #<subr set-match-data> 2).
I can`t fix this problem. Anyone know this?
Best regards
Song