Re: [PVS-Help] Latex in pvs

[Sam Owre <owre@csl.sri.com>]

> Hi, I'm having trouble running latex on my theories.  I get the
> message
> 
> The slot name is missing from the object
> #<auto-rewrite-plus-decl sq_simrel.nil> of class
> #<standard-class auto-rewrite-plus-decl> during operation slot-value
> 
> when running M-x latex-{theory,pvs-file}.  However there seems to be
> no trouble generating latex for proofs (M-x latex-proof).
> 
> It looks like bugs 770, 812 and 823 are relevant, but I can't seem
> to get any useful info from the bug reports.  Any help appreciated
> 
> Thanks,
> Rob

Hi Rob,

The latex printing for auto-rewrite declarations wasn't quite right - I'm
including the patches below.  Just add them to your ~/.pvs.lisp file in
your home directory (create it if it doesn't exist), and it should work.
Let me know if you have any other problems.

Thanks,
Sam

------

(defmethod pp-tex* :around ((decl auto-rewrite-decl))
  (with-slots (rewrite-names semi) decl
    (when (or (not *pretty-printing-decl-list*)
	      (not *pretty-printed-prefix*))
      (when *pretty-printing-decl-list*
	(setq *pretty-printed-prefix* t))
      (typecase decl
	(auto-rewrite-plus-decl (pp-tex-keyword 'AUTO_REWRITE+))
	(auto-rewrite-minus-decl (pp-tex-keyword 'AUTO_REWRITE-))
	(t (pp-tex-keyword 'AUTO_REWRITE)))
      (write-char #\space)
      (pprint-newline :miser))
    (pp-tex-rewrite-names rewrite-names)
    (when semi
      (write-char #\;))
    (pprint-newline :mandatory)))

(defun pp-tex-rewrite-names (names)
  (pprint-logical-block (nil names)
    (loop (pp-tex* (pprint-pop))
	  (pprint-exit-if-list-exhausted)
	  (write-char #\,)
	  (write-char #\space)
	  (pprint-newline :fill))))