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

Re: Help - using PVS



> Hi,
> 
> 1. Is there any possibility to disable pretty-printing on the
> proof(.prf) file ?
>    I have to prove some lemmas, in which each of them had a long proof
>    sequence (> 300 commands). Because of the preety printing, the proof
> file
>    exploded. each proof can take > 200K.

Yes, use M-x toggle-proof-prettyprinting to change it from the default.
If you want to change the default, you can add the line
 (pvs-send "(setq *save-proofs-pretty* nil)")
to your ~/.pvsemacs file.

> 2. Is there any primitive proof command to expand a definition without 
>    simplification ?

Yes, (expand "x" :assert? none) will expand x without simplification.
(help expand) gives more information.

> 3. In the middle of my proof, I wanted to expand a definition.
>    Somehow, the command (ex: (expand "x")) took a very long time > 10
> minutes.
>    Is it because of simplification ? Any suggestion on what should I do
> ?
>    (If it's needed, I have a dump file for the lemma. The file size is
>     around 1.2 M)
>    fyi: My system is running on LINUX - PII 400 - 256M(RAM)

It is possibly due to simplification, though it's hard to say without more
information.  Why don't you go ahead and send the dump file (or tell me
where to pick it up) and I'll take a look.

Thanks,

Sam Owre <Owre@csl.sri.com>
Computer Science Lab, SRI International   Tel: (650) 859-5114              
333 Ravenswood Avenue                     FAX: (650) 859-2844              
Menlo Park, CA  94025 USA                 WWW: http://www.csl.sri.com/~owre