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

PVS-Latex problems



Today I tried to use the latex-interface of PVS to
display proofs. I got problems running latex since 
some of the tabs generated seem to be undefined.

I'll include the frame-file but won't include
the proof .tex-file (which is a little too large).
Furtermore I'll include the tex-errors produced for
the first occurrences.

Probably I did use a wrong version of latex or
did not use the required .sty-files.

Bettina Buth

---------------------------------------------------------------------------
| Dr. Bettina Buth                   | Tel. : ++49-421-218-2955           |
| FB 3 Informatik                    | Fax  : ++49-421-218-3054           |
| Universitaet Bremen                | email: bb@informatik.uni-bremen.de |
| Postfach 330 440, D-28334 Bremen   |                                    |
---------------------------------------------------------------------------

\documentclass{article}

\usepackage{a4}
\usepackage{pvs}
\usepackage{supertab}
\usepackage{fullpage}
\usepackage{alltt}

\begin{document}
\include{dcpa_1_inv_loop_I_5_1_7}
\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
----------
X-Sun-Data-Type: default
X-Sun-Data-Description: default
X-Sun-Data-Name: tex-error
X-Sun-Charset: us-ascii
X-Sun-Content-Lines: 34

Running `LaTeX' on `pvs-frame' with ``latex '\nonstopmode\input{pvs-frame.tex}'''
This is TeX, Version 3.14159 (C version 6.1)
LaTeX2e <1996/06/01>
Hyphenation patterns for english, german, loaded.

(pvs-frame.tex (/usr/local/share/teTeX/texmf/tex/latex/base/article.cls
Document Class: article 1996/05/26 v1.3r Standard LaTeX document class
(/usr/local/share/teTeX/texmf/tex/latex/base/size10.clo))
(/usr/local/share/teTeX/texmf/tex/latex/ntgclass/a4.sty) (pvs.sty)
(supertab.sty) (fullpage.sty
Style Option FULLPAGE Version 2 as of 15 Dec 1988
) (alltt.sty) (pvs-frame.aux (dcpa_1_inv_loop_I_5_1_7.aux))
(dcpa_1_inv_loop_I_5_1_7.tex

! LaTeX Error: Undefined tab position.

See the LaTeX manual or LaTeX Companion for explanation.
Type  H   for immediate help.
 ...                                              
                                                  
l.164 \pvsid{allin}))))) })\\[-\baselineskip]\oo
                                                \zo\zo\zo\zo\zo\zo \end{prog...


! LaTeX Error: Undefined tab position.

See the LaTeX manual or LaTeX Companion for explanation.
Type  H   for immediate help.
 ...                                              
                                                  
l.164 ...))))) })\\[-\baselineskip]\oo\zo\zo\zo\zo
                                                  \zo\zo \end{program}}\end{...