PWD /home/master/thesis/bug3_minimal INPUT /usr/share/texmf/web2c/texmf.cnf INPUT /var/lib/texmf/web2c/pdftex/latex.fmt INPUT bug.tex OUTPUT bug.log INPUT /usr/share/texmf-texlive/tex/latex/base/fix-cm.sty INPUT /usr/share/texmf-texlive/tex/latex/base/fix-cm.sty INPUT /usr/share/texmf-texlive/tex/latex/base/ts1enc.def INPUT /usr/share/texmf-texlive/tex/latex/base/ts1enc.def INPUT /usr/share/texmf-texlive/tex/latex/base/report.cls INPUT /usr/share/texmf-texlive/tex/latex/base/report.cls INPUT /usr/share/texmf-texlive/tex/latex/base/size12.clo INPUT /usr/share/texmf-texlive/tex/latex/base/size12.clo INPUT /usr/share/texmf-texlive/fonts/map/fontname/texfonts.map INPUT /usr/share/texmf-texlive/fonts/map/fontname/texfonts.map INPUT /usr/share/texmf-texlive/fonts/tfm/public/cm/cmr12.tfm INPUT /usr/share/texmf-texlive/tex/latex/base/fixltx2e.sty INPUT /usr/share/texmf-texlive/tex/latex/base/fixltx2e.sty INPUT /usr/share/texmf-texlive/tex/latex/preprint/fullpage.sty INPUT /usr/share/texmf-texlive/tex/latex/preprint/fullpage.sty INPUT /usr/share/texmf-texlive/tex/latex/ntheorem/ntheorem.sty INPUT /usr/share/texmf-texlive/tex/latex/ntheorem/ntheorem.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/ifpdf.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/ifpdf.sty INPUT /usr/share/texmf-texlive/tex/latex/hyperref/hyperref.sty INPUT /usr/share/texmf-texlive/tex/latex/hyperref/hyperref.sty INPUT /usr/share/texmf-texlive/tex/latex/graphics/keyval.sty INPUT /usr/share/texmf-texlive/tex/latex/graphics/keyval.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/ifvtex.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/ifvtex.sty INPUT /usr/share/texmf-texlive/tex/generic/ifxetex/ifxetex.sty INPUT /usr/share/texmf-texlive/tex/generic/ifxetex/ifxetex.sty INPUT /usr/share/texmf-texlive/tex/latex/oberdiek/hycolor.sty INPUT /usr/share/texmf-texlive/tex/latex/oberdiek/hycolor.sty INPUT /usr/share/texmf-texlive/tex/latex/oberdiek/xcolor-patch.sty INPUT /usr/share/texmf-texlive/tex/latex/oberdiek/xcolor-patch.sty INPUT /usr/share/texmf-texlive/tex/latex/hyperref/pd1enc.def INPUT /usr/share/texmf-texlive/tex/latex/hyperref/pd1enc.def INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/etexcmds.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/etexcmds.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/infwarerr.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/infwarerr.sty INPUT /etc/texmf/tex/latex/config/hyperref.cfg INPUT /etc/texmf/tex/latex/config/hyperref.cfg INPUT /usr/share/texmf-texlive/tex/latex/oberdiek/kvoptions.sty INPUT /usr/share/texmf-texlive/tex/latex/oberdiek/kvoptions.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/kvsetkeys.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/kvsetkeys.sty INPUT /usr/share/texmf-texlive/tex/latex/ltxmisc/url.sty INPUT /usr/share/texmf-texlive/tex/latex/ltxmisc/url.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/bitset.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/bitset.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/intcalc.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/intcalc.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/bigintcalc.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/bigintcalc.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/pdftexcmds.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/pdftexcmds.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/ifluatex.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/ifluatex.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/ltxcmds.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/ltxcmds.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/atbegshi.sty INPUT /usr/share/texmf-texlive/tex/generic/oberdiek/atbegshi.sty INPUT /usr/share/texmf-texlive/tex/latex/hyperref/hypertex.def INPUT /usr/share/texmf-texlive/tex/latex/hyperref/hypertex.def INPUT bug.aux INPUT bug.aux OUTPUT bug.aux INPUT /usr/share/texmf-texlive/tex/latex/hyperref/nameref.sty INPUT /usr/share/texmf-texlive/tex/latex/hyperref/nameref.sty INPUT /usr/share/texmf-texlive/tex/latex/oberdiek/refcount.sty INPUT /usr/share/texmf-texlive/tex/latex/oberdiek/refcount.sty INPUT /usr/share/texmf-texlive/fonts/tfm/public/cm/cmr17.tfm INPUT /usr/share/texmf-texlive/fonts/tfm/public/cm/cmbx12.tfm INPUT /usr/share/texmf-texlive/fonts/tfm/public/cm/cmti12.tfm INPUT /usr/share/texmf-texlive/fonts/tfm/public/cm/cmbx12.tfm INPUT /usr/share/texmf-texlive/fonts/tfm/public/cm/cmr8.tfm INPUT /usr/share/texmf-texlive/fonts/tfm/public/cm/cmr6.tfm INPUT /usr/share/texmf-texlive/fonts/tfm/public/cm/cmmi12.tfm INPUT /usr/share/texmf-texlive/fonts/tfm/public/cm/cmmi8.tfm INPUT /usr/share/texmf-texlive/fonts/tfm/public/cm/cmmi6.tfm INPUT /usr/share/texmf-texlive/fonts/tfm/public/cm/cmsy10.tfm INPUT /usr/share/texmf-texlive/fonts/tfm/public/cm/cmsy8.tfm INPUT /usr/share/texmf-texlive/fonts/tfm/public/cm/cmsy6.tfm OUTPUT bug.thm OUTPUT bug.dvi INPUT bug.aux
bug.dvi
Description: TeX dvi file
Description: TeX dvi file\RequirePackage{fix-cm} \documentclass[a4paper,12pt]{report} \usepackage{fixltx2e} \usepackage{fullpage} \usepackage{ntheorem} \usepackage{ifpdf} \ifpdf \usepackage[pdftex,bookmarks=true]{hyperref} \else \ifx\hrd\undefined \ifx\lempdf\undefined\def\hrd{hypertex}\else\def\hrd{dvipdfm}\fi \fi \ifx\gxd\undefined \ifx\lempdf\undefined\def\gxd{dvips}\else\def\gxd{dvipdfm}\fi \fi \usepackage[\hrd]{hyperref} \fi \newtheorem{definition}{Definition}[section] \begin{document} \chapter{Too much vspace} The user interacts with a proof assistant via a proof script in the following general sense. \begin{definition}[proof script] A \emph{proof script} is the sequence of instructions a user gives a proof assistant to prove a statement. \end{definition} The user interacts with a proof assistant via a proof script in the following general sense \begin{definition}[proof script] A \emph{proof script} is the sequence of instructions a user gives a proof assistant to prove a statement. \end{definition} The user interacts with a proof assistant via a proof script in the following general sense. \begin{definition}[proof script] A \emph{proof script} is the sequence of instructions a user gives a proof assistant to prove a statement. \end{definition} The user interacts with a proof assistant via a proof script in the following general sense \begin{definition}[proof script] A \emph{proof script} is the sequence of instructions a user gives a proof assistant to prove a statement. \end{definition} \end{document}This is pdfTeX, Version 3.1415926-1.40.10 (TeX Live 2009/Debian) (format=latex 2011.6.10) 22 MAY 2012 13:52 entering extended mode %&-line parsing enabled. **bug.tex (./bug.tex LaTeX2e <2009/09/24> Babel <v3.8l> and hyphenation patterns for english, usenglishmax, dumylang, noh yphenation, farsi, arabic, croatian, bulgarian, ukrainian, russian, czech, slov ak, danish, dutch, finnish, french, basque, ngerman, german, german-x-2009-06-1 9, ngerman-x-2009-06-19, ibycus, monogreek, greek, ancientgreek, hungarian, san skrit, italian, latin, latvian, lithuanian, mongolian2a, mongolian, bokmal, nyn orsk, romanian, irish, coptic, serbian, turkish, welsh, esperanto, uppersorbian , estonian, indonesian, interlingua, icelandic, kurmanji, slovenian, polish, po rtuguese, spanish, galician, catalan, swedish, ukenglish, pinyin, loaded. (/usr/share/texmf-texlive/tex/latex/base/fix-cm.sty Package: fix-cm 2006/09/13 v1.1m fixes to LaTeX (/usr/share/texmf-texlive/tex/latex/base/ts1enc.def File: ts1enc.def 2001/06/05 v3.0e (jk/car/fm) Standard LaTeX file )) (/usr/share/texmf-texlive/tex/latex/base/report.cls Document Class: report 2007/10/19 v1.4h Standard LaTeX document class (/usr/share/texmf-texlive/tex/latex/base/size12.clo File: size12.clo 2007/10/19 v1.4h Standard LaTeX file (size option) ) \c@part=\count79 \c@chapter=\count80 \c@section=\count81 \c@subsection=\count82 \c@subsubsection=\count83 \c@paragraph=\count84 \c@subparagraph=\count85 \c@figure=\count86 \c@table=\count87 \abovecaptionskip=\skip41 \belowcaptionskip=\skip42 \bibindent=\dimen102 ) (/usr/share/texmf-texlive/tex/latex/base/fixltx2e.sty Package: fixltx2e 2006/09/13 v1.1m fixes to LaTeX LaTeX Info: Redefining \em on input line 420. ) (/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/ntheorem/ntheorem.sty Style `ntheorem', Version 1.25 <2005/07/07> Package: ntheorem 2005/07/07 1.25 \theorem@style=\toks14 \theorem@@style=\toks15 \theorembodyfont=\toks16 \theoremnumbering=\toks17 \theorempreskipamount=\skip44 \theorempostskipamount=\skip45 \theoremindent=\dimen103 \theorem@indent=\dimen104 \theoremheaderfont=\toks18 \theoremseparator=\toks19 \theoremprework=\toks20 \theorempostwork=\toks21 \theoremsymbol=\toks22 \qedsymbol=\toks23 \theoremkeyword=\toks24 \qedsymbol=\toks25 \thm@topsepadd=\skip46 ) (/usr/share/texmf-texlive/tex/generic/oberdiek/ifpdf.sty Package: ifpdf 2009/04/10 v2.0 Provides the ifpdf switch (HO) Package ifpdf Info: pdfTeX in pdf mode not detected. ) (/usr/share/texmf-texlive/tex/latex/hyperref/hyperref.sty Package: hyperref 2009/10/09 v6.79a Hypertext links for LaTeX (/usr/share/texmf-texlive/tex/latex/graphics/keyval.sty Package: keyval 1999/03/16 v1.13 key=value parser (DPC) \KV@toks@=\toks26 ) (/usr/share/texmf-texlive/tex/generic/oberdiek/ifvtex.sty Package: ifvtex 2008/11/04 v1.4 Switches for detecting VTeX and its modes (HO) Package ifvtex Info: VTeX not detected. ) (/usr/share/texmf-texlive/tex/generic/ifxetex/ifxetex.sty Package: ifxetex 2009/01/23 v0.5 Provides ifxetex conditional ) (/usr/share/texmf-texlive/tex/latex/oberdiek/hycolor.sty Package: hycolor 2009/10/02 v1.5 Code for color options of hyperref/bookmark (H O) (/usr/share/texmf-texlive/tex/latex/oberdiek/xcolor-patch.sty Package: xcolor-patch 2009/10/02 xcolor patch )) \@linkdim=\dimen105 \Hy@linkcounter=\count88 \Hy@pagecounter=\count89 (/usr/share/texmf-texlive/tex/latex/hyperref/pd1enc.def File: pd1enc.def 2009/10/09 v6.79a Hyperref: PDFDocEncoding definition (HO) ) (/usr/share/texmf-texlive/tex/generic/oberdiek/etexcmds.sty Package: etexcmds 2007/12/12 v1.2 Prefix for e-TeX command names (HO) (/usr/share/texmf-texlive/tex/generic/oberdiek/infwarerr.sty Package: infwarerr 2007/09/09 v1.2 Providing info/warning/message (HO) ) Package etexcmds Info: Could not find \expanded. (etexcmds) That can mean that you are not using pdfTeX 1.50 or (etexcmds) that some package has redefined \expanded. (etexcmds) In the latter case, load this package earlier. ) (/etc/texmf/tex/latex/config/hyperref.cfg File: hyperref.cfg 2002/06/06 v1.2 hyperref configuration of TeXLive ) (/usr/share/texmf-texlive/tex/latex/oberdiek/kvoptions.sty Package: kvoptions 2009/08/13 v3.4 Keyval support for LaTeX options (HO) (/usr/share/texmf-texlive/tex/generic/oberdiek/kvsetkeys.sty Package: kvsetkeys 2009/07/30 v1.5 Key value parser with default handler suppor t (HO) )) Package hyperref Info: Hyper figures OFF on input line 2975. Package hyperref Info: Link nesting OFF on input line 2980. Package hyperref Info: Hyper index ON on input line 2983. Package hyperref Info: Plain pages OFF on input line 2990. Package hyperref Info: Backreferencing OFF on input line 2995. Implicit mode ON; LaTeX internals redefined Package hyperref Info: Bookmarks ON on input line 3191. (/usr/share/texmf-texlive/tex/latex/ltxmisc/url.sty \Urlmuskip=\muskip10 Package: url 2006/04/12 ver 3.3 Verb mode for urls, etc. ) LaTeX Info: Redefining \url on input line 3428. (/usr/share/texmf-texlive/tex/generic/oberdiek/bitset.sty Package: bitset 2007/09/28 v1.0 Data type bit set (HO) (/usr/share/texmf-texlive/tex/generic/oberdiek/intcalc.sty Package: intcalc 2007/09/27 v1.1 Expandable integer calculations (HO) ) (/usr/share/texmf-texlive/tex/generic/oberdiek/bigintcalc.sty Package: bigintcalc 2007/11/11 v1.1 Expandable big integer calculations (HO) (/usr/share/texmf-texlive/tex/generic/oberdiek/pdftexcmds.sty Package: pdftexcmds 2009/09/23 v0.6 LuaTeX support for pdfTeX utility functions (HO) (/usr/share/texmf-texlive/tex/generic/oberdiek/ifluatex.sty Package: ifluatex 2009/04/17 v1.2 Provides the ifluatex switch (HO) Package ifluatex Info: LuaTeX not detected. ) (/usr/share/texmf-texlive/tex/generic/oberdiek/ltxcmds.sty Package: ltxcmds 2009/08/05 v1.0 Some LaTeX kernel commands for general use (HO ) ) Package pdftexcmds Info: LuaTeX not detected. Package pdftexcmds Info: \pdf@primitive is available. Package pdftexcmds Info: \pdf@ifprimitive is available. ))) \Fld@menulength=\count90 \Field@Width=\dimen106 \Fld@charsize=\dimen107 \Field@toks=\toks27 Package hyperref Info: Hyper figures OFF on input line 4377. Package hyperref Info: Link nesting OFF on input line 4382. Package hyperref Info: Hyper index ON on input line 4385. Package hyperref Info: backreferencing OFF on input line 4392. Package hyperref Info: Link coloring OFF on input line 4397. Package hyperref Info: Link coloring with OCG OFF on input line 4402. Package hyperref Info: PDF/A mode OFF on input line 4407. (/usr/share/texmf-texlive/tex/generic/oberdiek/atbegshi.sty Package: atbegshi 2008/07/31 v1.9 At begin shipout hook (HO) ) \Hy@abspage=\count91 \c@Item=\count92 \c@Hfootnote=\count93 ) *hyperref using driver hypertex* (/usr/share/texmf-texlive/tex/latex/hyperref/hypertex.def File: hypertex.def 2009/10/09 v6.79a Hyperref driver for HyperTeX specials ) \c@definition=\count94 (./bug.aux) \openout1 = `bug.aux'. LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 23. LaTeX Font Info: ... okay on input line 23. LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 23. LaTeX Font Info: ... okay on input line 23. LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 23. LaTeX Font Info: ... okay on input line 23. LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 23. LaTeX Font Info: ... okay on input line 23. LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 23. LaTeX Font Info: ... okay on input line 23. LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 23. LaTeX Font Info: ... okay on input line 23. LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 23. LaTeX Font Info: ... okay on input line 23. LaTeX Font Info: Checking defaults for PD1/pdf/m/n on input line 23. LaTeX Font Info: ... okay on input line 23. Package hyperref Info: Link coloring OFF on input line 23. (/usr/share/texmf-texlive/tex/latex/hyperref/nameref.sty Package: nameref 2007/05/29 v2.31 Cross-referencing by name of section (/usr/share/texmf-texlive/tex/latex/oberdiek/refcount.sty Package: refcount 2008/08/11 v3.1 Data extraction from references (HO) ) \c@section@level=\count95 ) LaTeX Info: Redefining \ref on input line 23. LaTeX Info: Redefining \pageref on input line 23. \AtBeginShipoutBox=\box26 Chapter 1. LaTeX Font Info: External font `cmex10' loaded for size (Font) <12> on input line 28. LaTeX Font Info: External font `cmex10' loaded for size (Font) <8> on input line 28. LaTeX Font Info: External font `cmex10' loaded for size (Font) <6> on input line 28. Package hyperref Info: bookmark level for unknown definition defaults to 0 on i nput line 28. \tf@thm=\write3 \openout3 = `bug.thm'. [1 ] (./bug.aux) ) Here is how much of TeX's memory you used: 4051 strings out of 493849 62587 string characters out of 1152846 116235 words of memory out of 3000000 7309 multiletter control sequences out of 15000+50000 7636 words of font info for 27 fonts, out of 3000000 for 9000 714 hyphenation exceptions out of 8191 38i,4n,21p,251b,291s stack positions out of 5000i,500n,10000p,200000b,50000s Output written on bug.dvi (1 page, 1980 bytes).
