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

Re: [PVS-Help] PVS batch mode



Thanks a lot for Sam to recognize the error for me. However, I do not
know why it des not display the result after using the strategy
"GRIND". (Sorry if the question seems so "baby")

I fix the error, and try it again.

----------------prove-all.el------------------
(pvs-message "Proving all unproven theorems in batch.pvs")
(typecheck "batch")
(let ((current-prefix-arg t))
 (prove-untried-pvs-file "batch" "(grind)"))
(pvs-message "Completed")
-----------------batch.pvs----------------------------
batch: THEORY
BEGIN

  a : theorem  1 < 2
  b : theorem  2 < 3
  c : theorem  3 < 4
  d : theorem  4 < 5

END batch

> pvs -batch -load prove-all.el
Loading /usr/lib/xemacs/xemacs-packages/lisp/site-start.d/psgml-init.el...
Loading pvs-load...
Loading pvs-prelude-files-and-regions...
Proving all unproven theorems in batch.pvs
Proving all unproven theorems in batch.pvs
Completed
Completed

Proving all unproven theorems in batch.pvs
Completed

(No files need saving)
Buffer *scratch* has no process



On 9/8/06, Sam Owre <owre@csl.sri.com> wrote:
> Hi Sara,
>
> I see the problem - the
>
> (pvs-message "Completed)
>
> is missing the closing string quote - it should be:
>
> (pvs-message "Completed")
>
> Sam
>