[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("&#193;&#194;\"&#135;" [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