[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Can one use comments in strategies?
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.
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: firstname.lastname@example.org, email@example.com
> From: Tamarah Arons <firstname.lastname@example.org>
> Subject: Can one use comments in strategies?
> 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?