Re: Can one use comments in strategies?

[Dave Stringer-Calvert <dave_sc@csl.sri.com>]

Tamarah -

This is indeed a bug.  You can use (comment) in strategies, but the
edit-proof mechanisms don't treat comments in proof scripts properly.
We'll try and get a patch for this shortly.

Thanks,
Dave

---
Dr Dave Stringer-Calvert,  Senior Project Manager,  Computer Science Lab
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA
Phone: (650) 859-3291 Fax: (650) 859-2844 David.Stringer-Calvert@sri.com



> Date:    Fri, 15 Jun 2001 16:50:38 +0300
> To:      pvs-help@csl.sri.com, tamarah@narkis.wisdom.weizmann.ac.il
> From:    Tamarah Arons <tamarah@wisdom.weizmann.ac.il>
> Subject: Can one use comments in strategies?
> 
> Hello,
> 
> I have been adding comments to strategies and have come across a
> problem : if I edit a proof file with comments in it from strategies 
> it seems to delete the commands after the comment. This happens 
> even if I just open the file for editing and then install it unchanged. 
> 
> Below is a PVS dump file with a short proof exhibiting this problem. 
> It was run on PVS2-3. Using a patch does not seem to make a difference.
> If you edit the proof using (M-x edit-proof), save, and then install it, 
> with or without making changes, the commands after (CASEPROP) are 
> replaced with NIL.
> 
> Is there some prohibition on using comments in strategies? 
> Or is there some rule regarding their use that I am violating?
> 
> Thanks,
> Tamarah