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

pvs batch mode

I have PVS running in batch mode with -batch option.
I have some lisp functions that invoke PVS theorem prover commands and
do automated type-checking and proofs. The problem is i need to 
load these functions along with pvs environment in batch mode and then 
run my function..i.e
on command line have something like
$ pvs -batch -q -f my_function

Right now i am struggling  with running "my_function"(With no arguments)
using the above technique. 
Is there a way to load my lisp code (which calls PVS prover commands)
and run it in a batch mode?
Appreciate an early reply,

                   Makarand Patil
               System Level Design Group
                Call:- (785) 864 3041