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

Re: pvs batch mode



Makarand,

You can use '-l file' to load lisp code.
This is described on page 63 of the PVS User Guide.
Incidentally, you can use as many -l's and -f's as you want; they are
processed in the left-to-right order.  So, for example, you can run

pvs -l foo.el -f foo -l bar.el

where foo.el defines the function "foo" (of no arguments).  I usually just
use '-l file.el' as I can simply put "(foo)" at the end to get the same
effect.

Hope this helps,
Sam Owre

> From:    Makarand <makarand@ittc.ukans.edu>
> Subject: pvs batch mode
> Date:    Mon, 19 Jun 2000 14:36:24 CDT
> To:      pvs-help@csl.sri.com
> X-Accept-Language: en
> 
> 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
> 
> 
> **********************************************************
>                    Makarand Patil
>                System Level Design Group
>                 Call:- (785) 864 3041
> ----------------------------------------------------------