[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