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

[PVS-Help] Latex Errors



Thanks for the swift response to my last e-mail Rick. I've got another 
problem with producing latex output. I can produce M-x latex-theory 
without trouble but I get errors on M-x latex-proof. I am using pdfeTeX 
using libpoppler 3.141592-1.30.5-2.2 (Web2C 7.5.5)

For some of my proofs I get "Error: Attempt to store the wrong type of a 
value in an array." in the *Errors* buffer. I don't know how to debug 
this. 

For other proofs, PVS generates the Latex but then I get errors 
converting the .tex to .dvi (E.G. if I run M-x latex-proof-view) - I 
only get a partial proof in the dvi file. I've tried setting 
latex-set-linelength = 200 and 2000 but still no joy.

I've attached the latex file and the pvs-files.log so you can see the 
errors. Let me know if you want me to send you the theories that PVS 
refuses to produce Latex for.

Thanks
 -- 
Eddy Seager
University of Manchester Undergrad
This is pdfeTeX, Version 3.141592-1.30.5-2.2 (Web2C 7.5.5) (format=latex 2007.10.9)  23 FEB 2008 16:22
entering extended mode
**pvs-files
(./pvs-files.tex
LaTeX2e <2003/12/01>
Babel <v3.8g> and hyphenation patterns for english, usenglishmax, dumylang, noh
yphenation, loaded.
(/usr/share/texmf-texlive/tex/latex/base/article.cls
Document Class: article 2004/02/16 v1.4f Standard LaTeX document class
(/usr/share/texmf-texlive/tex/latex/base/fleqn.clo
File: fleqn.clo 1998/08/17 v1.1c Standard LaTeX option (flush left equations)
\mathindent=\dimen102
)
(/usr/share/texmf-texlive/tex/latex/base/size12.clo
File: size12.clo 2004/02/16 v1.4f Standard LaTeX file (size option)
)
\c@part=\count79
\c@section=\count80
\c@subsection=\count81
\c@subsubsection=\count82
\c@paragraph=\count83
\c@subparagraph=\count84
\c@figure=\count85
\c@table=\count86
\abovecaptionskip=\skip41
\belowcaptionskip=\skip42
\bibindent=\dimen103
)
(/usr/share/texmf-texlive/tex/latex/preprint/fullpage.sty
Package: fullpage 1999/02/23 1.1 (PWD)
\FP@margin=\skip43
)
(/usr/share/texmf-texlive/tex/latex/supertabular/supertabular.sty
Package: supertabular 2004/02/20 v4.1e the supertabular environment
\c@tracingst=\count87
\ST@wd=\dimen104
\ST@rightskip=\skip44
\ST@leftskip=\skip45
\ST@parfillskip=\skip46
\ST@pageleft=\dimen105
\ST@headht=\dimen106
\ST@tailht=\dimen107
\ST@pagesofar=\dimen108
\ST@pboxht=\dimen109
\ST@lineht=\dimen110
\ST@stretchht=\dimen111
\ST@prevht=\dimen112
\ST@toadd=\dimen113
\ST@dimen=\dimen114
\ST@pbox=\box26
)
(/usr/share/texmf-texlive/tex/latex/base/alltt.sty
Package: alltt 1997/06/16 v2.0g defines alltt environment
)
(/usr/share/texmf-texlive/tex/latex/base/latexsym.sty
Package: latexsym 1998/08/17 v2.2e Standard LaTeX package (lasy symbols)
\symlasy=\mathgroup4
LaTeX Font Info:    Overwriting symbol font `lasy' in version `bold'
(Font)                  U/lasy/m/n --> U/lasy/b/n on input line 47.
)
(/home/edward/pvsNewInstall/pvs.sty
(/usr/share/texmf-texlive/tex/latex/amslatex/amsmath.sty
Package: amsmath 2000/07/18 v2.13 AMS math features
\@mathmargin=\skip47

For additional information on amsmath, use the `?' option.
(/usr/share/texmf-texlive/tex/latex/amslatex/amstext.sty
Package: amstext 2000/06/29 v2.01

(/usr/share/texmf-texlive/tex/latex/amslatex/amsgen.sty
File: amsgen.sty 1999/11/30 v2.0
\@emptytoks=\toks14
\ex@=\dimen115
))
(/usr/share/texmf-texlive/tex/latex/amslatex/amsbsy.sty
Package: amsbsy 1999/11/29 v1.2d
\pmbraise@=\dimen116
)
(/usr/share/texmf-texlive/tex/latex/amslatex/amsopn.sty
Package: amsopn 1999/12/14 v2.01 operator names
)
\inf@bad=\count88
LaTeX Info: Redefining \frac on input line 211.
\uproot@=\count89
\leftroot@=\count90
LaTeX Info: Redefining \overline on input line 307.
\classnum@=\count91
\DOTSCASE@=\count92
LaTeX Info: Redefining \ldots on input line 379.
LaTeX Info: Redefining \dots on input line 382.
LaTeX Info: Redefining \cdots on input line 467.
\Mathstrutbox@=\box27
\strutbox@=\box28
\big@size=\dimen117
LaTeX Font Info:    Redeclaring font encoding OML on input line 567.
LaTeX Font Info:    Redeclaring font encoding OMS on input line 568.
\macc@depth=\count93
\c@MaxMatrixCols=\count94
\dotsspace@=\muskip10
\c@parentequation=\count95
\dspbrk@lvl=\count96
\tag@help=\toks15
\row@=\count97
\column@=\count98
\maxfields@=\count99
\andhelp@=\toks16
\eqnshift@=\dimen118
\alignsep@=\dimen119
\tagshift@=\dimen120
\tagwidth@=\dimen121
\totwidth@=\dimen122
\lineht@=\dimen123
\@envbody=\toks17
\multlinegap=\skip48
\multlinetaggap=\skip49
\mathdisplay@stack=\toks18
LaTeX Info: Redefining \[ on input line 2666.
LaTeX Info: Redefining \] on input line 2667.
)) (./pvs-files.aux)
\openout1 = `pvs-files.aux'.

LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 5.
LaTeX Font Info:    ... okay on input line 5.
LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 5.
LaTeX Font Info:    ... okay on input line 5.
LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 5.
LaTeX Font Info:    ... okay on input line 5.
LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 5.
LaTeX Font Info:    ... okay on input line 5.
LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 5.
LaTeX Font Info:    ... okay on input line 5.
LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 5.
LaTeX Font Info:    ... okay on input line 5.

(./tan_antiderivative.tex
LaTeX Font Info:    Try loading font information for U+lasy on input line 24.
 (/usr/share/texmf-texlive/tex/latex/base/ulasy.fd
File: ulasy.fd 1998/08/17 v2.2e LaTeX symbol font definitions
)
Overfull \hbox (4.29462pt too wide) in paragraph at lines 23--28
[]|  [] 
 []


Overfull \hbox (4.29462pt too wide) in paragraph at lines 33--38
[]|  [] 
 []


Overfull \hbox (8.21124pt too wide) in paragraph at lines 45--50
[]|  [] 
 []


Overfull \hbox (8.21124pt too wide) in paragraph at lines 57--62
[]|  [] 
 []


Overfull \hbox (8.21124pt too wide) in paragraph at lines 70--75
[]|  [] 
 []


Overfull \hbox (8.21124pt too wide) in paragraph at lines 84--89
[]|  [] 
 []


Overfull \hbox (8.21124pt too wide) in paragraph at lines 96--101
[]|  [] 
 []


Overfull \hbox (8.21124pt too wide) in paragraph at lines 108--113
[]|  [] 
 []

[1

]
Overfull \hbox (24.335pt too wide) in paragraph at lines 122--122
[]\OT1/cmr/m/n/12 deriv($[]$) $=$ ($\OML/cmm/m/it/12 ^^U$ \OT1/cmr/m/n/12 (x[]1
\OT1/cmtt/m/n/12 : \OT1/cmr/m/n/12 real[]abs[]lt[]pi2)\OT1/cmtt/m/n/12 : $[]$\O
T1/cmr/m/n/12 )[] 
 []


Overfull \hbox (8.21124pt too wide) in paragraph at lines 120--125
[]|  [] 
 []


Overfull \hbox (24.335pt too wide) in paragraph at lines 134--134
[]\OT1/cmr/m/n/12 deriv($[]$) $=$ ($\OML/cmm/m/it/12 ^^U$ \OT1/cmr/m/n/12 (x[]1
\OT1/cmtt/m/n/12 : \OT1/cmr/m/n/12 real[]abs[]lt[]pi2)\OT1/cmtt/m/n/12 : $[]$\O
T1/cmr/m/n/12 )[] 
 []


Overfull \hbox (8.21124pt too wide) in paragraph at lines 132--137
[]|  [] 
 []


! LaTeX Error: Bad math environment delimiter.

See the LaTeX manual or LaTeX Companion for explanation.
Type  H <return>  for immediate help.
 ...                                              
                                                  
l.148 ...pvsid{cos}\pvsid{(}\pvsid{x\_1}\pvsid{)}}
                                                  \)\pvsid{)}\end{alltt}}\en...

? 
! Emergency stop.
 ...                                              
                                                  
l.148 ...pvsid{cos}\pvsid{(}\pvsid{x\_1}\pvsid{)}}
                                                  \)\pvsid{)}\end{alltt}}\en...

Your command was ignored.
Type  I <command> <return>  to replace it with another command,
or  <return>  to continue without it.

 
Here is how much of TeX's memory you used:
 1031 strings out of 95213
 12521 string characters out of 1185476
 70340 words of memory out of 1000000
 4190 multiletter control sequences out of 10000+50000
 7873 words of font info for 32 fonts, out of 500000 for 2000
 28 hyphenation exceptions out of 8191
 34i,14n,24p,1323b,342s stack positions out of 1500i,500n,5000p,200000b,5000s
Output written on pvs-files.dvi (1 page, 4136 bytes).

trig_deriv2.tex